Setup and Installation - TACO Model Checker

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 CVC5, for example, you can install CVC5 on Debian-based Linux distributions (like Ubuntu) using:

sudo apt-get install cvc5

or under MacOS using homebrew with:

brew install cvc5

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

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.

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.