update

diff --git a/ar/assignments/4.smv b/ar/assignments/4.smv
new file mode 100644 (file)
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 (file)
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)