63 lines
1.5 KiB
Bash
Executable File
63 lines
1.5 KiB
Bash
Executable File
#!/bin/bash
|
|
|
|
set -e
|
|
|
|
SCRIPT_DIR=$(cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd)
|
|
|
|
if [ "$(uname)" = "Darwin" ]; then
|
|
cc="$(find /usr/local/bin -name 'gcc-*' | head -n 1)"
|
|
else
|
|
cc="gcc"
|
|
fi
|
|
|
|
|
|
if [ "$#" -ne 4 ]; then
|
|
echo "$0: [ltl-prop] [n] [length] [r]" > /dev/stderr
|
|
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$(head -n 1 "$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"
|
|
|
|
echo "Compiling in: $compile_dir"
|
|
|
|
if [ "$PRINTF" == "true" ]; then
|
|
defs="-DPRINTF "
|
|
else
|
|
defs=""
|
|
fi
|
|
|
|
m4 -DN="$2" -DLENGTH="$3" -DR="$4" -DLTL="$1" reversal.pml.m4 > "$filename"
|
|
spin -a "$filename"
|
|
"$cc" -Wno-format-overflow $defs -o "$pan_name" pan.c
|
|
"./$pan_name" -a -N "$1"
|
|
|
|
# Execute trail if check fails
|
|
if [ -f "$filename.trail" ]; then
|
|
echo -e "\033[31mVerification FAILED! Counterexample trace follows:\033[0m"
|
|
"./$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"
|
|
|