update

[master.git] / ar / assignments / 4a.smv

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