From f36a4faf3ca545644d3c859f8bc6592325fc33e9 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 1 Mar 2016 21:17:09 +0100
Subject: [PATCH] update phils

---
 e42.smv | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/e42.smv b/e42.smv
index a142f73..91f16e7 100644
--- a/e42.smv
+++ b/e42.smv
@@ -26,40 +26,40 @@ VAR
 	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;
+	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;
+		next(ph6.state)=both | next(ph1.state)=left | next(ph0.state)=both: inuse;
 		TRUE: free;
 	esac;
 	next(f[1]) := case
-		ph0.state=both | ph2.state=left | ph2.state=both: inuse;
+		next(ph0.state)=both | next(ph2.state)=left | next(ph2.state)=both: inuse;
 		TRUE: free;
 	esac;
 	next(f[2]) := case
-		ph1.state=both | ph3.state=left | ph3.state=both: inuse;
+		next(ph1.state)=both | next(ph3.state)=left | next(ph3.state)=both: inuse;
 		TRUE: free;
 	esac;
 	next(f[3]) := case
-		ph2.state=both | ph4.state=left | ph4.state=both: inuse;
+		next(ph2.state)=both | next(ph4.state)=left | next(ph4.state)=both: inuse;
 		TRUE: free;
 	esac;
 	next(f[4]) := case
-		ph3.state=both | ph5.state=left | ph5.state=both: inuse;
+		next(ph3.state)=both | next(ph5.state)=left | next(ph5.state)=both: inuse;
 		TRUE: free;
 	esac;
 	next(f[5]) := case
-		ph4.state=both | ph6.state=left | ph6.state=both: inuse;
+		next(ph4.state)=both | next(ph6.state)=left | next(ph6.state)=both: inuse;
 		TRUE: free;
 	esac;
 	next(f[6]) := case
-		ph5.state=both | ph0.state=left | ph0.state=both: inuse;
+		next(ph5.state)=both | next(ph0.state)=left | next(ph0.state)=both: inuse;
 		TRUE: free;
 	esac;
 LTLSPEC F(
-- 
2.20.1