new specification format in preparation for liveness by pleich · Pull Request #10 · cispa/TACO

pleich · 2026-09-24T12:36:42Z

This commit adds a new specification format in preparation of the push
towards supporting liveness. The old ReachabilitySpec is removed in
favor of the new more general type. Note that this is a breaking change.
The TACO benchmark files are also updated to remove the ByMC fairness
constraints.

Additionally, major bugs in the interval construction and specification
extraction logic have been fixed. More details can be found in the
included bug reports.

Additionally, this commit includes updates to new Rust and dependency
versions, as well as clippy fixes for the new Rust versions.

This commit has been co-authored and reviewed with the help of AI.
Models that have been used: glm5.3-flash, Fable 5.1, Opus 5.5

This commit adds a new specification format in preparation of the push towards supporting liveness. The old `ReachabilitySpec` is removed in favor of the new more general type. Note that this is a breaking change. The TACO benchmark files are also updated to remove the ByMC fairness constraints. Additionally, major bugs in the interval construction and specification extraction logic have been fixed. More details can be found in the included bug reports. Additionally, this commit includes updates to new Rust and dependency versions, as well as clippy fixes for the new Rust versions. This commit has been co-authored and reviewed with the help of AI. Models that have been used: glm5.3-flash, Fable 5.1, Opus 5.5

Copilot

Copilot review overview

🟡 Changes recommended

The interval correctness bug and additional reporting, test, and documentation issues remain unresolved.

Get a fresh assessment by requesting another Copilot review.

Review effort: Lite
Findings: 1 · 1

Open (2)

Correct integer existence check for open rational intervals · New
Correct example enum variant semantics · New

What changed in this PR

This breaking change replaces the reachability-only specification model with a generalized format, while updating model checkers, interval handling, benchmarks, tooling, and documentation.

Changes:

Adds generalized error specifications and unknown-property reporting.
Fixes specification extraction and interval construction.
Removes benchmark fairness constraints and updates Rust, dependencies, CI, and documentation.
Review identified unresolved interval, reporting, test, and documentation issues.

