Report explains ProMeLa code and all LTLs

ReversalModel/run.sh

@@ -6,7 +6,7 @@ SCRIPT_DIR=$(cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd)
 
 cc="gcc-13"
 
-if [ "$#" -ne 54]; then
+if [ "$#" -ne 4 ]; then
     echo "$0: [ltl-prop] [n] [length] [r]" > /dev/stderr
     exit 1
 fi
@@ -19,6 +19,8 @@ compile_dir="$(mktemp -d)"
 cp "$SCRIPT_DIR/reversal.pml.m4" "$compile_dir"
 cd "$compile_dir"
 
+echo "Compiling in: $compile_dir"
+
 m4 -DN="$2" -DLENGTH="$3" -DR="$4" -DLTL="$1" reversal.pml.m4 > "$filename"
 spin -a "$filename"
 "$cc" -Wno-format-overflow -o "$pan_name" pan.c

report.tex

@@ -3,7 +3,7 @@
 \usepackage{algpseudocode}
 \usepackage[utf8]{inputenc}
 \usepackage[english]{babel}
-\usepackage[margin=2.25cm]{geometry}
+\usepackage[margin=2cm,bottom=3cm]{geometry}
 \usepackage{hyperref}
 \usepackage{listings}
 \usepackage{xcolor}
@@ -140,22 +140,25 @@ bool seq_eq_to_parallel = true;
 reverser store the reversed array. The \texttt{done} array stores an array of
 boolean values: \mintinline{c}{done[0]} stores whether the sequential reverser
 has terminated, and each \mintinline{c}{done[i]} for $1 \leq i \leq N$ stores
-whether the i-th spawned thread of the parallel reverser has terminated
-(consequently, since threads are joined in order, when \mintinline{c}{done[N] == true} the parallel reverser terminates). Finally 
+whether the i-th spawned thread of the parallel reverser has terminated.
+Consequently, since threads are joined in order, when 
+\mintinline{c}{done[N] == true} the parallel reverser terminates, an effect that
+is exploited by the main model body implementation to wait for it. Finally
 \texttt{seq\_eq\_to\_parallel} is set to \mintinline{c}{false} when an
 incongruence between \texttt{reversed\_seq} and \texttt{reversed\_par} is found
-after termination of both reversers.
+after termination of
+both reversers.
 
 The body of the model is structured in the following way: 
 
-\begin{minted}{c}
+\begin{minted}{kotlin}
 init {
     { /* array initialization */ }
 
     /* sequential reverser algorithm */
     run SequentialReverser();
     /* parallel reverser algorithm */
-    run ParallelReverser()
+    run ParallelReverser();
 
     (done[0] == true && done[N] == true);
 
@@ -163,12 +166,16 @@ init {
 }
 \end{minted}
 
-{\color{red}TODO: FIX EXPLAINATION TO REFLECT USE OF PROCTYPE}
-
 Each of the enumerated sections is surrounded by curly braces to emulate the
 effect of locally scoped variables in procedures, which do not exist in
 \textit{ProMeLa} aside the concurrency emulating \texttt{proctype} construct.
 
+As requested by the assignment, the sequential and parallel reverser are
+implemented in a \texttt{proctype} and spawned in parallel in the model. The two
+\textit{ProMeLa} processes join before the congruence check thanks to an
+``expression'' statement waiting on the termination boolean array to signal that
+both reversers have finished doing their job.
+
 The array initialization is carried out as follows:
 
 \begin{minted}{c}
@@ -281,20 +288,97 @@ it is declared and set to a meaningful value in this block of the model.
 
 In this section I cover the LTL property definitions I included in the model.
 
-The following LTL property definition checks that once both reversers have
-terminated, the content of  
-
-\begin{minted}{c}
+\begin{minted}{scala}
 ltl seq_eq_parallel {
     [] (seq_eq_to_parallel == true)
 }
 \end{minted}
 
+This LTL property definition checks that once both reversers have terminated,
+the content of the respective reversed arrays they produce is the same. As
+discussed in the previous section, this variable can only turn to false during
+the execution of the congruence check and only if a pair of array elements of
+same index is indeed different. Therefore, if the program is correct, the value
+of the variable will always be true.
 
+Note that this property does not ensure
+termination of the program, at it relies on the congruence check to eventually
+run at the end of the program. To ensure termination, I define the following LTL
+property:
+
+\begin{minted}{scala}
+ltl termination {
+    <> (done[0] == true && done[N] == true)
+}
+\end{minted}
+
+This mirrors the wait statement introduced in the model code before the
+congruence check block, and relies exactly in the same way on the termination
+boolean array. Note that the elements of the array can only turn from
+\mintinline{c}{false} to \mintinline{c}{true} or not change at all, thus the
+property in the ``eventually'' operator is actually always true after it becomes
+indeed true (i.e.\ the program cannnot un-terminate according to the model).
+
+I then define other two custom properties showcasing the powers of the
+M4 macro processor when compared to the built-in \textit{ProMeLa} one.
+
+\begin{minted}{scala}
+// ifelse(LTL, correctness_seq, `
+ltl correctness_seq {
+    [] (done[0] == true -> (true for(`k', 0, LENGTH-1, ` &&
+        r_s[eval(LENGTH - k - 1)] == a[k]')))
+}
+// ', `')
+\end{minted}
+
+This property checks if the array produced by the sequential reverser is indeed
+the reverse of the input array. Note that the ``polyglot'' M4 sugar allows for
+the property to be arbitrairly unraveled based on the value of \texttt{LENGTH}.
+Notice that to simplify the \textit{ProMeLa} source code to compile for long
+array lengths, thanks to the \texttt{ifelse} macro the property is omitted by M4
+when the property is not actually checked (because long LTL properties actually
+make the model fail to parse). Here is an example of the unravelled property for
+\mintinline{c}{LENGTH = 10}:
+
+\begin{minted}{scala}
+ltl correctness_seq {
+    [] (done[0] == true -> (true  &&
+        r_s[9] == a[0] &&
+        r_s[8] == a[1] &&
+        r_s[7] == a[2] &&
+        r_s[6] == a[3] &&
+        r_s[5] == a[4] &&
+        r_s[4] == a[5] &&
+        r_s[3] == a[6] &&
+        r_s[2] == a[7] &&
+        r_s[1] == a[8] &&
+        r_s[0] == a[9]))
+}
+\end{minted}
+
+Note that the use of \mintinline{c}{true} as the first condition after the
+implication is simply to allow for \mintinline{c}{&&} to be simply appended at
+the start of each condition.
+
+In a similar fashion, I also define a property that is not generally true. The
+following LTL formula specifies that when the second thread of the parallel
+reverser terminates, the section to be reversed by the first thread is already
+reversed.
+
+\begin{minted}{scala}
+// ifelse(LTL, correctness_par, `
+ltl correctness_par {
+    [] (done[2] == true -> (true for(`k', 0, LENGTH / N - 1, ` &&
+        r_p[eval(LENGTH - k - 1)] == a[k]')))
+}
+// ', `')
+\end{minted}
+
+This property is clearly not generally true as the first thread may not complete
+the reversal process before the second thread terminates due to concurrency.
 
 
 The citation \cite{tange_2023_7855617}.
-The citation \cite{spin}.
 
 
 \begin{figure}