diff --git a/CHANGELOG.md b/CHANGELOG.md index 6d09972..775eb8e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,7 +9,9 @@ ### Fixed -- replaced `localhost` reference in `sitemap.xml` and `robots.txt` (#1) +- doc images as `.webp` and naming of TACO (toolsuite / model checker) + consistent (#3) +- replaced `localhost` reference in `sitemap.xml` and `robots.txt` (#2) ## [v0.1.0] diff --git a/docs/about.md b/docs/about.md index 4b777d6..de34898 100644 --- a/docs/about.md +++ b/docs/about.md @@ -1,25 +1,23 @@ # About -## TACO - -The TACO model checker has been developed by the +The TACO toolsuite has been developed by the [Rigorous Analysis and Design Group (RAD)](https://cispa.de/en/research/groups/jacobs) at the [CISPA - Helmholtz Center for Information Security](https://cispa.de/): -- [Paul Eichler](mailto:paul.eichler@cispa.de) -- [Tom Baumeister](mailto:tom.baumeister@cispa.de) +- [Paul Eichler](mailto:paul.eichler@cispa.de) +- [Tom Baumeister](mailto:tom.baumeister@cispa.de) - Peter Gastauer -- Supervisor: Swen Jacobs +- Supervisor: Swen Jacobs and [SnT](https://www.uni.lu/snt-en/) at [Luxembourg University](https://www.uni.lu): -- Mouhammad Sakr (now: American University of Beirut) +- Mouhammad Sakr (now: American University of Beirut) - Mahboubeh Kalateh Dowlati -- Kürşat Aker -- Supervisor: Markus Völp +- Kürşat Aker +- Supervisor: Markus Völp The development of TACO was funded in part by the German Research Foundation (DFG) grant 513487900 and the Luxembourg National Research Fund (FNR) diff --git a/docs/dev-docs.md b/docs/dev-docs.md index 3d1ecd9..c858936 100644 --- a/docs/dev-docs.md +++ b/docs/dev-docs.md @@ -23,12 +23,12 @@ directory. :::{tip} Clicking on the name of a crate will forward you to Rust documentation -of the crate, which contains the description of the external API of the crate, -as well as more details on the implementation. +of the crate, containing the API documentation as well as implementation +details. -These parts of the documentation will be directly derived from the -[Rust doc comments](https://doc.rust-lang.org/rust-by-example/meta/doc.html) -on the source code. +Note that the documentation is also available on [docs.rs](https://docs.rs). +However, our internal version also contains the documentation for private types, +giving you more insights into the implementation details. ::: ### Threshold Automaton Representations diff --git a/docs/landing-page.tex b/docs/landing-page.tex index ca3f968..75c429a 100644 --- a/docs/landing-page.tex +++ b/docs/landing-page.tex @@ -12,13 +12,13 @@ Welcome to the documentation of the Threshold Automata for COnsensus (TACO) toolsuite! \begin{abstract} - TACO is a model checker designed to verify distributed protocols, for example, byzantine consensus protocols, modeled as a threshold automata (TA). + TACO is a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms, for example, byzantine consensus protocols, modeled as threshold automata (TA). + Currently, TACO implements three model checkers for threshold automata, two of which can also be used for the verification of so called extended threshold automata (ETA). It can be used as a completely push-button tool - supply it with a TA and a specification, and it will automatically choose a model checking algorithm and check whether the specification is satisfied. - This allows you to model check threshold automata (and distributed algorithms in general) even if you are not an expert. + This allows you to verify threshold automata (and distributed algorithms in general) even if you are not an expert. - TACO features an extensively documented API, both for internal procedures as well as for the CLI. - In case of user errors such as faulty inputs, or if a given input is not supported by the chosen algorithm, it provides easy to read error messages in a user- and infrastructure-friendly output format via Rust's log trait. + Additionally, TACO is a modular, extensible, and well-documented framework for developing algorithms and tools for threshold automata. All of TACO's components are openly available and ready to use on \href{https://crates.io}{crates.io}. \end{abstract} \section{Organization of the Documentation} @@ -46,7 +46,7 @@ \begin{figure}[h] \centering - \includegraphics[width=0.9\textwidth]{resources/architecture-diagram} + \includegraphics[width=\textwidth]{resources/architecture-diagram.webp} \caption{Architecture of the TACO toolsuite.}\label{fig:architecture} \end{figure} @@ -65,7 +65,7 @@ While TACO can be used as a push-button tool, based only on an input TA and a specification, its behavior can be guided through a wealth of parameters. First, you can of course choose which of the three model checking algorithms to use. - Moreover, TACO allows for the fine-grained configuration of the underlying SMT solvers and BDD managers, for example to choose SMT solving heuristics. + Moreover, TACO allows for the fine-grained configuration of the underlying SMT solvers and BDD managers, for example, to choose SMT solving heuristics. For specifications composed of multiple properties, you can choose whether TACO should terminate after finding the first violation or whether it should continue until all properties are verified. Additionally, the ZCS approach can optionally be used as a heuristic that only tries to verify safety by checking if the error graph is empty. @@ -83,9 +83,9 @@ Note that this may depend on the given specification, as it may specify that some of the initial locations should be empty. \subsection{Code Quality} - The goal of a model checker is to verify safety of a protocol, thereby increasing trust in its correctness. + The goal of a model checker is to verify the safety of a protocol, thereby increasing trust in its correctness. However, we still need to trust the verifier. - While we have not proven the correctness of TACO in a proof assistant, TACO uses extensive testing (around 97\% of line coverage at the time of writing) and uses software engineering best practices, such as code reviews and linting to maintain a (somehwhat) trust worthy code base. + While we have not proven the correctness of TACO in a proof assistant, TACO uses extensive testing (around 97\% of line coverage at the time of writing) and uses software engineering best practices, such as code reviews and linting to maintain a (somewhat) trustworthy code base. Additionally, TACO is written entirely in the safe fragment of Rust (simply called \emph{safe Rust}), guaranteeing memory and type safety while not adding major overhead and allowing for low-level optimizations. @@ -94,7 +94,7 @@ Our goal with the design of TACO was not only to provide an efficient implementation of model checking algorithms but also to enable others to write tools for threshold automata. In this spirit, we designed TACO in a highly modular fashion. - Most major components, such as parser and preprocessor, or different TA representations and model checking algorithms, are separated into individual Rust crates and specific features are guarded by feature flags. + Most major components, such as parser and preprocessor, or different TA representations and model checking algorithms, are separated into individual Rust crates, and specific features are guarded by feature flags. This design for example allows you to easily create a new user interface by integrating the parser and one of the model checkers while not importing our CLI and the other model checking algorithms. Similarly, new specification formats can simply be implemented by implementing the existing parser trait. diff --git a/docs/myst.yml b/docs/myst.yml index c81a4b7..219894f 100644 --- a/docs/myst.yml +++ b/docs/myst.yml @@ -2,7 +2,7 @@ version: 1 project: id: 1ef2b476-ab7f-4869-bd13-7e17f203a02e - title: "TACO Model Checker" + title: "TACO Toolsuite" subtitle: "Model Checker for Threshold Automata" description: | "TACO is an automatic verification toolsuite for the development and \ @@ -84,5 +84,6 @@ site: options: numbered_references: true style: ./resources/style.css - logo: ./resources/taco-org.png - favicon: ./resources/taco.png + logo: ./resources/taco-logo.webp + logo_text: "TACO Toolsuite for Threshold Automata" + favicon: ./resources/taco-favicon.webp diff --git a/docs/resources/ORCID_iD.webp b/docs/resources/ORCID_iD.webp new file mode 100644 index 0000000..8433747 Binary files /dev/null and b/docs/resources/ORCID_iD.webp differ diff --git a/docs/resources/architecture-diagram.png b/docs/resources/architecture-diagram.png deleted file mode 100644 index ed40df2..0000000 Binary files a/docs/resources/architecture-diagram.png and /dev/null differ diff --git a/docs/resources/architecture-diagram.webp b/docs/resources/architecture-diagram.webp new file mode 100644 index 0000000..59aefe8 Binary files /dev/null and b/docs/resources/architecture-diagram.webp differ diff --git a/docs/resources/flood-min-pseudo.png b/docs/resources/flood-min-pseudo.png deleted file mode 100644 index 3269236..0000000 Binary files a/docs/resources/flood-min-pseudo.png and /dev/null differ diff --git a/docs/resources/flood-min-pseudo.webp b/docs/resources/flood-min-pseudo.webp new file mode 100644 index 0000000..35761dd Binary files /dev/null and b/docs/resources/flood-min-pseudo.webp differ diff --git a/docs/resources/flood-min-ta.png b/docs/resources/flood-min-ta.png deleted file mode 100644 index 4d43d4f..0000000 Binary files a/docs/resources/flood-min-ta.png and /dev/null differ diff --git a/docs/resources/flood-min-ta.webp b/docs/resources/flood-min-ta.webp new file mode 100644 index 0000000..5764448 Binary files /dev/null and b/docs/resources/flood-min-ta.webp differ diff --git a/docs/resources/github-mark-white.webp b/docs/resources/github-mark-white.webp new file mode 100644 index 0000000..c7b9d7e Binary files /dev/null and b/docs/resources/github-mark-white.webp differ diff --git a/docs/resources/github-mark.webp b/docs/resources/github-mark.webp new file mode 100644 index 0000000..dccdbb5 Binary files /dev/null and b/docs/resources/github-mark.webp differ diff --git a/docs/resources/taco-favicon.webp b/docs/resources/taco-favicon.webp new file mode 100644 index 0000000..481f4a1 Binary files /dev/null and b/docs/resources/taco-favicon.webp differ diff --git a/docs/resources/taco-logo.webp b/docs/resources/taco-logo.webp new file mode 100644 index 0000000..c25c015 Binary files /dev/null and b/docs/resources/taco-logo.webp differ diff --git a/docs/resources/taco-small.png b/docs/resources/taco-small.png deleted file mode 100644 index 411f011..0000000 Binary files a/docs/resources/taco-small.png and /dev/null differ diff --git a/docs/theoretical-background/algorithms/bdd-based-alg.tex b/docs/theoretical-background/algorithms/bdd-based-alg.tex index 0c7f951..570589a 100644 --- a/docs/theoretical-background/algorithms/bdd-based-alg.tex +++ b/docs/theoretical-background/algorithms/bdd-based-alg.tex @@ -2,7 +2,7 @@ \subsection{ZCS Model Checking Algorithm}\label{alg:bdd} \begin{figure}[h] \centering - \includegraphics[width=0.8\textwidth]{./resources/zcs-algorithm.png} + \includegraphics[width=\textwidth]{./resources/zcs-algorithm.webp} \caption{Workflow of the ZCS model checking algorithm.} \end{figure} @@ -33,5 +33,5 @@ \subsection{ZCS Model Checking Algorithm}\label{alg:bdd} \textbf{Usage.} To use the ZCS model checking algorithm with TACO, the user needs to specify the option \texttt{zcs} when invoking the tool from the command line. Additionally, the user can choose a heuristic for exploring the error graph depending on the input TA by specifying the option \texttt{--heuristic}. -Since TACO automatically detects whether the input TA is a CTA or an ETA, this flag does not need to be set by the user to choose a suitable heuristic. +Since TACO automatically detects whether the input TA is a MTA or an ETA, this flag does not need to be set by the user to choose a suitable heuristic. However, if the user wants to check only whether the error graph is empty, they can set the flag to \texttt{empty-error-graph-heuristic}. diff --git a/docs/theoretical-background/algorithms/smt-based-alg.tex b/docs/theoretical-background/algorithms/smt-based-alg.tex index 52fe22c..ae42ad0 100644 --- a/docs/theoretical-background/algorithms/smt-based-alg.tex +++ b/docs/theoretical-background/algorithms/smt-based-alg.tex @@ -2,16 +2,16 @@ \subsection{SMT Model Checking Algorithm} \begin{figure}[h] \centering - \includegraphics[width=0.9\textwidth]{./resources/smt-algorithm.png} + \includegraphics[width=\textwidth]{./resources/smt-algorithm.webp} \caption{Architecture of the SMT-based model checking algorithm.}\label{fig:alg-smt} \end{figure} -Balasubramanian et al.~\citep{Balasubramanian20} showed that the reachability problem for CTA can be reduced to deciding the satisfiability of an SMT formula. -More precisely, they construct an existential Presburger arithmetic formula $\phi_{REACH}(\sigma,\sigma')$ such that $\phi_{REACH}(\sigma,\sigma')$ holds if and only if $\sigma'$ is reachable from $\sigma$ for the given CTA. +Balasubramanian et al.~\citep{Balasubramanian20} showed that the reachability problem for MTA can be reduced to deciding the satisfiability of an SMT formula. +More precisely, they construct an existential Presburger arithmetic formula $\phi_{REACH}(\sigma,\sigma')$ such that $\phi_{REACH}(\sigma,\sigma')$ holds if and only if $\sigma'$ is reachable from $\sigma$ for the given MTA. A central notion in this construction is the \emph{context} of a configuration $\sigma$, defined as the set of lower guards that evaluate to true together with the upper guards that evaluate to false. -A CTA path is called \emph{steady} if all its configurations have the same context. -The key idea underlying the SMT-based approach is that any CTA execution with $k$ guards can be represented as the concatenation of at most $k+1$ steady paths~\citep{Balasubramanian20}. +A MTA path is called \emph{steady} if all its configurations have the same context. +The key idea underlying the SMT-based approach is that any MTA execution with $k$ guards can be represented as the concatenation of at most $k+1$ steady paths~\citep{Balasubramanian20}. Therefore, for each steady path, the formula $\phi_{REACH}(\sigma,\sigma')$ encodes several constraints: the number of times each rule is fired, the effect on the number of processes in each location, the changes to shared variables, and that each fired rule is reachable via a sequence of rules where the target location of one rule provides the source location required to fire the next, starting from a location that initially contains a process~( ``firable'' chain of rules). Additional base constraints ensure that parameters, total process counts, and the guard context remain consistent along the path. Formally, the construction yields:\\ diff --git a/docs/theoretical-background/algorithms/wsts-based-alg.tex b/docs/theoretical-background/algorithms/wsts-based-alg.tex index ba0709c..fabeda4 100644 --- a/docs/theoretical-background/algorithms/wsts-based-alg.tex +++ b/docs/theoretical-background/algorithms/wsts-based-alg.tex @@ -2,7 +2,7 @@ \subsection{ACS Model Checking Algorithm}\label{sec:alg-wsts} \begin{figure}[h] \centering - \includegraphics{./resources/acs-model-checking.png} + \includegraphics[width=\textwidth]{./resources/acs-model-checking.webp} \caption{Workflow of the ACS model checking algorithm.}\label{fig:acs-model-checking} \end{figure} diff --git a/docs/theoretical-background/motivating_example.tex b/docs/theoretical-background/motivating_example.tex index 39a9ae8..6dac0e6 100644 --- a/docs/theoretical-background/motivating_example.tex +++ b/docs/theoretical-background/motivating_example.tex @@ -42,7 +42,7 @@ \section{Threshold Automata}\label{sec:TA} Most commonly, the parameter variables are $\Pi = \{n,t,f\}$, where $n$ is the number of processes, $t$ is a bound on the number of faulty processes, and $f$ is the actual number of faulty processes. This allows $RC$ to express assumptions about the fraction of faulty processes in the system, e.g., $RC = n > 3t\, \land\, t \geq f$. -If $\vup \in \Nat_0^{|\Shared|}$ and no variables are reset, then the TA is called a \emph{canonical TA} (CTA). +If $\vup \in \Nat_0^{|\Shared|}$ and no variables are reset, then the TA is called a \emph{monotonic TA} (MTA). Otherwise we call it an \emph{extended TA} (ETA)\citep{BaumeisterEJSV24}. Note that rechability is in general undecidable for ETA~\citep{Kukovec0W18,BaumeisterEJSV24}. @@ -69,7 +69,7 @@ \subsection{Semantics} \vspace{-2em} \begin{figure}[h] \centering - \includegraphics[width=0.8\textwidth]{resources/flood-min-pseudo} + \includegraphics[width=0.6\textwidth]{resources/flood-min-pseudo.webp} \caption{Pseudocode of a reliable broadcast protocol.}\label{fig:alg-floodmin} \end{figure} \vspace{-1.5em} @@ -83,7 +83,7 @@ \subsection{Semantics} \vspace{-2em} \begin{figure}[h] \centering - \includegraphics[width=0.7\textwidth]{resources/flood-min-ta} + \includegraphics[width=0.6\textwidth]{resources/flood-min-ta.webp} \caption{Threshold automaton of the algorithm in Figure~\ref{fig:alg-floodmin}.}\label{fig:ta-floodmin} \end{figure} \vspace{-1.5em} diff --git a/docs/theoretical-background/resources/acs-model-checking.png b/docs/theoretical-background/resources/acs-model-checking.png deleted file mode 100644 index bc52563..0000000 Binary files a/docs/theoretical-background/resources/acs-model-checking.png and /dev/null differ diff --git a/docs/theoretical-background/resources/acs-model-checking.webp b/docs/theoretical-background/resources/acs-model-checking.webp new file mode 100644 index 0000000..268604c Binary files /dev/null and b/docs/theoretical-background/resources/acs-model-checking.webp differ diff --git a/docs/theoretical-background/resources/smt-algorithm.png b/docs/theoretical-background/resources/smt-algorithm.png deleted file mode 100644 index 1ce1c9b..0000000 Binary files a/docs/theoretical-background/resources/smt-algorithm.png and /dev/null differ diff --git a/docs/theoretical-background/resources/smt-algorithm.webp b/docs/theoretical-background/resources/smt-algorithm.webp new file mode 100644 index 0000000..d9528d8 Binary files /dev/null and b/docs/theoretical-background/resources/smt-algorithm.webp differ diff --git a/docs/theoretical-background/resources/zcs-algorithm.png b/docs/theoretical-background/resources/zcs-algorithm.png deleted file mode 100644 index 6ceec4d..0000000 Binary files a/docs/theoretical-background/resources/zcs-algorithm.png and /dev/null differ diff --git a/docs/theoretical-background/resources/zcs-algorithm.webp b/docs/theoretical-background/resources/zcs-algorithm.webp new file mode 100644 index 0000000..76f36e5 Binary files /dev/null and b/docs/theoretical-background/resources/zcs-algorithm.webp differ diff --git a/docs/usage-cli/install.md b/docs/usage-cli/install.md index 156c103..439408a 100644 --- a/docs/usage-cli/install.md +++ b/docs/usage-cli/install.md @@ -8,7 +8,7 @@ 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](github.com/cvc5/cvc5) and/or [Z3](https://github.com/Z3Prover/z3). +[CVC5](https://github.com/cvc5/cvc5) and/or [Z3](https://github.com/Z3Prover/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