From 4f00be95f582e8c377cc5f453f154158ea3596b7 Mon Sep 17 00:00:00 2001
From: Claudio Maggioni <maggicl@usi.ch>
Date: Mon, 8 May 2023 14:31:13 +0200
Subject: [PATCH] ProMeLa implementation (excl. ltl) done

---
 ReversalModel/reversal.pml | 37 +++++++++++++++++++++++--------------
 1 file changed, 23 insertions(+), 14 deletions(-)

diff --git a/ReversalModel/reversal.pml b/ReversalModel/reversal.pml
index efb3aa2..c75a667 100644
--- a/ReversalModel/reversal.pml
+++ b/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