The Threshold Automata for COnsensus (TACO) model checker tool suite is a collection of tools to analyze and verify distributed algorithms, modeled as threshold automata.
You can learn more about threshold automata, the algorithms implemented in TACO
and how to use them on TACO's web page taco-mc.dev.
You can find general information about the structure of TACO on the TACO website.
For instructions on how to install the CLI, i.e., taco-cli refer to
the installation page.
Once you have installed the CLI you can find a quick start guide
here.
Alternatively, you can find all the documentation files TACO's website is
generated from in the ./docs folder.
TACO consists of multiple crates:
| Crate | Current Version | Docs | Description |
|---|---|---|---|
| taco-acs-model-checker |  |
 |
ACS Model Checker Implementation |
| taco-bdd |  |
|
High-level interface for BDDs in TACO |
| taco-cli |  |
|
Command Line Interface for TACO |
| taco-display-utils |  |
|
Utility functions for printing string representations |
| taco-interval-ta |  |
|
Threshold automaton with interval abstraction applied |
| taco-model-checker |  |
|
Model Checker Interface and Specifications |
| taco-parser |  |
|
Parser implementations for threshold automata |
| taco-smt-encoder |  |
|
Utility code to setup SMT solvers and encoding functions |
| taco-smt-model-checker |  |
|
Implementation of the SMT model checker |
| taco-threshold-automaton |  |
|
Basic types for threshold automata |
| taco-zcs-model-checker |  |
|
Implementation of the ZCS model checker |
You can find the source code in the respective folder under
./crates. You can find a more detailed explanation of the
function of each crate and development dependencies in the
Developer Documentation.
We tried to design TACO as modular as possible. We hope that this will enable you to write your own tools for threshold automata.
You will be able to find more information about TACO's internal structure in the developer documentation.
If you have any questions, feature requests, or something is unclear, feel free to open an issue or create a discussion on this repository.
If you think TACO is missing a vital feature, feel free to open a PR!