/has-verifier

Implementation of Verifiers for Hierarchical Artifact Systems

Primary LanguageCMIT LicenseMIT

has-verifier

Implementation of two Verifiers for Hierarchical Artifact Systems

  1. Spin-based link
  2. Karp-Miller-based (VERIFAS) link
  3. VLDB PhD workshop paper link
  4. More on the theory link

Prerequisite

  • Boost
  • Flex + Bison
  • g++-6
  • Spin
  • Python 2.7 (for running the experiment scripts)

How to compile

Simply use the Makefile in verifier/

How to run

./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.

How to run batch experiment

Real set of workflows

  • Spin: python run_spin.py
  • Karp-Miller: python run_km.py
  • Karp-Miller with no artifact relations: python run_km_noset.py

Synthetic set of workflows

  • 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