From 125904a4b1be2057a1d9a4a3269c28d4c3cd934b Mon Sep 17 00:00:00 2001 From: Paul Eichler Date: Fri, 20 Mar 2026 15:05:46 +0100 Subject: [PATCH 1/2] improve: documentation on preprocessors, upgrade Rust version This commit - improves the documentation on the preprocessors - fixes the grant information in the about page - upgrades the CI and Dockerfile to the latest Rust version --- .github/workflows/static.yml | 2 +- .github/workflows/test.yml | 2 +- CHANGELOG.md | 6 +++ Dockerfile | 2 +- crates/taco-model-checker/src/lib.rs | 9 ++-- docs/about.md | 3 +- docs/landing-page.tex | 3 +- docs/usage-cli/advanced-configuration.md | 55 ++++++++++++++++++------ 8 files changed, 61 insertions(+), 21 deletions(-) diff --git a/.github/workflows/static.yml b/.github/workflows/static.yml index dbc3e8f..e45fbe4 100644 --- a/.github/workflows/static.yml +++ b/.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: diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index f1f2e9d..42db2db 100644 --- a/.github/workflows/test.yml +++ b/.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 diff --git a/CHANGELOG.md b/CHANGELOG.md index e940323..2c23669 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/Dockerfile b/Dockerfile index 0164c98..7e9b017 100644 --- a/Dockerfile +++ b/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 diff --git a/crates/taco-model-checker/src/lib.rs b/crates/taco-model-checker/src/lib.rs index 3f6e79d..aa822cf 100644 --- a/crates/taco-model-checker/src/lib.rs +++ b/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)>), - /// 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), } diff --git a/docs/about.md b/docs/about.md index de34898..7f60eb9 100644 --- a/docs/about.md +++ b/docs/about.md @@ -20,7 +20,8 @@ and [SnT](https://www.uni.lu/snt-en/) at - 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) +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 diff --git a/docs/landing-page.tex b/docs/landing-page.tex index 75c429a..ba6fe88 100644 --- a/docs/landing-page.tex +++ b/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{preprocessors}. \subsection{Code Quality} The goal of a model checker is to verify the safety of a protocol, thereby increasing trust in its correctness. diff --git a/docs/usage-cli/advanced-configuration.md b/docs/usage-cli/advanced-configuration.md index 9717c9e..d495163 100644 --- a/docs/usage-cli/advanced-configuration.md +++ b/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 preprocess 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. Analog 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 From 055e7148db95c9e6803e4e741f51d7395bdb6f0e Mon Sep 17 00:00:00 2001 From: Paul Eichler Date: Thu, 2 Apr 2026 17:18:34 +0200 Subject: [PATCH 2/2] fixup! improve: documentation on preprocessors, upgrade Rust version --- docs/landing-page.tex | 2 +- docs/usage-cli/advanced-configuration.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/landing-page.tex b/docs/landing-page.tex index ba6fe88..40d62b1 100644 --- a/docs/landing-page.tex +++ b/docs/landing-page.tex @@ -81,7 +81,7 @@ 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. - You can find more information on the purpose of different preprocessors in \cref{preprocessors}. + 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. diff --git a/docs/usage-cli/advanced-configuration.md b/docs/usage-cli/advanced-configuration.md index d495163..9229345 100644 --- a/docs/usage-cli/advanced-configuration.md +++ b/docs/usage-cli/advanced-configuration.md @@ -31,7 +31,7 @@ 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 preprocess does reachability analysis: It +- `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 @@ -46,7 +46,7 @@ Currently, the following preprocessors are available: This preprocessor is mostly useful after other preprocessors have already eliminated locations and rules. - `DropUnsatisfiableRules`: Removes rules with guards that can never be - satisfied. Analog to `ReplaceTrivialGuardsSMT`, this preprocessor uses SMT + 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