This project contains an executable tool (command line) for running analyses on XTAs.
xta: Classes to represent XTAs and a domain specific language (DSL) to parse XTAs from a textual representation.xta-analysis: XTA specific analysis modules enabling the algorithms to operate on them.
- 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-xta-cli-<VERSION>-all.jar, you can simply rename it to theta-xta-cli.jar.
- Alternatively, you can use our docker image (see below).
- Running the tool requires Java (JRE) 17.
- The tool also requires the Z3 SMT solver libraries to be available
on
PATH. - The tool can be executed with
java -jar theta-xta-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.
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-xta-cli -f docker/theta-xta-cli.Dockerfile .
The script run-theta-xta-cli.sh can be used for running the containerized version on models
residing on the host:
./docker/run-theta-xta-cli.sh model.xta [OTHER ARGUMENTS]
Note that the model must be given as the first positional argument (without --model).