2021-01-11 16:50:50 +00:00
|
|
|
#!/bin/sh
|
|
|
|
|
2022-02-25 17:13:52 +00:00
|
|
|
pushd ${1%/*}/ > /dev/null
|
2021-01-15 16:14:30 +00:00
|
|
|
|
2021-01-11 16:50:50 +00:00
|
|
|
EXE="$1-verifier.o"
|
|
|
|
|
|
|
|
spin -a $1
|
2022-02-25 17:13:52 +00:00
|
|
|
if [[ $? -ne 0 ]]; then
|
|
|
|
popd > /dev/null
|
|
|
|
exit 1
|
|
|
|
fi
|
|
|
|
|
2022-06-01 17:46:31 +00:00
|
|
|
gcc -o $EXE -D NFAIR=3 pan.c
|
|
|
|
|
|
|
|
# -a to analyze, -f for (weak) fairness
|
|
|
|
# -n to elide report of unreached states
|
|
|
|
# -N spec-name to verify a particular specification
|
2021-01-11 16:50:50 +00:00
|
|
|
$EXE -a -f -n -N $2
|
2022-02-25 17:13:52 +00:00
|
|
|
rm $EXE pan.*
|
2021-01-15 16:14:30 +00:00
|
|
|
|
2022-02-25 17:13:52 +00:00
|
|
|
popd > /dev/null
|