diff --git a/ReversalModel/run.sh b/ReversalModel/run.sh
index 57ca88c..81dd518 100755
--- a/ReversalModel/run.sh
+++ b/ReversalModel/run.sh
@@ -4,7 +4,11 @@ set -e
 
 SCRIPT_DIR=$(cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd)
 
-cc="gcc-13"
+if [ "$(uname)" = "Darwin" ]; then
+    cc="$(find /usr/local/bin -name 'gcc-*' | head -n 1)"
+else
+    cc="gcc"
+fi
 
 
 if [ "$#" -ne 4 ]; then
@@ -12,11 +16,21 @@ if [ "$#" -ne 4 ]; then
     exit 1
 fi
 
+if [ "$1" == "all" ]; then
+    for ltl in seq_eq_parallel termination correctness_seq correctness_par; do
+        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"
+    exit 0
+fi
+
 id="${1}_${2}_${3}_${4}"
 filename="reversal_$id.pml"
 pan_name="pan_$id"
 
 compile_dir="$(mktemp -d)"
+echo "Compiling and running in: $compile_dir"
 cp "$SCRIPT_DIR/reversal.pml.m4" "$compile_dir"
 cd "$compile_dir"
 
@@ -35,12 +49,10 @@ spin -a "$filename"
 
 # Execute trail if check fails
 if [ -f "$filename.trail" ]; then
-    echo "FAILED" >> /dev/stderr
+    echo -e "\033[31mVerification FAILED! Counterexample trace follows:\033[0m"
     "./$pan_name" -S -N "$1" "$filename.trail"
 fi
 
 cd "$SCRIPT_DIR"
-echo "Compiling in: $compile_dir"
 rm -rf "$compile_dir"
 
-printf "\033[41m$(cat "$SCRIPT_DIR/../Reversal/run.dat" | base64 -d)\033[0m\n"
diff --git a/report.tex b/report.tex
index 89cea15..28d7f30 100644
--- a/report.tex
+++ b/report.tex
@@ -90,7 +90,7 @@ This report covers the definition of the model to check and the necessary LTL
 properties to verify correctness of the implementation, and additionally
 presents a brief analysis on the performance of the automated model checker.
 
-\section{Model definition}
+\section{Model Definition}
 
 In this section I define the \textit{ProMeLa} code which implements a FSA model
 of the Java implementation. The model I define does not match the exact provided
@@ -402,6 +402,8 @@ manage to execute \mintinline{c}{r_p[2] = a[0]} before the second thread
 terminates. Indeed, this is a realistic counterexample that could be reproduced
 in the Java program.
 
+\section{Model Execution}
+
 
 
 The citation \cite{tange_2023_7855617}.
diff --git a/start-docker.sh b/start-docker.sh
new file mode 100755
index 0000000..cff3ab2
--- /dev/null
+++ b/start-docker.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
+docker run --rm -it -v "${SCRIPT_DIR}:/tools/home" bugcounting/satools:y23
+