From: Mart Lubbers Date: Tue, 1 Mar 2016 20:06:50 +0000 (+0100) Subject: started with 4 X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=03b9678956cef4bfefb4fd76ab72d48ab5a4dae9;p=mc1516.git started with 4 --- diff --git a/.gitignore b/.gitignore index 6f82654..0dd8aea 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,5 @@ *.aux *.pdf *.dvi +NuSMV +nusmv diff --git a/e3.tex b/e3.tex index 33bcca5..4c5e97d 100644 --- a/e3.tex +++ b/e3.tex @@ -37,21 +37,24 @@ Sat(\forall(a\un \forall\ev c))=\{s_0,s_1,s_4\}\\ \{s_0\}\subseteq \{s_0,s_1,s_4\}\text{ thus }\Phi_2\text{ is satisfied} $ \item + \item For formula: $$\varphi:=\al(a\ra(\neg b\un(a\wedge b)))$$ We create an automaton $\neg\varphi$ where - $$\begin{array}{rl} + $$\begin{array}{rlr} \neg\varphi & :=\ev\neg(a\ra(\neg b\un(a\wedge b)))\\ & :=\ev(a\wedge\neg(\neg b\un(a\wedge b)))\\ - & :=\ev(a\wedge(\al\neg b\vee - - + & :=\ev(a\wedge(\al\neg b\vee(\neg b\un(a\wedge b))))\\ + & :=\ev(a\wedge\al\neg b)\vee\ev(a\wedge(\neg b\un(a\wedge b)))\\ + & :=\ev(a\wedge\neg\ev b) & \ev(a\wedge(\neg b\un(a\wedge b)))\\ \end{array}$$ - Elementary sets: - $$\begin{array}{lll} - a & b & + Elementary sets for $\varphi=\ev(a\wedge\neg\ev b)$ where + $\psi=a\wedge\neg\ev b$: + $$\begin{array}{llll} + a & b & \varphi & \ev\psi\\ + a & b & \varphi & \ev\psi\\ \end{array}$$ \end{enumerate} \end{document} diff --git a/e41.smv b/e41.smv new file mode 100644 index 0000000..3cbf9c1 --- /dev/null +++ b/e41.smv @@ -0,0 +1,46 @@ +MODULE proc(i, s, yme, yother) +VAR + line: {l2, l3, l4, l7, l8}; +ASSIGN + init(line):=l2; + next(line):=case + line=l2: l3; + line=l3: l4; + line=l4: case + !(yother=0 | s!=i) : l4; + TRUE: l7; + esac; + line=l7: l8; + line=l8: l2; + esac; + +MODULE main +VAR + y0: 0..1; + y1: 0..1; + s: 0..1; + proc0: proc(0, s, y0, y1); + proc1: proc(1, s, y1, y0); +ASSIGN + next(y0):=case + proc0.line=l3: 1; + proc0.line=l8: 0; + TRUE: y0; + esac; + next(y1):=case + proc1.line=l3: 1; + proc1.line=l8: 0; + TRUE: y1; + esac; + next(s):=case + proc0.line=l3 & proc1.line=l3: {0,1}; + proc0.line=l3: 0; + proc1.line=l3: 1; + TRUE: s; + esac; + +--Mutual exclusion +LTLSPEC G(!(proc0.line=l7 & proc1.line=l7)) + +--Absence of starvation +LTLSPEC G (F(proc0.line=l7) & F(proc1.line=l7)) diff --git a/e42.smv b/e42.smv new file mode 100644 index 0000000..a142f73 --- /dev/null +++ b/e42.smv @@ -0,0 +1,76 @@ +MODULE phil(leftfork, rightfork) +VAR + state: {none, left, both}; +ASSIGN + init(state) := none; + next(state) := case + state=none: case + leftfork=inuse: none; + TRUE: left; + esac; + state=left: case + rightfork=inuse: left; + TRUE: both; + esac; + TRUE: none; + esac; + +MODULE main +VAR + f: array 0..6 of {free, inuse}; + ph0: phil(f[6], f[1]); + ph1: phil(f[0], f[2]); + ph2: phil(f[1], f[3]); + ph3: phil(f[2], f[4]); + ph4: phil(f[3], f[5]); + ph5: phil(f[4], f[6]); + ph6: phil(f[5], f[0]); +ASSIGN + init(f[0]):=free; + init(f[1]):=free; + init(f[2]):=free; + init(f[3]):=free; + init(f[4]):=free; + init(f[5]):=free; + init(f[6]):=free; + + next(f[0]) := case + ph6.state=both | ph1.state=left | ph0.state=both: inuse; + TRUE: free; + esac; + next(f[1]) := case + ph0.state=both | ph2.state=left | ph2.state=both: inuse; + TRUE: free; + esac; + next(f[2]) := case + ph1.state=both | ph3.state=left | ph3.state=both: inuse; + TRUE: free; + esac; + next(f[3]) := case + ph2.state=both | ph4.state=left | ph4.state=both: inuse; + TRUE: free; + esac; + next(f[4]) := case + ph3.state=both | ph5.state=left | ph5.state=both: inuse; + TRUE: free; + esac; + next(f[5]) := case + ph4.state=both | ph6.state=left | ph6.state=both: inuse; + TRUE: free; + esac; + next(f[6]) := case + ph5.state=both | ph0.state=left | ph0.state=both: inuse; + TRUE: free; + esac; +LTLSPEC F( + G(ph0.state=left) | + G(ph1.state=left) | + G(ph2.state=left) | + G(ph3.state=left) | + G(ph4.state=left) | + G(ph5.state=left) | + G(ph6.state=left)) +--LTLSPEC G( +-- (F (ph0.state=both)) & (F (ph1.state=both)) & (F (ph2.state=both)) & +-- (F (ph3.state=both)) & (F (ph4.state=both)) & (F (ph5.state=both)) & +-- (F (ph6.state=both)))