move everything out of trunk

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

diff --git a/trunk/verif/Spin/Test/leader2 b/trunk/verif/Spin/Test/leader2
deleted file mode 100755 (executable)
index 40f2ec3..0000000
--- a/trunk/verif/Spin/Test/leader2
+++ /dev/null
@@ -1,130 +0,0 @@
-/* Dolev, Klawe & Rodeh for leader election in unidirectional ring
- * `An O(n log n) unidirectional distributed algorithm for extrema
- * finding in a circle,'  J. of Algs, Vol 3. (1982), pp. 245-260
-
- * Randomized initialization added -- Feb 17, 1997
- */
-
-#define elected                (nr_leaders >  0)
-#define noLeader       (nr_leaders == 0)
-#define oneLeader      (nr_leaders == 1)
-
-/* sample properties:
- *     ![] noLeader
- *     <>  elected
- *     <>[]oneLeader
- *     [] (noLeader U oneLeader)
- */
-
-byte nr_leaders = 0;
-
-#define N      5       /* number of processes in the ring */
-#define L      10      /* 2xN */
-byte I;
-
-mtype = { one, two, winner };
-chan q[N] = [L] of { mtype, byte};
-
-proctype node (chan in, out; byte mynumber)
-{      bit Active = 1, know_winner = 0;
-       byte nr, maximum = mynumber, neighbourR;
-
-       xr in;
-       xs out;
-
-       printf("MSC: %d\n", mynumber);
-       out!one(mynumber);
-end:   do
-       :: in?one(nr) ->
-               if
-               :: Active -> 
-                       if
-                       :: nr != maximum ->
-                               out!two(nr);
-                               neighbourR = nr
-                       :: else ->
-                               know_winner = 1;
-                               out!winner,nr;
-                       fi
-               :: else ->
-                       out!one(nr)
-               fi
-
-       :: in?two(nr) ->
-               if
-               :: Active -> 
-                       if
-                       :: neighbourR > nr && neighbourR > maximum ->
-                               maximum = neighbourR;
-                               out!one(neighbourR)
-                       :: else ->
-                               Active = 0
-                       fi
-               :: else ->
-                       out!two(nr)
-               fi
-       :: in?winner,nr ->
-               if
-               :: nr != mynumber ->
-                       printf("MSC: LOST\n");
-               :: else ->
-                       printf("MSC: LEADER\n");
-                       nr_leaders++;
-                       assert(nr_leaders == 1)
-               fi;
-               if
-               :: know_winner
-               :: else -> out!winner,nr
-               fi;
-               break
-       od
-}
-
-init {
-       byte proc;
-       byte Ini[6];    /* N<=6 randomize the process numbers */
-       atomic {
-
-               I = 1;  /* pick a number to be assigned 1..N */
-               do
-               :: I <= N ->
-                       if      /* non-deterministic choice */
-                       :: Ini[0] == 0 && N >= 1 -> Ini[0] = I
-                       :: Ini[1] == 0 && N >= 2 -> Ini[1] = I
-                       :: Ini[2] == 0 && N >= 3 -> Ini[2] = I
-                       :: Ini[3] == 0 && N >= 4 -> Ini[3] = I
-                       :: Ini[4] == 0 && N >= 5 -> Ini[4] = I
-                       :: Ini[5] == 0 && N >= 6 -> Ini[5] = I  /* works for up to N=6 */
-                       fi;
-                       I++
-               :: I > N ->     /* assigned all numbers 1..N */
-                       break
-               od;
-
-               proc = 1;
-               do
-               :: proc <= N ->
-                       run node (q[proc-1], q[proc%N], Ini[proc-1]);
-                       proc++
-               :: proc > N ->
-                       break
-               od
-       }
-}
-
-#if 0
-
-/* !(<>[]oneLeader) -- a sample LTL property */
-
-never {
-T0:
-        if
-        :: skip -> goto T0
-        :: !oneLeader -> goto accept
-        fi;
-accept:
-        if
-        :: skip -> goto T0
-        fi
-}
-#endif