From be174d923a8fbf2326674c02e751bc88958b3927 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 6 Oct 2015 12:58:28 +0200 Subject: [PATCH] update --- ar/assignments/4.smv | 48 +++++++++++++++++++++++++++++++++++++++ ar/assignments/marble.smv | 20 ++++++++++++++++ 2 files changed, 68 insertions(+) create mode 100644 ar/assignments/4.smv create mode 100644 ar/assignments/marble.smv 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) -- 2.20.1