remove files unneeded for lttv

[lttv.git] / verif / Spin / Test / petersonN

diff --git a/verif/Spin/Test/petersonN b/verif/Spin/Test/petersonN
deleted file mode 100755 (executable)
index 1cccdb5..0000000
--- a/verif/Spin/Test/petersonN
+++ /dev/null
@@ -1,45 +0,0 @@
-/* Peterson's algorithm for N processes - see Lynch's book, p. 284 */
-
-#ifndef N
-       #define N       3       /* nr of processes */
-#endif
-
-byte turn[N], flag[N];
-
-byte ncrit;    /* auxiliary var to check mutual exclusion */
-
-active [N] proctype user()
-{      byte j, k;
-       /* without never claims, _pid's are: 0 .. N-1 */
-again:
-       k = 0;  /* count max N-1 rounds of competition */
-       do
-       :: k < N-1 ->
-               flag[_pid] = k;
-               turn[k] = _pid;
-
-               j = 0;          /* for all j != _pid */
-               do
-               :: j == _pid ->
-                       j++
-               :: j != _pid ->
-                       if
-                       :: j < N ->
-                               (flag[j] < k || turn[k] != _pid);
-                               j++
-                       :: j >= N  ->
-                               break
-                       fi
-               od;
-               k++
-       :: else ->      /* survived all N-1 rounds */
-               break
-       od;
-
-       ncrit++;
-       assert(ncrit == 1);     /* critical section */
-       ncrit--;
-
-       flag[_pid] = 0;
-       goto again
-}