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 [ARGUMENTS].
   • 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 --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).

Arguments

All arguments are optional, except --model and --property.

• --model: Path of the input XSTS model (mandatory). Can also accept PNML files with the *.pnml extension.
• --property: Input property as a string or a file (*.prop) (mandatory). For PNML models an unsafe target marking can also be described by listing the values of each place in their order of definition separated with spaces.
• --cex: Output file where the counterexample is written (if the result is unsafe). If the argument is not given (default) the counterexample is not printed. Use CON (Windows) or /dev/stdout (Linux) as argument to print to the standard output.
• --loglevel: Detailedness of logging.
  • Possible values (from the least to the most detailed): RESULT, MAINSTEP, SUBSTEP ( default), INFO, DETAIL, VERBOSE.
• --version: Print version info (in this case --model and --property is of course not required).
• --metrics: Print metrics about the XSTS model (number of variables and statements).
• --initialmarking: Can be used with the PNML frontend. Override the initial markings of the places. Format: list the values to be assigned to each place in the order of their definition in the PNML file separated with spaces.
• --visualize: Visualize the result of the analysis (the reachability graph if the model is safe, or a counterexample trace if it is unsafe). Prints to the dotfile given as parameter.
• --optimizestmts: The algorithm can optimize stmts by detecting failing assumptions and unreachable branches of choices.
  • Possible values: ON (default), OFF.

The arguments related to the algorithm are described in more detail (along with best practices) in CEGAR-algorithms.md.

For developer usage

Flag	Description
--stacktrace	Print full stack trace for exceptions.
--benchmark	Benchmark mode, only print metrics in csv format.
--header	Print the header for the benchmark mode csv format.