Implementation of two Verifiers for Hierarchical Artifact Systems
- Spin-based link
- Karp-Miller-based (VERIFAS) link
- VLDB PhD workshop paper link
- More on the theory link
Simply use the Makefile in verifier/
./has_real ../bpmn/INPUT_FILE_NAME MODE NAIVE PROPERTY
- Mode:
- 0 -> VERIFAS, the karp-miller based verifier
- 1 -> Spin-based verifier
- 2 -> VERIFAS with artifact relations ignored
- NAIVE:
- 0 -> All opimizations are on
- 1-4 (1-2 for Spin) -> One of the opimizations is turned off
- PROPERTY: 0 - 11, template of the LTL-FO property to be verified. Please refer to Table 4 of link for more details. A LTL-FO property will be generated from the template and verified by the verifier.
- Spin:
python run_spin.py
- Karp-Miller:
python run_km.py
- Karp-Miller with no artifact relations:
python run_km_noset.py
- Spin:
python run_spin_synthetic.py
- Karp-Miller:
python run_km_synthetic.py
- Karp-Miller with no artifact relations:
python run_km_noset_synthetic.py