Skip to content

Commit 7294a72

Browse files
pleichpleich
committed
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.
1 parent 507c3e2 commit 7294a72

3 files changed

Lines changed: 87 additions & 32 deletions

File tree

‎CHANGELOG.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99

1010
### Fixed
1111

12+
- update the README and fix developer documentation links (#4)
1213
- doc images as `.webp` and naming of TACO (toolsuite / model checker)
1314
consistent (#3)
1415
- replaced `localhost` reference in `sitemap.xml` and `robots.txt` (#2)

‎README.md‎

Lines changed: 43 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,64 @@
1+
![GitHub License](https://img.shields.io/github/license/cispa/TACO?style=flat-square)
2+
![GitHub top language](https://img.shields.io/github/languages/top/cispa/TACO?style=flat-square)
3+
[![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)
4+
[![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)
5+
[![GitHub Release](https://img.shields.io/github/v/release/cispa/TACO?style=flat-square)](https://github.com/cispa/TACO/releases)
6+
![GitHub Discussions](https://img.shields.io/github/discussions/cispa/TACO?style=flat-square)
7+
18
# TACO Toolsuite
29

310
The Threshold Automata for COnsensus (TACO) model checker tool suite is a
411
collection of tools to analyze and verify distributed algorithms, modeled as
512
threshold automata.
613

714
You can learn more about threshold automata, the algorithms implemented in TACO
8-
and how to use them by visiting TACO's web page
9-
[`taco-mc.dev`](https://taco-mc.dev).
15+
and how to use them on [TACO's web page `taco-mc.dev`](https://taco-mc.dev).
16+
17+
## Documentation & Installation
1018

11-
There you will also be able to find installation instructions and the developer
12-
documentation for TACO.
19+
You can find general information about the structure of TACO on the
20+
[TACO website](https://taco-mc.dev/).
21+
22+
For instructions on how to install the CLI, i.e., `taco-cli` refer to
23+
[the installation page](https://taco-mc.dev/install/).
24+
Once you have installed the CLI you can find a quick start guide
25+
[here](https://taco-mc.dev/usage-cli/).
1326

1427
Alternatively, you can find all the documentation files TACO's website is
1528
generated from in the [`./docs`](./docs) folder.
1629

17-
## Contributing
30+
## Crates
31+
32+
TACO consists of multiple crates:
33+
34+
| Crate | Current Version | Docs | Description |
35+
| ------------------------ | --------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------- |
36+
| 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 |
37+
| 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 |
38+
| 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 |
39+
| 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 |
40+
| 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 |
41+
| 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 |
42+
| 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 |
43+
| 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 |
44+
| 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 |
45+
| 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 |
46+
| 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 |
47+
48+
You can find the source code in the respective folder under
49+
[`./crates`](./crates/). You can find a more detailed explanation of the
50+
function of each crate and development dependencies in the
51+
[`Developer Documentation`](https://taco-mc.dev/dev-docs/).
52+
53+
## Questions & Contributing
1854

1955
We tried to design TACO as modular as possible. We hope that this will enable
2056
you to write your own tools for threshold automata.
2157

2258
You will be able to find more information about TACO's internal structure in the
2359
developer documentation.
2460

25-
If you have any questions, feature requests or something is unclear feel free to
26-
open an issue on this repository.
61+
If you have any questions, feature requests, or something is unclear, feel free
62+
to open an issue or create a discussion on this repository.
2763

2864
If you think TACO is missing a vital feature, feel free to open a PR!

‎docs/dev-docs.md‎

Lines changed: 43 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,11 @@ It consists of two main sections:
1717

1818
## Crates
1919

20+
[![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)
21+
2022
This section describes the high-level function of the crates that comprise the
21-
TACO toolsuite. You can find the source code for all of them in the `crates`
22-
directory.
23+
TACO toolsuite. You can find the source code for all of them in the [GitHub
24+
Repository](https://github.com/cispa/TACO) in the `crates` directory.
2325

2426
:::{tip}
2527
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,
3133
giving you more insights into the implementation details.
3234
:::
3335

36+
#### Backend and Utility Crates
37+
38+
- [`taco-bdd`](./dev-docs/taco_bdd/index.html) : This library crate implements a common interface
39+
to interact with BDD libraries. Currently it supports
40+
[OxiDD](https://oxidd.net/) and [CUDD](https://github.com/cuddorg/cudd).
41+
- [`taco-cli`](./dev-docs/taco_cli/index.html): The binary crate containing the code of
42+
the TACO Command Line Interface.
43+
- [`taco-display-utils`](./dev-docs/taco_display_utils/index.html): A small library crate for
44+
common helper methods for nicely displaying types.
45+
- [`taco-parser`](./dev-docs/taco_parser/index.html): An interface definition of parsers that can be
46+
used to parse a threshold automaton from different formats. This crate already
47+
contains a parser for `.ta` and `.eta` files that has been introduced by ByMC
48+
[here](https://github.com/konnov/bymc/blob/master/bymc/doc/ta-format.md).
49+
- [`taco-smt-encoder`](./dev-docs/taco_smt_encoder/index.html): This library crate implements
50+
the configuration and setup of connections to SMT solvers. Additionally, it
51+
defines SMT encodings of types of the `threshold-automaton` crate and provides
52+
structures to encode constraints on configurations and paths.
53+
3454
### Threshold Automaton Representations
3555

3656
These crates define different representations of threshold automata at different
3757
levels of abstraction, which can be used as inputs to model checkers.
3858

39-
- [`taco-interval-ta`](./taco_interval_ta/index.html):
59+
- [`taco-interval-ta`](./dev-docs/taco_interval_ta/index.html):
4060
This library crate implements the interval abstraction of a threshold
4161
automaton. It contains a threshold automaton type that uses sets of
4262
(symbolic) intervals as guards.
43-
- [`taco-threshold-automaton`](./taco_threshold_automaton/index.html): This crate defines
63+
- [`taco-threshold-automaton`](./dev-docs/taco_threshold_automaton/index.html): This crate defines
4464
the types:
4565
- `GeneralThresholdAutomaton`, which is the most general form of a threshold
4666
automaton. For example, it allows comparisons between variables or guards in
@@ -54,38 +74,36 @@ levels of abstraction, which can be used as inputs to model checkers.
5474

5575
Model checkers and specifications must implement the interfaces defined in the
5676

57-
- [`taco-model-checker`](./taco_model_checker/index.html) crate. This library crate
77+
- [`taco-model-checker`](./dev-docs/taco_model_checker/index.html) crate. This library crate
5878
defines the common interface for model checkers, as well as some useful
5979
preprocessing tools that can apply useful transformations or simplifications
6080
to threshold automata.
6181

6282
TACO already implements 3 algorithms, which are split into their own separate
6383
crates:
6484

65-
- [`taco-acs-model-checker`](./taco_acs_model_checker/index.html): Contains the
85+
- [`taco-acs-model-checker`](./dev-docs/taco_acs_model_checker/index.html): Contains the
6686
implementation of the 'ACS' model checker.
67-
- [`taco-smt-model-checker`](./taco_smt_model_checker/index.html): Contains the
87+
- [`taco-smt-model-checker`](./dev-docs/taco_smt_model_checker/index.html): Contains the
6888
implementation of the 'SMT' model checker.
69-
- [`taco-zcs-model-checker`](./taco_zcs_model_checker/index.html): Contains the
89+
- [`taco-zcs-model-checker`](./dev-docs/taco_zcs_model_checker/index.html): Contains the
7090
implementation of the 'ZCS' model checker.
7191

72-
### Backend and Utility Crates
73-
74-
- [`taco-bdd`](./taco_bdd/index.html) : This library crate implements a common interface
75-
to interact with BDD libraries. Currently it supports
76-
[OxiDD](https://oxidd.net/) and [CUDD](https://github.com/cuddorg/cudd).
77-
- [`taco-cli`](./taco_cli/index.html): The binary crate containing the code of
78-
the TACO Command Line Interface.
79-
- [`taco-display-utils`](./taco_display_utils/index.html): A small library crate for
80-
common helper methods for nicely displaying types.
81-
- [`taco-parser`](./taco_parser/index.html): An interface definition of parsers that can be
82-
used to parse a threshold automaton from different formats. This crate already
83-
contains a parser for `.ta` and `.eta` files that has been introduced by ByMC
84-
[here](https://github.com/konnov/bymc/blob/master/bymc/doc/ta-format.md).
85-
- [`taco-smt-encoder`](./taco_smt_encoder/index.html): This library crate implements
86-
the configuration and setup of connections to SMT solvers. Additionally, it
87-
defines SMT encodings of types of the `threshold-automaton` crate and provides
88-
structures to encode constraints on configurations and paths.
92+
### Summary
93+
94+
| Crate | Current Version | Docs | Description |
95+
| ------------------------ | --------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------- |
96+
| 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 |
97+
| 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 |
98+
| 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 |
99+
| 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 |
100+
| 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 |
101+
| 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 |
102+
| 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 |
103+
| 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 |
104+
| 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 |
105+
| 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 |
106+
| 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 |
89107

90108
(development-setup)=
91109

0 commit comments

Comments
 (0)