xsts-cli

Overview

The xsts-cli project is an executable (command line) tool for running CEGAR-based analyses on XSTSs. For more information about the XSTS formalism and its supported language elements, take a look at the xsts project.

Related projects

• xsts: Classes to represent XSTSs and a domain specific language (DSL) to parse XSTSs from a textual representation.
• xsts-analysis: XSTS specific analysis modules enabling the algorithms to operate on them.

Frontends

• Gamma is a statechart composition framework, that supports theta-xsts-cli as a backend to verify collaborating state machines.

Using the tool

1. First, get the tool.
   • The easiest way is to download a pre-built release.
   • You can also build the tool yourself. The runnable jar file will appear under build/libs/ with the name theta-xsts-cli-<VERSION>-all.jar, you can simply rename it to theta-xsts-cli.jar.
   • Alternatively, you can use our docker image (see below).
2. Running the tool requires Java (JRE) 17.
3. The tool also requires the Z3 SMT solver libraries to be available on PATH.
4. The tool can be executed with java -jar theta-xsts-cli.jar [SUBCOMMAND] [ARGUMENTS].
   • SUBCOMMAND should be the algorithm you want to run (Previous commands with the --algorithm switch should move the value here)
   • If no arguments are given, a help screen is displayed about the arguments and their possible values. More information can also be found below.
   • For example java -jar theta-xsts-cli.jar CEGAR --model crossroad.xsts --property "x>1" --loglevel INFO runs the default analysis with logging on the crossroad.xsts model file with the property x>1.

Docker

A Dockerfile is also available under the docker directory in the root of the repository. The image can be built using the following command (from the root of the repository):

docker build -t theta-xsts-cli -f docker/theta-xsts-cli.Dockerfile .

The script run-theta-xsts-cli.sh can be used for running the containerized version on models residing on the host:

./docker/run-theta-xsts-cli.sh crossroad.xsts --property "x>1" [OTHER ARGUMENTS]

Note that the model must be given as the first positional argument (without --model).

Subcommands

There are two categories of subcommands, one for model checking and one for helper texts. For up to date information, run the CLI without any subcommand, or with the --help flag and the available subcommands will be printed for you.

Algorithms

The following subcommands are available as arguments:

Feature	Description
CEGAR	Model checking using the CEGAR (CounterExample Guided Abstraction Refinement) algorithm
LTLCEGAR	Model checking using the CEGAR algorithm with an LTL property
BOUNDED	Bounded model checking algorithms (BMC, IMC, KINDUCTION). Use --variant to select the algorithm (by default, BMC is selected).
MDD	Model checking of XSTS using MDDs (Multi-value Decision Diagrams)
PN_MDD	Model checking of Petri nets using MDDs (Multi-value Decision Diagrams)
CHC	Model checking using the Horn solving backend

Helper commands

There are two subcommands that simply output information:

• header : Used to print a header for outputs generated by the --benchmark option in the algorithm commands. If you are doing a larger benchmark with multiple runs piping into a file, this can be run first to provide a header for the file
• metrics : Prints information about the input xsts model

Common arguments

There is two group of arguments that are mostly common among all the algorithm subcommands.

Input options

Options related to model and property input

Option	Description
--model=<path>	Path of the input model (XSTS or Pnml). Extension should be .pnml to be handled as Petri-net input
--property=<file>	Path of the property file. Has priority over --inlineProperty
--inline-property=<text>	Input property as a string. Ignored if --property is defined

Output options

Options related to output and statistics

Option	Description
--log-level=<value>	Detailedness of logging. Possible values: RESULT, MAINSTEP, SUBSTEP, INFO, DETAIL, VERBOSE
--benchmark=<value>	Quiet mode, output will be just the result metrics. Possible values: true, false
--cexfile=<path>	Write concrete counterexample to a file
--stacktrace	Print stack trace of exceptions
--visualize=<path>	Write proof or counterexample to file in DOT format