nico and md model

[lttv.git] / trunk / verif / md / pan.otl

diff --git a/trunk/verif/md/pan.otl b/trunk/verif/md/pan.otl
new file mode 100644 (file)
index 0000000..37e2edf
--- /dev/null
+++ b/trunk/verif/md/pan.otl
@@ -0,0 +1,32 @@
+#define p      (write_off - read_off >= 0)
+#define q      (write_off - read_off < HALF_UCHAR)
+
+       /*
+        * Formula As Typed: [] (p && q)
+        * The Never Claim Below Corresponds
+        * To The Negated Formula !([] (p && q))
+        * (formalizing violations of the original)
+        */
+
+never {    /* !([] (p && q)) */
+T0_init:
+       if
+       :: (((! ((p))) || (! ((q))))) -> goto accept_all
+       :: (1) -> goto T0_init
+       fi;
+accept_all:
+       skip
+}
+
+#ifdef NOTES
+Use Load to open a file or a template.
+#endif
+#ifdef RESULT
+warning: for p.o. reduction to be valid the never claim must be stutter-invariant
+(never claims generated from LTL formulae are stutter-invariant)
+depth 0: Claim reached state 5 (line 321)
+Running verification -- waiting for output
+       (kill background process 'pan' to abort run)
+       (use /bin/ps to find pid; then: kill -2 pid)
+
+#endif