Skip to content

Latest commit

 

History

History
26 lines (18 loc) · 1.14 KB

README.md

File metadata and controls

26 lines (18 loc) · 1.14 KB
Raw

torpedo

Partial kripke structure LTL model checker

Compile

Run sbt assembly.

Launch

Install the required Docker containers running ./prepare.sh from the docker folder.

After compilation, run java -jar target/scala-2.12/torpedo.jar analysis [options] <PKS XML file> <property file> to check a property.

Possible options are:

  • -c <filename>: write a trace violating the property to the given filename.
  • -i <filename prefix>: write the input passed to the external solver in files with a given prefix.
  • -l <filename prefix>: write the external solver output in files with a given prefix.
  • -o <filename>: write the parts of the PKS needed for the property to hold to the given filename.
  • -s solver [bound]: external solver to be used. Possible choices are pltlmup, hybrid and z3. The bound parameter is only allowed (and required) for z3.
  • -t <filename>: write the parts of the PKS needed for the property to hold to the given filename as a PKS slice.

Run java -jar target/scala-2.12/torpedo.jar recheck <PKS XML file> <PKS Slice file> to see if the proof contained in the slice file is still valid for the new PKS.