From 7294a7204d208ce046dabc4fefaa7181615b610b Mon Sep 17 00:00:00 2001 From: Paul Eichler Date: Mon, 26 Jan 2026 15:35:25 +0100 Subject: [PATCH 1/5] fix: developer documentation links, update: README This commit update the README and fixes the developer documentation links. Additionally, it adds links to the individual crates.io pages. --- CHANGELOG.md | 1 + README.md | 50 ++++++++++++++++++++++++++++++----- docs/dev-docs.md | 68 ++++++++++++++++++++++++++++++------------------ 3 files changed, 87 insertions(+), 32 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 775eb8e..f894825 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,7 @@ ### Fixed +- update the README and fix developer documentation links (#4) - doc images as `.webp` and naming of TACO (toolsuite / model checker) consistent (#3) - replaced `localhost` reference in `sitemap.xml` and `robots.txt` (#2) diff --git a/README.md b/README.md index 2e709ed..241ab90 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,10 @@ +![GitHub License](https://img.shields.io/github/license/cispa/TACO?style=flat-square) +![GitHub top language](https://img.shields.io/github/languages/top/cispa/TACO?style=flat-square) +[![Continuous Integration](https://img.shields.io/github/actions/workflow/status/cispa/TACO/test.yml?branch=main&label=tests&style=flat-square)](https://github.com/cispa/TACO/actions/workflows/test.yml?query=branch%3Amain) +[![Website Build](https://img.shields.io/github/actions/workflow/status/cispa/TACO/static.yml?branch=main&label=website&color=%2303dbfc&style=flat-square)](https://taco-mc.dev) +[![GitHub Release](https://img.shields.io/github/v/release/cispa/TACO?style=flat-square)](https://github.com/cispa/TACO/releases) +![GitHub Discussions](https://img.shields.io/github/discussions/cispa/TACO?style=flat-square) + # TACO Toolsuite The Threshold Automata for COnsensus (TACO) model checker tool suite is a @@ -5,16 +12,45 @@ 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 by visiting TACO's web page -[`taco-mc.dev`](https://taco-mc.dev). +and how to use them on [TACO's web page `taco-mc.dev`](https://taco-mc.dev). + +## Documentation & Installation -There you will also be able to find installation instructions and the developer -documentation for TACO. +You can find general information about the structure of TACO on the +[TACO website](https://taco-mc.dev/). + +For instructions on how to install the CLI, i.e., `taco-cli` refer to +[the installation page](https://taco-mc.dev/install/). +Once you have installed the CLI you can find a quick start guide +[here](https://taco-mc.dev/usage-cli/). Alternatively, you can find all the documentation files TACO's website is generated from in the [`./docs`](./docs) folder. -## Contributing +## Crates + +TACO consists of multiple crates: + +| Crate | Current Version | Docs | Description | +| ------------------------ | --------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------- | +| taco-acs-model-checker | [![Crates.io](https://img.shields.io/crates/v/taco-acs-model-checker?style=flat-square)](https://crates.io/crates/taco-acs-model-checker) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_acs_model_checker/index.html) | ACS Model Checker Implementation | +| taco-bdd | [![Crates.io](https://img.shields.io/crates/v/taco-bdd?style=flat-square)](https://crates.io/crates/taco-bdd) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_bdd/index.html) | High-level interface for BDDs in TACO | +| taco-cli | [![Crates.io](https://img.shields.io/crates/v/taco-cli?style=flat-square)](https://crates.io/crates/taco-cli) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_cli/index.html) | Command Line Interface for TACO | +| taco-display-utils | [![Crates.io](https://img.shields.io/crates/v/taco-display-utils?style=flat-square)](https://crates.io/crates/taco-display-utils) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_display_utils/index.html) | Utility functions for printing string representations | +| taco-interval-ta | [![Crates.io](https://img.shields.io/crates/v/taco-interval-ta?style=flat-square)](https://crates.io/crates/taco-interval-ta) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_interval_ta/index.html) | Threshold automaton with interval abstraction applied | +| taco-model-checker | [![Crates.io](https://img.shields.io/crates/v/taco-model-checker?style=flat-square)](https://crates.io/crates/taco-model-checker) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_model_checker/index.html) | Model Checker Interface and Specifications | +| taco-parser | [![Crates.io](https://img.shields.io/crates/v/taco-parser?style=flat-square)](https://crates.io/crates/taco-parser) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_parser/index.html) | Parser implementations for threshold automata | +| taco-smt-encoder | [![Crates.io](https://img.shields.io/crates/v/taco-smt-encoder?style=flat-square)](https://crates.io/crates/taco-smt-encoder) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_smt_encoder/index.html) | Utility code to setup SMT solvers and encoding functions | +| taco-smt-model-checker | [![Crates.io](https://img.shields.io/crates/v/taco-smt-model-checker?style=flat-square)](https://crates.io/crates/taco-smt-model-checker) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_smt_model_checker/index.html) | Implementation of the SMT model checker | +| taco-threshold-automaton | [![Crates.io](https://img.shields.io/crates/v/taco-threshold-automaton?style=flat-square)](https://crates.io/crates/taco-threshold-automaton) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_threshold_automaton/index.html) | Basic types for threshold automata | +| taco-zcs-model-checker | [![Crates.io](https://img.shields.io/crates/v/taco-zcs-model-checker?style=flat-square)](https://crates.io/crates/taco-zcs-model-checker) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_zcs_model_checker/index.html) | Implementation of the ZCS model checker | + +You can find the source code in the respective folder under +[`./crates`](./crates/). You can find a more detailed explanation of the +function of each crate and development dependencies in the +[`Developer Documentation`](https://taco-mc.dev/dev-docs/). + +## Questions & Contributing We tried to design TACO as modular as possible. We hope that this will enable you to write your own tools for threshold automata. @@ -22,7 +58,7 @@ 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 on this repository. +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! diff --git a/docs/dev-docs.md b/docs/dev-docs.md index c858936..e86a1b8 100644 --- a/docs/dev-docs.md +++ b/docs/dev-docs.md @@ -17,9 +17,11 @@ It consists of two main sections: ## Crates +[![Static Badge](https://img.shields.io/badge/github-repo-blue?logo=github&style=flat-square)![](https://img.shields.io/github/v/release/cispa/TACO?style=flat-square)](https://github.com/cispa/TACO) + This section describes the high-level function of the crates that comprise the -TACO toolsuite. You can find the source code for all of them in the `crates` -directory. +TACO toolsuite. You can find the source code for all of them in the [GitHub +Repository](https://github.com/cispa/TACO) in the `crates` directory. :::{tip} Clicking on the name of a crate will forward you to Rust documentation @@ -31,16 +33,34 @@ However, our internal version also contains the documentation for private types, giving you more insights into the implementation details. ::: +#### Backend and Utility Crates + +- [`taco-bdd`](./dev-docs/taco_bdd/index.html) : This library crate implements a common interface + to interact with BDD libraries. Currently it supports + [OxiDD](https://oxidd.net/) and [CUDD](https://github.com/cuddorg/cudd). +- [`taco-cli`](./dev-docs/taco_cli/index.html): The binary crate containing the code of + the TACO Command Line Interface. +- [`taco-display-utils`](./dev-docs/taco_display_utils/index.html): A small library crate for + common helper methods for nicely displaying types. +- [`taco-parser`](./dev-docs/taco_parser/index.html): An interface definition of parsers that can be + used to parse a threshold automaton from different formats. This crate already + contains a parser for `.ta` and `.eta` files that has been introduced by ByMC + [here](https://github.com/konnov/bymc/blob/master/bymc/doc/ta-format.md). +- [`taco-smt-encoder`](./dev-docs/taco_smt_encoder/index.html): This library crate implements + the configuration and setup of connections to SMT solvers. Additionally, it + defines SMT encodings of types of the `threshold-automaton` crate and provides + structures to encode constraints on configurations and paths. + ### Threshold Automaton Representations These crates define different representations of threshold automata at different levels of abstraction, which can be used as inputs to model checkers. -- [`taco-interval-ta`](./taco_interval_ta/index.html): +- [`taco-interval-ta`](./dev-docs/taco_interval_ta/index.html): This library crate implements the interval abstraction of a threshold automaton. It contains a threshold automaton type that uses sets of (symbolic) intervals as guards. -- [`taco-threshold-automaton`](./taco_threshold_automaton/index.html): This crate defines +- [`taco-threshold-automaton`](./dev-docs/taco_threshold_automaton/index.html): This crate defines the types: - `GeneralThresholdAutomaton`, which is the most general form of a threshold automaton. For example, it allows comparisons between variables or guards in @@ -54,7 +74,7 @@ levels of abstraction, which can be used as inputs to model checkers. Model checkers and specifications must implement the interfaces defined in the -- [`taco-model-checker`](./taco_model_checker/index.html) crate. This library crate +- [`taco-model-checker`](./dev-docs/taco_model_checker/index.html) crate. This library crate defines the common interface for model checkers, as well as some useful preprocessing tools that can apply useful transformations or simplifications to threshold automata. @@ -62,30 +82,28 @@ Model checkers and specifications must implement the interfaces defined in the TACO already implements 3 algorithms, which are split into their own separate crates: -- [`taco-acs-model-checker`](./taco_acs_model_checker/index.html): Contains the +- [`taco-acs-model-checker`](./dev-docs/taco_acs_model_checker/index.html): Contains the implementation of the 'ACS' model checker. -- [`taco-smt-model-checker`](./taco_smt_model_checker/index.html): Contains the +- [`taco-smt-model-checker`](./dev-docs/taco_smt_model_checker/index.html): Contains the implementation of the 'SMT' model checker. -- [`taco-zcs-model-checker`](./taco_zcs_model_checker/index.html): Contains the +- [`taco-zcs-model-checker`](./dev-docs/taco_zcs_model_checker/index.html): Contains the implementation of the 'ZCS' model checker. -### Backend and Utility Crates - -- [`taco-bdd`](./taco_bdd/index.html) : This library crate implements a common interface - to interact with BDD libraries. Currently it supports - [OxiDD](https://oxidd.net/) and [CUDD](https://github.com/cuddorg/cudd). -- [`taco-cli`](./taco_cli/index.html): The binary crate containing the code of - the TACO Command Line Interface. -- [`taco-display-utils`](./taco_display_utils/index.html): A small library crate for - common helper methods for nicely displaying types. -- [`taco-parser`](./taco_parser/index.html): An interface definition of parsers that can be - used to parse a threshold automaton from different formats. This crate already - contains a parser for `.ta` and `.eta` files that has been introduced by ByMC - [here](https://github.com/konnov/bymc/blob/master/bymc/doc/ta-format.md). -- [`taco-smt-encoder`](./taco_smt_encoder/index.html): This library crate implements - the configuration and setup of connections to SMT solvers. Additionally, it - defines SMT encodings of types of the `threshold-automaton` crate and provides - structures to encode constraints on configurations and paths. +### Summary + +| Crate | Current Version | Docs | Description | +| ------------------------ | --------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------- | +| taco-acs-model-checker | [![Crates.io](https://img.shields.io/crates/v/taco-acs-model-checker?style=flat-square)](https://crates.io/crates/taco-acs-model-checker) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_acs_model_checker/index.html) | ACS Model Checker Implementation | +| taco-bdd | [![Crates.io](https://img.shields.io/crates/v/taco-bdd?style=flat-square)](https://crates.io/crates/taco-bdd) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_bdd/index.html) | High-level interface for BDDs in TACO | +| taco-cli | [![Crates.io](https://img.shields.io/crates/v/taco-cli?style=flat-square)](https://crates.io/crates/taco-cli) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_cli/index.html) | Command Line Interface for TACO | +| taco-display-utils | [![Crates.io](https://img.shields.io/crates/v/taco-display-utils?style=flat-square)](https://crates.io/crates/taco-display-utils) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_display_utils/index.html) | Utility functions for printing string representations | +| taco-interval-ta | [![Crates.io](https://img.shields.io/crates/v/taco-interval-ta?style=flat-square)](https://crates.io/crates/taco-interval-ta) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_interval_ta/index.html) | Threshold automaton with interval abstraction applied | +| taco-model-checker | [![Crates.io](https://img.shields.io/crates/v/taco-model-checker?style=flat-square)](https://crates.io/crates/taco-model-checker) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_model_checker/index.html) | Model Checker Interface and Specifications | +| taco-parser | [![Crates.io](https://img.shields.io/crates/v/taco-parser?style=flat-square)](https://crates.io/crates/taco-parser) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_parser/index.html) | Parser implementations for threshold automata | +| taco-smt-encoder | [![Crates.io](https://img.shields.io/crates/v/taco-smt-encoder?style=flat-square)](https://crates.io/crates/taco-smt-encoder) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_smt_encoder/index.html) | Utility code to setup SMT solvers and encoding functions | +| taco-smt-model-checker | [![Crates.io](https://img.shields.io/crates/v/taco-smt-model-checker?style=flat-square)](https://crates.io/crates/taco-smt-model-checker) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_smt_model_checker/index.html) | Implementation of the SMT model checker | +| taco-threshold-automaton | [![Crates.io](https://img.shields.io/crates/v/taco-threshold-automaton?style=flat-square)](https://crates.io/crates/taco-threshold-automaton) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_threshold_automaton/index.html) | Basic types for threshold automata | +| taco-zcs-model-checker | [![Crates.io](https://img.shields.io/crates/v/taco-zcs-model-checker?style=flat-square)](https://crates.io/crates/taco-zcs-model-checker) | [![Api Docs](https://img.shields.io/badge/docs-api-blue?style=flat-square)](https://taco-mc.dev/dev-docs/taco_zcs_model_checker/index.html) | Implementation of the ZCS model checker | (development-setup)= From 9ad93f8ea3f17eb4c87bef3774b5ee7be789dad1 Mon Sep 17 00:00:00 2001 From: Paul Eichler Date: Mon, 26 Jan 2026 15:41:04 +0100 Subject: [PATCH 2/5] fixup! fix: developer documentation links, update: README --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f894825..e940323 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,7 +9,7 @@ ### Fixed -- update the README and fix developer documentation links (#4) +- update the README and fix developer documentation links (#5) - doc images as `.webp` and naming of TACO (toolsuite / model checker) consistent (#3) - replaced `localhost` reference in `sitemap.xml` and `robots.txt` (#2) From 622aa055021bbdff15a3eabdc073ea2ddfb83295 Mon Sep 17 00:00:00 2001 From: Paul Eichler Date: Mon, 26 Jan 2026 15:49:24 +0100 Subject: [PATCH 3/5] fixup! fix: logo text (#4) --- .github/workflows/test.yml | 22 +++++++++++----------- docs/usage-cli/install.md | 2 +- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index addb520..f1f2e9d 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -1,9 +1,9 @@ name: Formatting, Linting, License Checks and Testing on: push: - branches: [ "main" ] + branches: ["main"] pull_request: - branches: [ "main" ] + branches: ["main"] env: CARGO_TERM_COLOR: always @@ -62,7 +62,7 @@ jobs: run: rustup +${RUST_VERSION} component add clippy - name: check run: cargo +${RUST_VERSION} clippy --verbose --all-targets --all-features - + # Run tests on Linux test-linux: needs: clippy @@ -77,7 +77,7 @@ jobs: - name: Install Dependencies (Z3,CVC5,Graphviz) run: sudo apt-get install -y z3 cvc5 graphviz - name: Install Nextest - run: cargo +${RUST_VERSION} install cargo-nextest + run: cargo +${RUST_VERSION} install cargo-nextest --locked - name: Run unittests run: cargo +${RUST_VERSION} nextest run -P ci --verbose --all-targets --all-features - name: Publish Test Report @@ -85,11 +85,11 @@ jobs: if: always() # always run with: # Core Configuration - report-path: 'target/nextest/ci/test-output.xml' # Path or glob pattern to the CTRF report JSON file. + report-path: "target/nextest/ci/test-output.xml" # Path or glob pattern to the CTRF report JSON file. # Reports - Choose as many as you like. Default is false. Choosing none will use default reports. summary-report: true summary: true # Post report to the job summary. Default is true - title: 'Test Report Linux' # Set a custom title to display on the report. + title: "Test Report Linux" # Set a custom title to display on the report. integrations-config: | { "junit-to-ctrf": { @@ -105,7 +105,7 @@ jobs: } } } - + # Run tests on macOS test-macos: needs: clippy @@ -122,7 +122,7 @@ jobs: - name: Install CVC5 run: brew install --cask cvc5/cvc5/cvc5 - name: Install Nextest - run: cargo +${RUST_VERSION} install cargo-nextest + run: cargo +${RUST_VERSION} install cargo-nextest --locked - name: Run unittests run: cargo +${RUST_VERSION} nextest run -P ci --verbose --all-targets --all-features - name: Publish Test Report @@ -130,11 +130,11 @@ jobs: if: always() # always run with: # Core Configuration - report-path: 'target/nextest/ci/test-output.xml' # Path or glob pattern to the CTRF report JSON file. + report-path: "target/nextest/ci/test-output.xml" # Path or glob pattern to the CTRF report JSON file. # Reports - Choose as many as you like. Default is false. Choosing none will use default reports. summary-report: true summary: true # Post report to the job summary. Default is true - title: 'Test Report MacOS' # Set a custom title to display on the report. + title: "Test Report MacOS" # Set a custom title to display on the report. integrations-config: | { "junit-to-ctrf": { @@ -177,7 +177,7 @@ jobs: hide_complexity: true indicators: true output: both - thresholds: '90 95' + thresholds: "90 95" - name: Print coverage report to summary run: | cat code-coverage-results.md >> $GITHUB_STEP_SUMMARY diff --git a/docs/usage-cli/install.md b/docs/usage-cli/install.md index 439408a..169ba5a 100644 --- a/docs/usage-cli/install.md +++ b/docs/usage-cli/install.md @@ -102,7 +102,7 @@ instructions of the official Once cargo is installed, you can install TACO by running ```bash -cargo install taco-cli +cargo install taco-cli --locked ``` Now the `taco-cli` command should be available on your system. You can test the From 8d1f1f14536cdd05900f912508755698e1cdb978 Mon Sep 17 00:00:00 2001 From: Paul Eichler Date: Mon, 26 Jan 2026 15:50:52 +0100 Subject: [PATCH 4/5] fixup! fix: logo text (#4) --- docs/dev-docs.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/dev-docs.md b/docs/dev-docs.md index e86a1b8..b7a5e67 100644 --- a/docs/dev-docs.md +++ b/docs/dev-docs.md @@ -33,7 +33,7 @@ However, our internal version also contains the documentation for private types, giving you more insights into the implementation details. ::: -#### Backend and Utility Crates +### Backend and Utility Crates - [`taco-bdd`](./dev-docs/taco_bdd/index.html) : This library crate implements a common interface to interact with BDD libraries. Currently it supports From bc0fe295d88c552e6cf4a4ff76a0fc24c5068fa0 Mon Sep 17 00:00:00 2001 From: Paul Eichler <60977980+pleich@users.noreply.github.com> Date: Mon, 26 Jan 2026 15:56:50 +0100 Subject: [PATCH 5/5] remove extra whitespace Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> Signed-off-by: Paul Eichler <60977980+pleich@users.noreply.github.com> --- docs/dev-docs.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/dev-docs.md b/docs/dev-docs.md index b7a5e67..deb0d5d 100644 --- a/docs/dev-docs.md +++ b/docs/dev-docs.md @@ -35,7 +35,7 @@ giving you more insights into the implementation details. ### Backend and Utility Crates -- [`taco-bdd`](./dev-docs/taco_bdd/index.html) : This library crate implements a common interface +- [`taco-bdd`](./dev-docs/taco_bdd/index.html): This library crate implements a common interface to interact with BDD libraries. Currently it supports [OxiDD](https://oxidd.net/) and [CUDD](https://github.com/cuddorg/cudd). - [`taco-cli`](./dev-docs/taco_cli/index.html): The binary crate containing the code of