TorXakis is a tool for Model Based Testing.
It is licensed under the BSD3 license.
User documentation at our wiki.
For Windows systems an installer is provided in the releases section.
We provide a
deb package from Debian based systems (Debian, Ubuntu, etc), and an
rpm package for distros using the RPM package manager. Below we give
instructions on how to install
TorXakis on Ubuntu.
Download the latest
deb release of
the example below) and then run the following commands:
apt-get update apt-get install ./torxakis_0.6.0_amd64.deb -y
deb package was tested on Ubuntu version
TorXakis in RPM based distros please check your Linux distro
For macOS systems we provide a homebrew package. To install
brew tap torxakis/torxakis brew install torxakis
For more detailed instructions see the Homebrew tap for TorXakis.
TorXakis is written in Haskell and
stack as build tool. In addition
TorXakis needs an SMT solver, such as cvc4 or Z3. The SMT Solver
needs to support SMTLIB version 2.5, Algebraic Data Types (as
proposed for version 2.6), and Strings. The SMT Solvers are assumed to be
located on the PATH. For development acceptance tests javac is needed.
The Haddock documentation is also available here.
Make sure that
stack is installed, then clone this repository.
TorXakis requires a
1.6.1 or greater. To build and install
TorXakis locally, if you are on a Windows system run:
stack setup stack install
On Linux, the following libraries should be installed:
For Unix systems a different stack configuration is used:
stack setup --stack-yaml stack_linux.yaml stack install --stack-yaml stack_linux.yaml
The reason for having two configuration files is that on Windows systems the
libraries are linked statically, and thus we cannot use the
TorXakis is licensed under the BSD3 license.
In the instructions that follow we will omit the
--stack-yaml stack-linux.yaml flag, but bear in mind that if you're in an Unix system you
need to add it (or set the
STACK_YAML environment variable to
If you experience problems when building from source, sometimes this could be
due to Makefiles which do not handle parallel builds well. If problems appear
while building, try setting the
MAKEFLAGS variable to
" -j1 " before
running the build commands. For instance on Unix systems this can be achieved
export MAKEFLAGS=" -j1 " stack setup stack install
Note that the
MAKEFLAGS variable does not affect the parallelism within
By default, several compiler warnings are treated as errors. While developing
we'd like to avoid this: removing warnings requires some extra time. Some parts
of the code might not make it when submitting a pull request. Therefore, before
a new feature or fix is ready, it doesn't make sense to try to remove warnings
on code that will be deleted in the end. So to have the build system avoid
treating warnings as errors use the flag
develop as follows:
stack <STACK ARGS> --flag '*:develop'
stack test --stack-yaml stack_linux.yaml --file-watch txs-compiler --ta "-m wrong" --flag '*:develop'
Note that currently only the package
txs-compiler supports this flag. If you
find yourself needing this flag for other packages feel free to submit an
issue or pull request.
When submitting a pull request, our continuous integration process will run a
series of tests. There are two levels of tests that we use in
unit-tests and integration tests. Unit-tests can be run when building using
stack by passing this
stack install --test
To run the integration tests go to the
test/sqatt folder, and run:
See the README in the
sqatt folder for more
It is important to keep an eye on the performance of
there is no continuous benchmarking process in place, however you can check
locally the performance by running the benchmarks for the (current)
version, and the version that you are working on. To run the benchmarks and
generate the reports on Unix systems you can run:
cd test/sqatt stack bench --ba "--output `date +%s`-report-`git rev-parse HEAD`.html --csv `date +%s`-report-`git rev-parse HEAD`.csv"
On Windows PowerShell you can run:
cd test\sqatt stack bench --ba "--output $(get-date).ToString("yyyyMMdd-hhmmss")-report-$((git rev-parse HEAD).Substring(0,8)).html --csv $(get-date).ToString("yyyyMMdd-hhmmss")-report-$((git rev-parse HEAD).Substring(0,8)).csv"
See the README in the
sqatt folder for more
There are several folders in this repository, which serve different purposes:
bin: utility scripts to start
TorXakisUI and server.
ci: scripts used in our continuous integration process.
ci/mk-package: files needed to create Linux packages.
docs: documentation files for
examps: example models and systems-under-test (SUT's) to play around with. This folder also contains some binary (.jpg and .pptx) files, which are used for documentation. Such files are tracked with Git-LFS(*).
sys: packages that make up
TorXakisthis is where the source code resides.
test: utilities for quality assurance tests (integration-tests, license-checking, etc).
See the README files in each folders to get a more detailed explanation.
(*): Git-LFS is installed by default along with official git client, so you should be able to access these files without extra effort. If, for some reason, you don't have Git-LFS, then you can install the official Git-LFS extension.