From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 1 Mar 2016 20:27:32 +0000 (+0100)
Subject: up
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;ds=inline;p=mc1516.git

up
---

diff --git a/e42.smv b/e42.smv
index 91f16e7..c227d2a 100644
--- a/e42.smv
+++ b/e42.smv
@@ -6,14 +6,17 @@ ASSIGN
 	next(state) := case
 		state=none: case
 			leftfork=inuse: none;
-			TRUE: left;
+			TRUE: {none, left};
 		esac;
 		state=left: case
-			rightfork=inuse: left;
-			TRUE: both;
+--			rightfork=inuse: left;
+			rightfork=inuse: {none, left};
+--			TRUE: {left, both};
+			TRUE: {none, left, both};
 		esac;
 		TRUE: none;
 	esac;
+JUSTICE state=both
 
 MODULE main
 VAR
@@ -62,15 +65,22 @@ ASSIGN
 		next(ph5.state)=both | next(ph0.state)=left | next(ph0.state)=both: inuse;
 		TRUE: free;
 	esac;
+--This finds a deadlock
 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)))
+	ph0.state=left &
+	ph1.state=left &
+	ph2.state=left &
+	ph3.state=left &
+	ph4.state=left &
+	ph5.state=left &
+	ph6.state=left)
+
+--Checks starvation
+CTLSPEC AG(
+	(EF (ph0.state=both)) &
+	(EF (ph1.state=both)) &
+	(EF (ph2.state=both)) &
+	(EF (ph3.state=both)) &
+	(EF (ph4.state=both)) &
+	(EF (ph5.state=both)) &
+	(EF (ph6.state=both)))