From 5db40b6ce3ce91a870c49c4fae819eff421b202c Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 6 Oct 2015 21:11:26 +0200
Subject: [PATCH] update

---
 ar/assignments/4.smv  | 56 +++++++++++++------------------------------
 ar/assignments/4a.smv | 24 +++++++++++++++++++
 2 files changed, 40 insertions(+), 40 deletions(-)
 create mode 100644 ar/assignments/4a.smv

diff --git a/ar/assignments/4.smv b/ar/assignments/4.smv
index 2f84ac3..2f98101 100644
--- a/ar/assignments/4.smv
+++ b/ar/assignments/4.smv
@@ -1,48 +1,24 @@
 MODULE main
 VAR
-a1 : 0..100;
-a2 : 0..100;
-a3 : 0..100;
-a4 : 0..100;
-a5 : 0..100;
-a6 : 0..100;
-a7 : 0..100;
+a2 : 2..100;
+a3 : 3..100;
+a4 : 4..100;
+a5 : 5..100;
+a6 : 6..100;
 c : 0..25;
 INIT
-a1 = 1 & 
-a2 = 2 &
-a3 = 3 &
-a4 = 4 &
-a5 = 5 &
-a6 = 6 &
-a7 = 7 &
-c = 0
+a2 = 2 & a3 = 3 & a4 = 4 & a5 = 5 & a6 = 6 & c=1
 TRANS
-next(c) = c + 1 & (
-	next(a2) = a1+a3 |
-	next(a3) = a2+a4 |
-	next(a4) = a3+a5 |
-	next(a5) = a4+a6 |
-	next(a6) = a5+a7
+next(c)=c+1 & (
+	next(a2)=1+a3 |
+	next(a3)=a2+a4 |
+	next(a4)=a3+a5 |
+	next(a5)=a4+a6 |
+	next(a6)=a5+7
 )
 LTLSPEC G !(
-	c < 10 &
-	a2>50 & (
-		a2=a3 |
-		a2=a4 |
-		a2=a5 |
-		a2=a6
-	) |
-	a3>50 & (
-		a3=a4 |
-		a3=a5 |
-		a3=a6
-	) |
-	a4>50 & (
-		a4=a5 |
-		a4=a6
-	) |
-	a5>50 & (
-		a5=a6
-	)
+	(a2>=50) |
+	(a3>=50) |
+	(a4>=50) |
+	(a5>=50)
 )
diff --git a/ar/assignments/4a.smv b/ar/assignments/4a.smv
new file mode 100644
index 0000000..b88f231
--- /dev/null
+++ b/ar/assignments/4a.smv
@@ -0,0 +1,24 @@
+MODULE main
+VAR
+a2 : 2..65;
+a3 : 3..65;
+a4 : 4..65;
+a5 : 5..65;
+a6 : 6..65;
+c : 0..15;
+INIT
+a2 = 2 & a3 = 3 & a4 = 4 & a5 = 5 & a6 = 6 & c = 0
+TRANS
+next(c)=c+1 & (
+	next(a2)=1+a3 |
+	next(a3)=a2+a4 |
+	next(a4)=a3+a5 |
+	next(a5)=a4+a6 |
+	next(a6)=a5+7
+)
+LTLSPEC G !(
+	(a2>=50 & (a2=a3 | a2=a4 | a2=a5 | a2=a6)) |
+	(a3>=50 & (a3=a4 | a3=a5 | a3=a6)) |
+	(a4>=50 & (a4=a5 | a4=a6)) |
+	(a5>=50 & (a5=a6))
+)
-- 
2.20.1