add formal verif

[lttv.git] / trunk / verif / Spin / Test / loops

diff --git a/trunk/verif/Spin/Test/loops b/trunk/verif/Spin/Test/loops
new file mode 100755 (executable)
index 0000000..1ed711d
--- /dev/null
+++ b/trunk/verif/Spin/Test/loops
@@ -0,0 +1,12 @@
+active proctype loop()
+{      byte a, b;
+
+       do
+       :: a = (a+1)%3;
+               if
+               :: b = 2*a; skip
+               :: b = 2*a; accept: skip
+               fi;
+progress:      b--
+       od
+}