move everything out of trunk

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

diff --git a/trunk/verif/md/pan.otl b/trunk/verif/md/pan.otl
deleted file mode 100644 (file)
index 37e2edf..0000000
--- a/trunk/verif/md/pan.otl
+++ /dev/null
@@ -1,32 +0,0 @@
-#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