From 03b9678956cef4bfefb4fd76ab72d48ab5a4dae9 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 1 Mar 2016 21:06:50 +0100
Subject: [PATCH] started with 4

---
 .gitignore |  2 ++
 e3.tex     | 17 +++++++-----
 e41.smv    | 46 +++++++++++++++++++++++++++++++++
 e42.smv    | 76 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 134 insertions(+), 7 deletions(-)
 create mode 100644 e41.smv
 create mode 100644 e42.smv

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)))
-- 
2.20.1