From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 6 Oct 2015 10:58:28 +0000 (+0200)
Subject: update
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=be174d923a8fbf2326674c02e751bc88958b3927;p=master.git

update
---

diff --git a/ar/assignments/4.smv b/ar/assignments/4.smv
new file mode 100644
index 0000000..2f84ac3
--- /dev/null
+++ b/ar/assignments/4.smv
@@ -0,0 +1,48 @@
+MODULE main
+VAR
+a1 : 0..100;
+a2 : 0..100;
+a3 : 0..100;
+a4 : 0..100;
+a5 : 0..100;
+a6 : 0..100;
+a7 : 0..100;
+c : 0..25;
+INIT
+a1 = 1 & 
+a2 = 2 &
+a3 = 3 &
+a4 = 4 &
+a5 = 5 &
+a6 = 6 &
+a7 = 7 &
+c = 0
+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
+)
+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
+	)
+)
diff --git a/ar/assignments/marble.smv b/ar/assignments/marble.smv
new file mode 100644
index 0000000..d9845a8
--- /dev/null
+++ b/ar/assignments/marble.smv
@@ -0,0 +1,20 @@
+MODULE main
+VAR
+a : 0..100;
+c : 0..20;
+INIT
+a = 1 & c = 0
+TRANS
+case 
+	c<20 : next(c) = c+1;
+	TRUE : next(c) = c;
+esac & (
+case 
+	a<100 : next(a) = a+1;
+	TRUE : next(a)=a;
+esac |
+case
+	a<=50 : next(a) = 2*a;
+	TRUE : next(a)=a;
+esac)
+LTLSPEC G !(a = 100 & c = 8)