ProMeLa implementation (excl. ltl) done

ReversalModel/reversal.pml

@@ -2,10 +2,18 @@
 #define LENGTH 3
 #define R 2
 
+int to_reverse[LENGTH]; // array to reverse
+int reversed[LENGTH]; // array where the reverse is stored
+
+// ThreadedReverser implementation
+proctype ThreadedReverser(int from; int to) {
+    int k;
+    for (k: from .. to) {
+        reversed[LENGTH - k - 1] = to_reverse[k];
+    } 
+}
 
 init {
-    int to_reverse[LENGTH];
-    
     // array initialization
     {
         int i;
@@ -16,20 +24,21 @@ init {
         }
     }
 
-    int reversed[LENGTH];
-
-    // sequential reverser
-    {
-        int from = 0;
-        int to = LENGTH ;
-        
-        int k;
-        for (k: from..to) {
-            reversed[LENGTH - k - 1] = to_reverse[k];
-        }
+    // ParallelReverser implementation
+    int n;
+    int s = LENGTH / N;
+    for (n: 0 .. N) {
+        int from = n * s;
+        int to;
+        if
+        :: (n == N - 1) -> to = LENGTH;
+        :: else -> to = n * s + s; 
+        fi
+        run ThreadedReverser(from, to);
     }    
 }
 
+// ltl syntax: https://spinroot.com/spin/Man/ltl.html
 ltl test { 
     eventually (false) implies true
 //   eventually (a > b) implies len(q) == 0