move everything out of trunk

[lttv.git] / trunk / verif / examples / spin-increment.spin

diff --git a/trunk/verif/examples/spin-increment.spin b/trunk/verif/examples/spin-increment.spin
deleted file mode 100644 (file)
index b308fb5..0000000
--- a/trunk/verif/examples/spin-increment.spin
+++ /dev/null
@@ -1,40 +0,0 @@
-#define NUMPROCS 2
-
-byte counter = 0;
-byte progress[NUMPROCS];
-
-proctype incrementer(byte me)
-{
-  int temp;
-
-  temp = counter;
-  counter = temp + 1;
-  progress[me] = 1;
-}
-
-init {
-  int i = 0;
-  int sum = 0;
-
-  atomic {
-    i = 0;
-    do
-    :: i < NUMPROCS ->
-      progress[i] = 0;
-      run incrementer(i);
-      i++
-    :: i >= NUMPROCS -> break
-    od;
-  }
-  atomic {
-    i = 0;
-    sum = 0;
-    do
-    :: i < NUMPROCS ->
-      sum = sum + progress[i];
-      i++
-    :: i >= NUMPROCS -> break
-    od;
-    assert(sum < NUMPROCS || counter == NUMPROCS)
-  }
-}