Proof of concept sequential reverser

.gitignore

@@ -0,0 +1,4 @@
+Examples
+**/pan.*
+**/pan
+*.tmp

ReversalModel/reversal.pml

@@ -0,0 +1,36 @@
+#define N 10
+#define LENGTH 3
+#define R 2
+
+
+init {
+    int to_reverse[LENGTH];
+    
+    // array initialization
+    {
+        int i;
+        for (i in to_reverse) {
+            int value;
+            select(value: 0 .. R);
+            to_reverse[i] = value;
+        }
+    }
+
+    int reversed[LENGTH];
+
+    // sequential reverser
+    {
+        int from = 0;
+        int to = LENGTH ;
+        
+        int k;
+        for (k: from..to) {
+            reversed[LENGTH - k - 1] = to_reverse[k];
+        }
+    }
+}
+
+ltl test { 
+    eventually (false) implies true
+//   eventually (a > b) implies len(q) == 0 
+}

ReversalModel/verify.sh

@@ -0,0 +1,23 @@
+#!/bin/bash
+
+if [ $# -ne 1 ]; then
+    echo "LTL property name required" > /dev/stderr
+    exit 1
+else
+    userid="$1"
+fi
+
+set -e
+
+spin -a reversal.pml
+gcc-13 -Wno-format-overflow -o pan pan.c
+./pan -a "$1"
+
+exitcode="$?"
+
+if [ "$exitcode" -ne 0 ]; then
+    echo "Terminated with status: $exitcode" > /dev/stderr
+    exit "$exitcode"
+else
+    echo "Terminated successfully"
+fi