fix: doc images as .webp, naming

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]
 

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) <a href="https://orcid.org/0009-0008-6117-318X"><img src="./resources/ORCID_iD.png" class="align-center" width="17.5px"> <a href="https://github.com/pleich"><img src="./resources/github-mark.png" class="align-center only-light" width="17.5px"><img src="./resources/github-mark-white.png" class="align-center only-dark" width="17.5px">
-- [Tom Baumeister](mailto:tom.baumeister@cispa.de) <a href="https://orcid.org/0009-0009-8539-6246"><img src="./resources/ORCID_iD.png" class="align-center" width="17.5px">
+- [Paul Eichler](mailto:paul.eichler@cispa.de) <a href="https://orcid.org/0009-0008-6117-318X"><img src="./resources/ORCID_iD.webp" class="align-center" width="17.5px"></a> <a href="https://github.com/pleich"><img src="./resources/github-mark.webp" class="align-center only-light" width="17.5px"><img src="./resources/github-mark-white.webp" class="align-center only-dark" width="17.5px"></a>
+- [Tom Baumeister](mailto:tom.baumeister@cispa.de) <a href="https://orcid.org/0009-0009-8539-6246"><img src="./resources/ORCID_iD.webp" class="align-center" width="17.5px"></a>
 - Peter Gastauer
-- Supervisor: Swen Jacobs <a href="https://orcid.org/0000-0002-9051-4050"><img src="./resources/ORCID_iD.png" class="align-center" width="17.5px">
+- Supervisor: Swen Jacobs <a href="https://orcid.org/0000-0002-9051-4050"><img src="./resources/ORCID_iD.webp" class="align-center" width="17.5px"></a>
 
 and [SnT](https://www.uni.lu/snt-en/) at
 [Luxembourg University](https://www.uni.lu):
 
-- Mouhammad Sakr (now: American University of Beirut) <a href="https://orcid.org/0000-0002-5160-0327"><img src="./resources/ORCID_iD.png" class="align-center" width="17.5px">
+- Mouhammad Sakr (now: American University of Beirut) <a href="https://orcid.org/0000-0002-5160-0327"><img src="./resources/ORCID_iD.webp" class="align-center" width="17.5px"></a>
 - Mahboubeh Kalateh Dowlati
-- Kürşat Aker <a href="https://orcid.org/0009-0005-2734-1125"><img src="./resources/ORCID_iD.png" class="align-center" width="17.5px">
-- Supervisor: Markus Völp <a href="https://orcid.org/0000-0002-8020-4446"><img src="./resources/ORCID_iD.png" class="align-center" width="17.5px">
+- Kürşat Aker <a href="https://orcid.org/0009-0005-2734-1125"><img src="./resources/ORCID_iD.webp" class="align-center" width="17.5px"></a>
+- Supervisor: Markus Völp <a href="https://orcid.org/0000-0002-8020-4446"><img src="./resources/ORCID_iD.webp" class="align-center" width="17.5px"></a>
 
 The development of TACO was funded in part by the German Research
 Foundation (DFG) grant 513487900 and the Luxembourg National Research Fund (FNR)

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

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.
 

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

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}.

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:\\

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}
 

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}

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