File	Description
`docs/design-docs/internal-spec.md`	Documents the new specification format; enum examples need correction.
`docs/bug-analysis/README.md`	Adds bug-analysis overview.
`docs/bug-analysis/1-distributivity-reach.md`	Documents reachability extraction issues; contains a grammar issue.
`docs/bug-analysis/0-interval-rounding.md`	Documents interval-rounding issues; contains grammar corrections.
`Dockerfile`	Updates Rust and Fedora images.
`crates/taco-zcs-model-checker/tests/test_mc_full_ta.rs`	Updates ZCS model-checker expectations.
`crates/taco-zcs-model-checker/src/zcs_error_graph.rs`	Handles initial error states and generalized targets.
`crates/taco-zcs-model-checker/src/smt_encoder_steady.rs`	Migrates steady encoding to generalized targets.
`crates/taco-zcs-model-checker/src/paths.rs`	Adapts path checking to new targets.
`crates/taco-threshold-automaton/src/path.rs`	Simplifies checked rule application.
`crates/taco-threshold-automaton/src/lia_threshold_automaton/properties.rs`	Adds constraint helpers and operators.
`crates/taco-threshold-automaton/src/lia_threshold_automaton/general_to_lia.rs`	Updates conversion tests.
`crates/taco-threshold-automaton/src/general_threshold_automaton/builder.rs`	Cleans up error formatting.
`crates/taco-threshold-automaton/src/expressions/properties.rs`	Uses reusable boolean-expression traits.
`crates/taco-threshold-automaton/src/expressions/fraction.rs`	Adds fraction rounding helpers.
`crates/taco-threshold-automaton/src/expressions.rs`	Adds boolean-combination traits and macros.
`crates/taco-smt-model-checker/tests/test_smt_model_checker.rs`	Tests generalized extraction; currently drops extraction errors and unknown properties.
`crates/taco-smt-model-checker/src/smt_encoding.rs`	Migrates SMT reachability encoding.
`crates/taco-smt-model-checker/Cargo.toml`	Updates `itertools`.
`crates/taco-smt-encoder/src/lib.rs`	Improves solver-version parsing.
`crates/taco-smt-encoder/src/expression_encoding.rs`	Adds integer declarations; fresh-variable naming needs correction.
`crates/taco-model-checker/tests/test_preprocessors_on_benchmark.rs`	Migrates preprocessing tests.
`crates/taco-model-checker/tests/test_extract_spec_on_benchmark.rs`	Tests new specification extraction.
`crates/taco-model-checker/src/preprocessing.rs`	Migrates preprocessor APIs.
`crates/taco-model-checker/src/lib.rs`	Introduces generalized model-checker APIs.
`crates/taco-model-checker/src/eltl/remove_negations.rs`	Adds display support for normalized ELTL.
`crates/taco-model-checker/Cargo.toml`	Adds test logging dependency.
`crates/taco-interval-ta/src/lib.rs`	Migrates interval automata to generalized specifications.
`crates/taco-interval-ta/src/interval.rs`	Adds interval inhabitance checks; finite rational bounds are handled incorrectly.
`crates/taco-interval-ta/src/builder/static_interval_order/simple_order_generator.rs`	Generates exact intervals and filters empty intervals.
`crates/taco-interval-ta/src/builder/static_interval_order.rs`	Supports strict and non-strict thresholds.
`crates/taco-interval-ta/src/builder.rs`	Propagates exact-boundary requirements.
`crates/taco-cli/src/cli.rs`	Displays unknown properties in results.
`crates/taco-acs-model-checker/tests/test_mc_full_ta.rs`	Updates ACS model-checker expectations.
`crates/taco-acs-model-checker/tests/test_mc_full_eta.rs`	Skips unsupported liveness checks.
`crates/taco-acs-model-checker/tests/test_error_graph_only.rs`	Migrates error-graph tests.
`crates/taco-acs-model-checker/src/lib.rs`	Adds generalized result reporting; property names are lost in initialization errors.
`crates/taco-acs-model-checker/src/error_graph/spurious_path_checker.rs`	Migrates spurious-path results.
`crates/taco-acs-model-checker/src/error_graph/node.rs`	Migrates error-graph targets.
`crates/taco-acs-model-checker/src/error_graph.rs`	Migrates error-graph specifications.
`crates/taco-acs-model-checker/src/acs_threshold_automaton/index_ctx.rs`	Updates interval tests.
`crates/taco-acs-model-checker/src/acs_threshold_automaton.rs`	Adds guard inspection support.
`CHANGELOG.md`	Records specification and interval changes.
`benchmarks/TACO/random19/p-rs-bosco.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/p-rabc.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/p-rabc-s.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/p-rabc-cr.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/p-kset.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/p-ben-or.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/p-ben-or-nonclean.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/p-ben-or-byz.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/n-rs-bosco.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/n-rabc.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/n-rabc-s.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/n-rabc-cr.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/n-kset.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/n-ben-or.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/n-ben-or-nonclean.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/n-ben-or-byz.ta`	Removes fairness constraints.
`benchmarks/TACO/random19/ben-or.ta`	Removes fairness constraints.
`benchmarks/TACO/popl17-fmsd17/bcast-byz.ta`	Removes fairness constraints.
`benchmarks/TACO/popl17-fmsd17/asyn-guer01-nbac.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/ta-(handcoded)/strb.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/ta-(handcoded)/nbacr.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/ta-(handcoded)/nbacg.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/ta-(handcoded)/frb.ta`	Removes fairness constraints; an adjacent comment still describes removed constraints.
`benchmarks/TACO/isola18/ta-(handcoded)/cf1s.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/ta-(handcoded)/cc.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/ta-(handcoded)/c1cs.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/ta-(handcoded)/bosco.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/ta-(handcoded)/bcrb.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/ta-(handcoded)/aba.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/promela/strb.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/promela/nbacg.ta`	Removes fairness constraints.
`benchmarks/TACO/isola18/promela/frb.ta`	Removes fairness constraints.
`benchmarks/TACO/concur14/bcast-folklore-crash.ta`	Removes fairness constraints.
`benchmarks/TACO/concur14/bcast-byz.ta`	Removes fairness constraints.
`benchmarks/TACO/cav15/promela/strb-bcast-byz.ta`	Removes fairness constraints.
`benchmarks/TACO/cav15/promela/nbacg-asyn-guer01-nbac.ta`	Removes fairness constraints.
`benchmarks/TACO/cav15/promela/frb-bcast-folklore-crash.ta`	Removes fairness constraints.
`.github/workflows/test.yml`	Updates CI tool versions.
`.github/workflows/static.yml`	Updates documentation workflow versions.
`.github/workflows/release.yml`	Updates release workflow actions.

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

pleich added 5 commits September 24, 2026 11:40

fixup! new specification format in preparation for liveness

5cf096c

CI maintenance

850b7e7

fix cargo about

cc19780

fix compatibility with new cvc5 versions

e8e091d

pleich requested a lite review from Copilot September 24, 2026 12:36

Copilot started reviewing on behalf of pleich September 24, 2026 12:37

View session

Copilot AI reviewed Sep 24, 2026

View reviewed changes

Comment thread crates/taco-interval-ta/src/interval.rs

Comment thread docs/design-docs/internal-spec.md

pleich merged commit 255172b into cispa:main Sep 24, 2026
6 checks passed

Navigation Menu

Repository navigation

new specification format in preparation for liveness - #10

new specification format in preparation for liveness#10
pleich merged 5 commits into
cispa:mainfrom
pleich:main

pleich commented Sep 24, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

pleich commented Sep 24, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Copilot review overview

🟡 Changes recommended

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants