First LTL property implemented

ReversalModel/reversal.pml

@@ -3,10 +3,15 @@
 #define R 2
 
 int to_reverse[LENGTH]; // array to reverse
-int reversed[LENGTH]; // array where the reverse is stored
+int reversed_seq[LENGTH]; // for SequentialReverser: where the reverse is stored 
+int reversed_par[LENGTH]; // for ParallelReverser: where the reverse is stored
 
-// stores termination of each pid
+// stores termination of each reverser
-bool done[N]; // initialized to false
+// index 0 is for the sequential algorithm
+// indices 1-N are for the ThreadedReverser instances
+bool done[N + 1]; // initialized to false
+
+bool seq_eq_to_parallel = true;
 
 // ThreadedReverser implementation
 proctype ThreadedReverser(int from; int to; int n) {
@@ -14,8 +19,8 @@ proctype ThreadedReverser(int from; int to; int n) {
     
     int k;
     for (k: from .. to) {
-        printf("reversed[%d] = to_reverse[%d]\n", LENGTH - k - 1, k);
+        printf("reversed_par[%d] = to_reverse[%d]\n", LENGTH - k - 1, k);
-        reversed[LENGTH - k - 1] = to_reverse[k];
+        reversed_par[LENGTH - k - 1] = to_reverse[k];
     }
 
     printf("proc[%d]: ended\n", n);
@@ -35,31 +40,62 @@ init {
         }
     }
 
+    printf("sequential start\n");
+    // SequentialReverser implementation
+    {
+        int k;
+        for (k: 0 .. (LENGTH - 1)) {
+            reversed_par[LENGTH - k - 1] = to_reverse[k];
+            printf("reversed_seq[%d] = to_reverse[%d]\n", LENGTH - k - 1, k);
+        }
+        done[0] = true; // mark sequential end
+    }
+    printf("sequential end\n");
+
+    printf("parallel start\n");
     // ParallelReverser implementation
-    int n;
+    {
-    int s = LENGTH / N;
+        int n;
+        int s = LENGTH / N;
         
-    // fork section
+        // fork section
-    for (n: 0 .. (N - 1)) {
+        for (n: 1 .. N) {
-        int from = n * s;
+            int from = n * s;
-        int to;
+            int to;
-        if
+            if
-        :: (n == N - 1) -> to = LENGTH - 1;
+            :: (n == N - 1) -> to = LENGTH - 1;
-        :: else -> to = n * s + s - 1; 
+            :: else -> to = n * s + s - 1; 
-        fi
+            fi
-        run ThreadedReverser(from, to, n);
+            run ThreadedReverser(from, to, n); // run as "thread n"
+        }
+
+        // join section
+        for (n: 1 .. N) {
+            (done[n] == true); // wait "thread n"
+            printf("[%d] joined\n", n);
+        }
     }
+    printf("parallel end\n");
 
-    // join section
+    // test if seq and parallel are the same
-    for (n: 0 .. (N - 1)) {
+    {
-        (done[n] == true);
+        int i;
-        printf("init: joined process %d\n", n);
+        for (i: 0 .. (LENGTH - 1)) {
+            if
+            :: (reversed_seq[i] != reversed_par[i]) -> seq_eq_to_parallel = false;
+            fi
+        }
     }
-
-    printf("program end\n");
 }
 
 // ltl syntax: https://spinroot.com/spin/Man/ltl.html
-ltl test {
+
-    (done[N - 1] == false) U (reversed[LENGTH - 1] == to_reverse[0])
+ltl seq_eq_parallel {
+    // the variable seq_eq_to_parallel will never be false if all the elements
+    // between the sequential and parallel reversed arrays are equal
+    (done[0] == false || done[N] == false) U (seq_eq_to_parallel == true)
+}
+
+ltl termination {
+    <> (done[0] == true && done[N] == true)
 }

ReversalModel/verify.sh

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