move everything out of trunk

[lttv.git] / trunk / verif / Spin / Test / leader.ltl

diff --git a/trunk/verif/Spin/Test/leader.ltl b/trunk/verif/Spin/Test/leader.ltl
deleted file mode 100755 (executable)
index 776c367..0000000
--- a/trunk/verif/Spin/Test/leader.ltl
+++ /dev/null
@@ -1,70 +0,0 @@
-#define elected                (nr_leaders >  0)
-#define noLeader       (nr_leaders == 0)
-#define oneLeader      (nr_leaders == 1)
-
-       /*
-        * Formula As Typed: <>[]oneLeader
-        * The Never Claim Below Corresponds
-        * To The Negated Formula !(<>[]oneLeader)
-        * (formalizing violations of the original)
-        */
-
-never {    /* !(<>[]oneLeader) */
-T0_init:
-       if
-       :: (1) -> goto T0_init
-       :: (! ((oneLeader))) -> goto accept_S5
-       fi;
-accept_S5:
-       if
-       :: (1) -> goto T0_init
-       fi;
-accept_all:
-       skip
-}
-
-#ifdef NOTES
-Some other properties:
-       ![] noLeader
-       <>  elected
-       [] (noLeader U oneLeader)
-
-
-
-
-
-
-#endif
-#ifdef RESULT
-warning: for p.o. reduction to be valid the never claim must be stutter-closed
-(never claims generated from LTL formulae are stutter-closed)
-(Spin Version 3.1.2 -- 14 March 1998)
-       + Partial Order Reduction
-
-Full statespace search for:
-       never-claim             +
-       assertion violations    + (if within scope of claim)
-       acceptance   cycles     + (fairness disabled)
-       invalid endstates       - (disabled by never-claim)
-
-State-vector 200 byte, depth reached 233, errors: 0
-     202 states, stored (402 visited)
-     281 states, matched
-     683 transitions (= visited+matched)
-      36 atomic steps
-hash conflicts: 0 (resolved)
-(max size 2^19 states)
-
-2.542  memory usage (Mbyte)
-
-unreached in proctype node
-       line 105, state 28, "out!two,nr"
-       (1 of 49 states)
-unreached in proctype :init:
-       (0 of 11 states)
-
-real 0.13
-user 0.04
-sys  0.09
-
-#endif