From 6f31f57b32be666d0300e883e684b2c1aa0991f6 Mon Sep 17 00:00:00 2001
From: Claudio Maggioni <maggicl@usi.ch>
Date: Mon, 8 May 2023 16:15:17 +0200
Subject: [PATCH] First LTL property implemented

---
 ReversalModel/reversal.pml | 86 +++++++++++++++++++++++++++-----------
 ReversalModel/verify.sh    |  2 +-
 2 files changed, 62 insertions(+), 26 deletions(-)

diff --git a/ReversalModel/reversal.pml b/ReversalModel/reversal.pml
index 1fc66f4..0efde77 100644
--- a/ReversalModel/reversal.pml
+++ b/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
-bool done[N]; // initialized to false
+// stores termination of each reverser
+// 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);
-        reversed[LENGTH - k - 1] = to_reverse[k];
+        printf("reversed_par[%d] = to_reverse[%d]\n", LENGTH - k - 1, 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;
-    
-    // fork section
-    for (n: 0 .. (N - 1)) {
-        int from = n * s;
-        int to;
-        if
-        :: (n == N - 1) -> to = LENGTH - 1;
-        :: else -> to = n * s + s - 1; 
-        fi
-        run ThreadedReverser(from, to, n);
-    }
+    {
+        int n;
+        int s = LENGTH / N;
+        
+        // fork section
+        for (n: 1 .. N) {
+            int from = n * s;
+            int to;
+            if
+            :: (n == N - 1) -> to = LENGTH - 1;
+            :: else -> to = n * s + s - 1; 
+            fi
+            run ThreadedReverser(from, to, n); // run as "thread n"
+        }
 
-    // join section
-    for (n: 0 .. (N - 1)) {
-        (done[n] == true);
-        printf("init: joined process %d\n", n);
+        // join section
+        for (n: 1 .. N) {
+            (done[n] == true); // wait "thread n"
+            printf("[%d] joined\n", n);
+        }
     }
+    printf("parallel end\n");
 
-    printf("program end\n");
+    // test if seq and parallel are the same
+    {
+        int i;
+        for (i: 0 .. (LENGTH - 1)) {
+            if
+            :: (reversed_seq[i] != reversed_par[i]) -> seq_eq_to_parallel = false;
+            fi
+        }
+    }
 }
 
 // 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)
 }
\ No newline at end of file
diff --git a/ReversalModel/verify.sh b/ReversalModel/verify.sh
index 0dfd7d3..84bd5d2 100755
--- a/ReversalModel/verify.sh
+++ b/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="$?"