Artur Meski
f0019619b3
- Minor codebase clean-up - Slight reorganisation of examples + tests so that we don't break stuff by accident - CI tests
66 lines
1.8 KiB
Markdown
66 lines
1.8 KiB
Markdown
# Testing ReactICS
|
|
|
|
## Prerequisites
|
|
|
|
- **BDD module**: compiled (`./reactics setup` or `make` in `reactics-bdd/`)
|
|
- **SMT module**: Python 3 with `z3-solver` and `pytest` installed
|
|
|
|
```
|
|
pip install z3-solver pytest
|
|
```
|
|
|
|
## Running all tests
|
|
|
|
```
|
|
./run_tests.sh
|
|
```
|
|
|
|
This runs the BDD, SMT, and generator test suites in sequence.
|
|
|
|
## BDD tests
|
|
|
|
```
|
|
bash tests/run_tests.sh
|
|
```
|
|
|
|
10 regression tests that run the compiled `reactics-bdd/reactics` binary
|
|
against example `.drs` files and compare output to saved baselines in
|
|
`tests/expected/`. Covers:
|
|
|
|
- Parsed system printing (`-P`)
|
|
- Reaction listing (`-r`)
|
|
- Reachable state enumeration (`-s`)
|
|
- RSCTLK model checking (`-c`) for properties f1--f4
|
|
|
|
Input files: `examples/bdd/tgc.drs`, `examples/bdd/tgc4.drs`,
|
|
`reactics-bdd/in/trivial.drs`.
|
|
|
|
To update baselines after an intentional output change, delete the
|
|
relevant file in `tests/expected/` and re-run; the test will regenerate it.
|
|
|
|
## SMT tests
|
|
|
|
```
|
|
python3 -m pytest tests/test_smt.py -v
|
|
```
|
|
|
|
23 pytest tests exercising the Python API directly. Organised by layer:
|
|
|
|
- **Data model** -- ReactionSystem, concentrations, context automata,
|
|
formula construction (BagDescription, rsLTL)
|
|
- **SmtCheckerRS** -- basic reachability (no concentrations)
|
|
- **SmtCheckerRSC** -- reachability and rsLTL model checking with
|
|
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.
|