diff --git a/TESTING.md b/TESTING.md index e0abb66..1c99d4b 100644 --- a/TESTING.md +++ b/TESTING.md @@ -12,10 +12,10 @@ pip install z3-solver pytest ## Running all tests ``` -bash tests/run_all_tests.sh +./run_tests.sh ``` -This runs both the BDD and SMT test suites in sequence. +This runs the BDD, SMT, and generator test suites in sequence. ## BDD tests @@ -53,3 +53,13 @@ python3 -m pytest tests/test_smt.py -v concentrations (chain reaction, heat shock response) - **SmtCheckerRSCParam** -- parametric verification - **RSC-to-RS translation** -- verifying the translated system + +## Generator tests + +7 tests that run each generator (from `examples/bdd/generators/`), +feed the output into the BDD model checker, and verify the expected +verification result (holds / does not hold). + +Generators using old syntax (`examples/bdd/generators/old_syntax/`) +are not tested this way as they are not compatible with the current +parser. diff --git a/run_tests.sh b/run_tests.sh new file mode 100755 index 0000000..bc65fc7 --- /dev/null +++ b/run_tests.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +# Run all ReactICS tests (BDD, SMT, generators) +exec bash "$(dirname "$0")/tests/run_all_tests.sh" "$@" diff --git a/tests/run_all_tests.sh b/tests/run_all_tests.sh index 747d926..bbfa9d3 100755 --- a/tests/run_all_tests.sh +++ b/tests/run_all_tests.sh @@ -1,24 +1,82 @@ #!/usr/bin/env bash -# Runs all ReactICS regression tests (BDD + SMT) +# Runs all ReactICS regression tests (BDD + SMT + generators) + +set -uo pipefail SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" ROOT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)" +REACTICS="$ROOT_DIR/reactics-bdd/reactics" +GENERATORS="$ROOT_DIR/examples/bdd/generators" cd "$ROOT_DIR" failed=0 +# --------------------------------------------------------------- echo "========== BDD Tests ==========" echo bash "$SCRIPT_DIR/run_tests.sh" || failed=1 +# --------------------------------------------------------------- echo echo "========== SMT Tests (pytest) ==========" echo python3 -m pytest "$SCRIPT_DIR/test_smt.py" -v || failed=1 +# --------------------------------------------------------------- echo +echo "========== Generator Tests ==========" +echo + +gen_pass=0 +gen_fail=0 + +check_gen() { + local name="$1" + local gen_cmd="$2" + local property="$3" + local expected="$4" + + local tmpfile + tmpfile=$(mktemp /tmp/reactics_gen_XXXXXX.drs) + + eval "$gen_cmd" > "$tmpfile" 2>&1 + local result + result=$("$REACTICS" -c "$property" "$tmpfile" 2>&1 | grep -oE "(holds|does not hold)" || true) + rm -f "$tmpfile" + + if [[ "$result" == "$expected" ]]; then + echo " PASS: $name" + ((gen_pass++)) + else + echo " FAIL: $name (expected '$expected', got '$result')" + ((gen_fail++)) + failed=1 + fi +} + +echo "[gen_tgc]" +check_gen "tgc(3) f1" "python3 $GENERATORS/gen_tgc.py 3" f1 "holds" +check_gen "tgc(3) f3" "python3 $GENERATORS/gen_tgc.py 3" f3 "holds" +check_gen "tgc(4) f2" "python3 $GENERATORS/gen_tgc.py 4" f2 "holds" + +echo +echo "[gen_asm]" +check_gen "asm(3) f1" "python3 $GENERATORS/gen_asm.py 3" f1 "holds" +check_gen "asm(3) f2" "python3 $GENERATORS/gen_asm.py 3" f2 "holds" + +echo +echo "[gen_drs]" +check_gen "drs(2,2,2,a) f0" "python3 $GENERATORS/gen_drs.py 2 2 2 a" f0 "does not hold" +check_gen "drs(2,2,2,b) f0" "python3 $GENERATORS/gen_drs.py 2 2 2 b" f0 "holds" + +echo +echo "Generator results: $gen_pass passed, $gen_fail failed" + +# --------------------------------------------------------------- +echo +echo "================================" if [[ $failed -eq 0 ]]; then echo "All test suites passed." else