Setup and Installation - TACO Toolsuite

Prerequisites¶

Supported SMT Solvers¶

TACO internally uses SMT solvers for the model checking. However, it does not ship with any solvers by default. Currently, TACO will check whether Z3 or CVC5 is installed on your system. If you do not have a favorite SMT solver we recommend you install CVC5 and/or Z3.

You can also use a custom SMT solver when verifying systems with TACO. You can find more details on how to configure a custom solver in section Using a custom SMT solver.

Many package managers have a package for Z3, for example, you can install Z3 on Debian-based Linux distributions (like Ubuntu) using:

sudo apt-get install z3

or under MacOS using homebrew with:

brew install z3

For other operating systems consult your package manager or check the Z3 documentation.

Many package managers have a package for CVC5, for example, you can install CVC5 on Debian-based Linux distributions (like Ubuntu) using:

sudo apt-get install cvc5

Under MacOS there exists a cask in the cvc5 GitHub organization (see) which you can use with homebrew with:

brew install --cask cvc5/cvc5/cvc5

For other operating systems consult your package manager or check the CVC5 download page.

Visualization: Installing Graphviz¶

Currently, the tool only supports a simple visualization of threshold automata by encoding the threshold automata into graphs encoded in the DOT Language.

This format can be converted into an image using the graphviz library.

The tool provides a convenient CLI command visualize. However, to output svg or png the graphviz library must already be installed on your system. Otherwise, you can always export an automaton into the dot format and use a compatible visualization tool.

On Debian / Ubuntu you can use

sudo apt-get install graphviz

to install graphviz or under MacOS use homebrew with:

brew install graphviz

For other operating systems please consult the official graphviz download page.

Installation¶

TACO can be installed using cargo, the Rust package manager (and a working Rust installation). If cargo (and Rust) is not yet installed on your system, you can follow the instructions of the official Rust installation guide.

Once cargo is installed, you can install TACO by running

cargo install taco-cli --locked

Now the taco-cli command should be available on your system. You can test the installation by running

taco-cli --version