improve: documentation on preprocessors, upgrade Rust version

.github/workflows/static.yml

@@ -10,7 +10,7 @@ on:
 
 env:
   CARGO_TERM_COLOR: always
-  RUST_VERSION: "1.92.0"
+  RUST_VERSION: "1.94.0"
 
 # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:

.github/workflows/test.yml

@@ -7,7 +7,7 @@ on:
 
 env:
   CARGO_TERM_COLOR: always
-  RUST_VERSION: "1.92.0"
+  RUST_VERSION: "1.94.0"
 
 jobs:
   # Check formatting & basic code validity

CHANGELOG.md

@@ -9,11 +9,17 @@
 
 ### Fixed
 
+- grant information for the development of TACO (#6)
 - 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)
 
+### Added
+
+- Elaborate on the function of the different preprocessors (#6)
+- upgrade CI pipeline & Dockerfile to Rust 1.94
+
 ## [v0.1.0]
 
 ### Added

Dockerfile

@@ -1,4 +1,4 @@
-FROM rust:1.92-slim AS BUILD
+FROM rust:1.94-slim AS BUILD
 
 RUN apt update && apt-get install -y --no-install-recommends\
         # CUDD build dependencies

crates/taco-model-checker/src/lib.rs

@@ -224,14 +224,17 @@ where
 /// Result type for a model checking run
 #[derive(Debug, Clone, PartialEq)]
 pub enum ModelCheckerResult {
-    /// Threshold automaton fulfills all the specification
+    /// Threshold automaton fulfills all specifications
     SAFE,
     /// Threshold automaton does not fulfill the specification
+    ///
     /// The string contains the name of the violated specification and the path
     /// is a concrete error path that serves as an example for the violation
     UNSAFE(Vec<(String, Box<Path>)>),
-    /// The model checker could not determine if the specification holds or not.
-    /// The vector contains the names of the specifications that are unknown
+    /// Model checker could not determine if the specification holds or not
+    ///
+    /// The vector contains the names of the specifications for which the result
+    /// could not be determined.
     UNKNOWN(Vec<String>),
 }
 

docs/about.md

@@ -20,7 +20,8 @@ and [SnT](https://www.uni.lu/snt-en/) at
 - 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)
+Foundation (DFG) grant 513487900, German Research Foundation (DFG) grant
+513487900, and the Luxembourg National Research Fund (FNR)
 grant C22/IS/17432184.
 
 For the purpose of open access, and in fulfilment of the obligations arising

docs/landing-page.tex

@@ -80,7 +80,8 @@
     This includes self-loops of the TA that do not have any effect (i.e., they do not change the value of any variable), or transition guards that are trivial because they will always be satisfied for the given resilience condition specified in the TA.
 
     Moreover, if TACO can statically determine that some locations are never reachable because they are empty initially and there are no incoming transitions from non-empty locations, then we completely remove these locations from the TA when checking the given property.
-    Note that this may depend on the given specification, as it may specify that some of the initial locations should be empty.
+    Note that this may depend on the given specification, as it may specify that some of the initial locations should be empty. 
+    You can find more information on the purpose of different preprocessors in \cref{specifying-preprocessors}.
 
     \subsection{Code Quality}
     The goal of a model checker is to verify the safety of a protocol, thereby increasing trust in its correctness.

docs/usage-cli/advanced-configuration.md

@@ -8,28 +8,57 @@ configuration file in `.yaml` format.
 
 The file can then be passed to TACO by using the `-c`/`--config-file` flag.
 
+(specifying-preprocessors)=
+
 ### Specifying Preprocessors
 
 Before model checking a threshold automaton, TACO will use different
-preprocessors to simplify the automaton. Currently, the following preprocessors
-are available:
-
-- `DropSelfLoops`: Removes self-loops that do not contain variable updates
-- `DropUnreachableLocations`: Constructs the underlying directed graph of the
-  automaton from the initial states and removes locations that cannot be
-  reached in the graph.
-- `ReplaceTrivialGuardsStatic`: Replaces rule guards which always be enabled
+preprocessors to simplify the automaton. To understand the usefulness of
+preprocessors, it is important to note that the preprocessing is not only
+executed once per automaton but instead at least once per property that is being
+verified.
+
+This can be helpful because many correctness properties have the form "If no
+process starts with input 0, then the algorithm does not accept 0". When
+verifying such a property, one assumes that no process starts in the location
+corresponding to an input of 0. This means that in the exploration, one does not
+need to consider this input location (assuming there is no incoming transition).
+In this case, the location would be removed by the preprocessor
+`DropUnreachableLocations`.
+
+Currently, the following preprocessors are available:
+
+- `DropSelfLoops`: Removes self-loops that do not contain variable updates. Such
+  loops are not useful as they do not change the configuration. Therefore, they
+  can be safely disregarded during verification.
+- `DropUnreachableLocations`: This preprocessor does reachability analysis: It
+  constructs the underlying directed graph of the automaton from the initial
+  states (ignoring rule guards) and removes locations that cannot be reached in
+  the graph. Locations that are removed cannot be reached from any of the
+  initial locations and can therefore be safely disregarded.
+- `ReplaceTrivialGuardsStatic`: Replaces rule guards, which are always enabled,
   with `true`. This preprocessor only works for some known patterns.
-- `ReplaceTrivialGuardsSMT`: Replaces rule guards which are always enabled
+- `ReplaceTrivialGuardsSMT`: Replaces rule guards, which are always enabled,
   with `true`. This preprocessor uses the SMT solver to determine which guards
-  can be true.
-- `RemoveUnusedVariables`: Removes variables which do not appear in any rule.
+  can be true. The outcome of SMT queries for a specific guard is cached during
+  preprocessing to decrease the number of SMT queries.
+- `RemoveUnusedVariables`: Removes any variables that do not appear in any rule.
+  This preprocessor is mostly useful after other preprocessors have already
+  eliminated locations and rules.
 - `DropUnsatisfiableRules`: Removes rules with guards that can never be
-  satisfied.
+  satisfied. Analogous to `ReplaceTrivialGuardsSMT`, this preprocessor uses SMT
+  solvers to determine whether a guard can be satisfied under the current
+  resilience condition. If this is not the case, the rule is removed.
+  This preprocessor has not proven effective in practice. Therefore, it is
+  disabled by default.
 - `CollapseLocations`: Collapse locations that all have the same incoming rules.
 - `CheckInitCondSatSMT`: Checks whether the initial conditions of a threshold
   automaton are satisfiable first.
 
+(specifying-preprocessors)=
+
+#### Specifying Preprocessors
+
 By default TACO will use `ReplaceTrivialGuardsSMT`,`DropSelfLoops`,
 `DropUnreachableLocations`, `CheckInitCondSatSMT` and `RemoveUnusedVariables`.
 Note that preprocessors that rely on the SMT solver, like
@@ -78,7 +107,7 @@ The example configuration above instructs TACO to start an SMT solver by using
 the command `z3` with arguments `--smt2` and `-in` and then sets the `parallel`
 option of the solver to `true`.
 
-### Configuring the BDD backend
+### Configuring the BDD Backend
 
 Analogously to the configuration for SMT solvers, you can also configure the BDD
 backend. For example, if you want to try the performance of TACO's ZCS model