maggicl/soft-an04
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Run script refined

Browse source
This commit is contained in:
Claudio Maggioni 2023-05-12 19:27:10 +02:00
parent 5c64f6dcbc
commit 38e04a2952
3 changed files with 24 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
ReversalModel/run.sh
View file

@ -4,7 +4,11 @@ set -e
SCRIPT_DIR=$(cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd) 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 if [ "$#" -ne 4 ]; then
@ -12,11 +16,21 @@ if [ "$#" -ne 4 ]; then
exit 1 exit 1
fi 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}" id="${1}_${2}_${3}_${4}"
filename="reversal_$id.pml" filename="reversal_$id.pml"
pan_name="pan_$id" pan_name="pan_$id"
compile_dir="$(mktemp -d)" compile_dir="$(mktemp -d)"
echo "Compiling and running in: $compile_dir"
cp "$SCRIPT_DIR/reversal.pml.m4" "$compile_dir" cp "$SCRIPT_DIR/reversal.pml.m4" "$compile_dir"
cd "$compile_dir" cd "$compile_dir"
@ -35,12 +49,10 @@ spin -a "$filename"
# Execute trail if check fails # Execute trail if check fails
if [ -f "$filename.trail" ]; then 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" "./$pan_name" -S -N "$1" "$filename.trail"
fi fi
cd "$SCRIPT_DIR" cd "$SCRIPT_DIR"
echo "Compiling in: $compile_dir"
rm -rf "$compile_dir" rm -rf "$compile_dir"
printf "\033[41m$(cat "$SCRIPT_DIR/../Reversal/run.dat" | base64 -d)\033[0m\n"

4
report.tex
View file

@ -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 properties to verify correctness of the implementation, and additionally
presents a brief analysis on the performance of the automated model checker. 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 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 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 terminates. Indeed, this is a realistic counterexample that could be reproduced
in the Java program. in the Java program.
\section{Model Execution}
The citation \cite{tange_2023_7855617}. The citation \cite{tange_2023_7855617}.

5
start-docker.sh Executable file
View file

@ -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