ITS-Tools command line

ITS-Tools is a model checker for Petri nets and for its own language GAL, combining structural reductions, SMT, symbolic decision diagrams, partial-order explicit engines and random walks. The project homepage describes the tool; this page distributes its command line, the build that runs in the Model Checking Contest.

Downloads

Unzip, then run the command from the unzipped folder. Java 21 or later must be on the path; the archives embed the solver binaries (ITS, LTSmin, Spot, Z3, PetriSpot, GreatSPN order heuristics) for their platform. The same site is the Eclipse update site of ITS-Tools (https://lip6.github.io/ITSTools/) for the version with editors and the graphical integration.

Checking a Model Checking Contest instance

Give a folder holding model.pnml and the property files of the contest (ReachabilityCardinality.xml, LTLFireability.xml, ...), and an examination name:

./its-tools -pnfolder path/to/AirplaneLD-PT-0010 -examination LTLCardinality \
    -its -ltsmin -smt -timeout 3600

Verdicts are printed as FORMULA name TRUE|FALSE|value TECHNIQUES ... lines as they are established. Engines are opted in: -its (decision diagrams), -ltsmin (partial-order explicit), -smt (Z3 on the state equation), -greatspnpath DIR -order META -manyOrder (GreatSPN variable orders, the contest setting); -timeout is in seconds. -onlyGal stops after the translation to GAL.

Checking a GAL model

./its-tools -i model.gal -reach              # the safety and bound properties of the file
./its-tools -i model.gal -ctl                # its CTL properties
./its-tools -i model.gal -ltl                # its LTL properties
./its-tools -i model.gal -ltl -itsflags "--trace-states -manywitness 10"

-i takes a full GAL model as written in Eclipse (parameters, hierarchy, loops, properties); one logic flag at a time; -itsflags passes its argument as is to the underlying engine; -timeout bounds the run in seconds, -o FILE writes the translated model.

The same tool without the JVM start-up

The Linux archive also ships its-tools-flat.sh, which runs the same classes on a plain class path (no Eclipse framework, no configuration folder, same arguments), and the site publishes its-tools-native, a GraalVM native image of it that starts in a few milliseconds. The image is built for the contest driver, whose runs define the set of classes it knows: put it in the unzipped Linux folder, beside plugins/, and run it with the -pnfolder arguments above.

The native image is experimental. A use it was not built for may fail with a ClassNotFoundException, NoSuchMethodException or MissingReflectionRegistrationError naming a class: please open an issue with the command line and that message, and run its-tools from the same folder meanwhile, which has no such limit.

Converter

fr.lip6.converter.jar converts several Petri net dialects and property formats to PNML and to the contest's property format. Run it with java -jar fr.lip6.converter.jar (Java 21 or later).

Source, issues, licence

Source code and issue tracker: github.com/lip6/ITSTools. The contest packaging (driver scripts, installation) lives in ITS-Tools-MCC. ITS-Tools is distributed under the GPL v3. LIP6, CNRS & Sorbonne Université.