report conclusions

Reversal/run.dat

@@ -1 +1,2 @@
 U28gbG9uZywgYW5kIHRoYW5rcyBmb3IgYWxsIHRoZSBmaXNoIQpodHRwczovL3lvdXR1LmJlL3JUZ2E0MXIzYTRz
+WW91IGhhdmUgdW5sb2NrZWQgdGhlIHNlY3JldCBlbmRpbmcKaHR0cHM6Ly95b3V0dS5iZS9DNW9lV0huZ0RTNA==

ReversalModel/run.sh

@@ -21,7 +21,7 @@ if [ "$1" == "all" ]; then
         printf "\033[36m>>> Checking LTL property: $ltl\033[0m\n"
         "$0" "$ltl" "$2" "$3" "$4"
     done
-    printf "\033[41m$(cat "$SCRIPT_DIR/../Reversal/run.dat" | base64 -d)\033[0m\n"
+    printf "\033[41m$(head -n 1 "$SCRIPT_DIR/../Reversal/run.dat" | base64 -d)\033[0m\n"
     exit 0
 fi
 
@@ -53,6 +53,10 @@ if [ -f "$filename.trail" ]; then
     "./$pan_name" -S -N "$1" "$filename.trail"
 fi
 
+if [[ ! -f "$filename.trail" && "$1" == "correctness_par" ]]; then
+    printf "\033[41m$(tail -n 1 "$SCRIPT_DIR/../Reversal/run.dat" | base64 -d)\033[0m\n"
+fi
+
 cd "$SCRIPT_DIR"
 rm -rf "$compile_dir"
 

report.tex

@@ -404,10 +404,61 @@ in the Java program.
 
 \section{Model Execution}
 
+To compile and check all LTL properties included in the model execute the
+command:
 
+\begin{minted}{shell}
+./ReversalModel/run.sh all $N $LENGTH $R
+\end{minted}
 
-The citation \cite{tange_2023_7855617}.
+from the root git directory of the assignment, where \mintinline{shell}{$N} is
+the value of the variable $N$, \mintinline{shell}{$LENGTH} is the length of the
+array and \mintinline{shell}{$R} is the value of $R$. The parameter \texttt{all}
+can be replaced by the name of an LTL property to only check the model for that
+property.
 
+\subsection{Execution limits}
+
+To better gauge the efficiency of the model checker algorithm, I run the model
+to check the LTL property \texttt{seq\_eq\_parallel} for all possible
+combinations of the values of $N \in [2,10]$, $\text{LENGTH} \in [3,10]$ and $R
+\in [2,10]$. The script \texttt{ReversalModel/grid-search.sh} implements this
+procedure with the following GNU Parallel \cite{tange_2023_7855617} command,
+allowing for parallel execution of up to 4 model instances:
+
+\begin{minted}[breaklines]{shell}
+parallel --jobs 4 "$SCRIPT_DIR/test-property.sh" ::: "$prop" ::: "$(seq 2 10)" ::: "$(seq 3 10)" ::: "$(seq 2 10)" ::: "$SCRIPT_DIR/$time_out"
+\end{minted}
+
+The \texttt{test-property.sh} script times out the model execution after 5
+minutes of \texttt{real} execution time due to time constraints. Thus, for each
+combination of parameters, I measure the process time (\texttt{user} and
+\texttt{sys} time) it takes to verify the LTL property and, if the execution
+times out, whether this happens or not. I then summarize the execution times for
+successful runs and the frequency of timeouts grouping the execution by each
+variable in figure \ref{fig:bigplot}.
+
+It is apparent that even small increases in the array length significantly
+hinder the performance of the model checking algorithm and increasee the number
+of timeouts. Increasing the number of processes $N$ instead shows a tamer effect
+on execution time, and avoids a significantly greater number of timeouts for the
+values 8, 9, and 10. Finally, increasing upper bound on the values of the array
+($R$) has the least significant effect, albeit being a close second to the
+distribution for $N$.
+
+\section{Conclusions}
+
+I find the Spin model checker a relatively straightforward tool to use. The 
+\textit{ProMeLa} model implementation was easy to carry out due to syntax
+similarities with C, and no tweaks were required after writing it to make the
+model work.
+
+The model manages to realistic model program behaviour of the Java reverser
+implementations, the moder checker did not flag any surprising behaviour w.r.t.\ 
+my understanding of the original code. It is however interesting that the
+\texttt{correctness\_par} property was invaidated with such an effective
+counterexample, and it shows the value of the tool for analysis of (albeit
+simple) concurrent program behaviour.
 
 \begin{figure}
 \begin{subfigure}[t]{\linewidth}