Promela refinement

ReversalModel/reversal.pml

@@ -1,30 +1,29 @@
-#define N 10
+#define N 2
 #define LENGTH 3
 #define R 2
 
 int to_reverse[LENGTH]; // array to reverse
 int reversed[LENGTH]; // array where the reverse is stored
 
-mtype = { END };
+// stores termination of each pid
+bool done[N]; // initialized to false
 
 // ThreadedReverser implementation
-proctype ThreadedReverser(int from; int to; chan out) {
+proctype ThreadedReverser(int from; int to; int n) {
     printf("proc[%d]: started\n", _pid);
     
     int k;
     for (k: from .. to) {
+        printf("reversed[%d] = to_reverse[%d]\n", LENGTH - k - 1, k);
         reversed[LENGTH - k - 1] = to_reverse[k];
     }
 
-    printf("proc[%d]: ended\n", _pid);
-    
-end:
-    out!_pid;
+    printf("proc[%d]: ended\n", n);
+    done[n] = true;
 }
 
 init {
-    chan in = [N] of { mtype };
-
+    printf("program start\n");
     // array initialization
     {
         int i;
@@ -32,36 +31,35 @@ init {
             int value;
             select(value: 0 .. R);
             to_reverse[i] = value;
+            printf("to_reverse[%d]: %d\n", i, value);
         }
     }
 
     // ParallelReverser implementation
     int n;
     int s = LENGTH / N;
-
-    pid pids[N];
     
     // fork section
-    for (n: 0 .. N) {
+    for (n: 0 .. (N - 1)) {
         int from = n * s;
         int to;
         if
-        :: (n == N - 1) -> to = LENGTH;
-        :: else -> to = n * s + s; 
+        :: (n == N - 1) -> to = LENGTH - 1;
+        :: else -> to = n * s + s - 1; 
         fi
-        pids[n] = run ThreadedReverser(from, to, in);
+        run ThreadedReverser(from, to, n);
     }
 
     // join section
-    for (n: 0 .. N) {
-        in??eval(pids[n]);
+    for (n: 0 .. (N - 1)) {
+        (done[n] == true);
+        printf("init: joined process %d\n", n);
+    }
 
-        printf("init: joined process %d\n", pids[n]);
-    }    
+    printf("program end\n");
 }
 
 // ltl syntax: https://spinroot.com/spin/Man/ltl.html
-ltl test { 
-    eventually (false) implies true
-//   eventually (a > b) implies len(q) == 0 
+ltl test {
+    (done[N - 1] == false) U (reversed[LENGTH - 1] == to_reverse[0])
 }

ReversalModel/verify.sh

@@ -10,7 +10,7 @@ fi
 set -e
 
 spin -a reversal.pml
-gcc-13 -Wno-format-overflow -o pan pan.c
+gcc-13 -Wno-format-overflow -DPRINTF -o pan pan.c
 ./pan -a "$1"
 
 exitcode="$?"