Implement stable failures and impossible futures refinement

[mlaveaux]

We are still missing failures-divergences refinement due to the divergence check. Furthermore, divergence preserving branching bisimulation would be necessary to preprocess stable failures refinement. Finally, the optimisation of impossible futures are still missing.

[Copilot]

Pull request overview

This PR extends the refinement checking pipeline to support stable failures and impossible futures refinement, including preprocessing changes and counterexample/formula generation updates.

Changes:

• Adds new refinement variants (StableFailures, ImpossibleFutures) and threads an exploration strategy through the refines entrypoint.
• Refactors the antichain-based refinement core into a generic checker and adds/refines refusal/future counterexample construction.
• Improves/extends supporting utilities (VecSet ops, random BDD construction, doc updates) and updates CLI wiring.

Reviewed changes

Copilot reviewed 10 out of 10 changed files in this pull request and generated 8 comments.

Show a summary per file

File	Description
tools/lts/src/main.rs	Passes ExplorationStrategy into refinement checking from the CLI tool.
crates/vpg/src/translate.rs	Updates regular-formula translation docs/logic and iteration conversion helper.
crates/symbolic/src/random_bdd.rs	Refactors BDD cube construction and changes error type to OutOfMemory.
crates/refinement/src/refinement.rs	Adds new refinement types + preprocessing flow; centralizes exploration strategy and dispatch.
crates/refinement/src/lib.rs	Exposes new impossible futures module via re-exports.
crates/refinement/src/impossible_futures.rs	Introduces impossible futures refinement algorithm implementation.
crates/refinement/src/failures_refinement.rs	Refactors refinement core into is_refinement_generic, adds stable failures refusal check + new tests.
crates/refinement/src/counterexample_formula.rs	Extends counterexample representation and formula generation for stable failures/impossible futures.
crates/reduction/src/simple_block_partition.rs	Makes block_number available outside tests (needed by new preprocessing path).
crates/collections/src/vecset.rs	Adds from_iter, difference, extend, and switches to sort_unstable + adds tests.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

You can also share your feedback on Copilot code review. Take the survey.

[Copilot]

Pull request overview

This PR extends the refinement-checking tooling by adding stable failures and impossible futures refinement support, refactoring the existing failures/trace refinement implementation, and updating related utilities (LTS builders, quotienting, BDD helpers, and tests) to support the new behavior.

Changes:

• Add StableFailures and ImpossibleFutures refinement types with counterexample generation support and preprocessing hooks.
• Refactor failures/trace checking into a generic antichain-based refinement core and extend counterexample formula generation for the new refinement relations.
• Update supporting utilities (tau/hidden label mapping, quotienting, random generators, and CLI integration) and add/adjust tests.

Reviewed changes

Copilot reviewed 17 out of 18 changed files in this pull request and generated 15 comments.

Show a summary per file

File	Description
tools/mcrl2/Cargo.lock	Updates Rust dependency lock entries (e.g., toml, winnow).
tools/lts/src/main.rs	Wires ExplorationStrategy::BFS into the refinement CLI call.
crates/vpg/src/verify.rs	Adds extra verification assertions and introduces a new test-only “solitaire” wrapper + tests.
crates/vpg/src/translate.rs	Fixes/extends regular-formula translation to support diamond-iteration semantics (mu/`
crates/vpg/src/parity_games/random_game.rs	Minor cleanup/formatting changes to random parity game generation and tests.
crates/symbolic/src/random_bdd.rs	Refactors BDD cube construction and switches error type to OutOfMemory.
crates/refinement/src/refinement.rs	Centralizes preprocessing/merging and dispatches to failures vs. impossible-futures refinement logic.
crates/refinement/src/lib.rs	Exposes new impossible_futures module publicly.
crates/refinement/src/impossible_futures.rs	New impossible futures refinement implementation (with weak-trace helper and divergence check).
crates/refinement/src/failures_refinement.rs	Refactors into is_refinement_generic, adds stable-failures refusal checking, exposes tau_closure.
crates/refinement/src/counterexample_formula.rs	Adds counterexample variants + formula generation for stable failures and impossible futures.
crates/refinement/src/antichain.rs	Adds basic antichain utility methods (len/clear/metrics).
crates/reduction/src/simple_block_partition.rs	Removes test-only guard from block_number.
crates/reduction/src/quotient.rs	Improves bottom-state selection for branching quotienting and adds diverges + tests.
crates/lts/src/random_lts.rs	Adds mutate_lts helper used by refinement tests.
crates/lts/src/lts_builder_fast.rs	Maps configured hidden labels to tau (label index 0) when adding transitions.
crates/lts/src/lts_builder.rs	Same hidden-label-to-tau mapping for the memory-optimized builder.
crates/collections/src/vecset.rs	Adds difference, extend, FromIterator, and tests; uses sort_unstable.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

You can also share your feedback on Copilot code review. Take the survey.

[Copilot]

Pull request overview

This PR extends the refinement checking pipeline to support additional semantic relations (stable failures and impossible futures), including updated preprocessing/reduction plumbing and counterexample generation to produce distinguishing modal formulas.

Changes:

• Add StableFailures and ImpossibleFutures refinement variants, plus a configurable exploration strategy (BFS/DFS), and route refinement checks through a shared antichain-based core.
• Implement impossible futures refinement checking and extend counterexample generation to produce stable-failures and impossible-futures formulas.
• Refactor reduction/preprocessing utilities (tau-loop elimination + reorder, weak/branching bisim entrypoints) and add assorted supporting utilities/tests/docs across the workspace.

Reviewed changes

Copilot reviewed 46 out of 48 changed files in this pull request and generated 7 comments.

Show a summary per file

File	Description
tools/mcrl2/Cargo.lock	Dependency lock updates (toml/winnow versions).
tools/lts/src/main.rs	Update CLI refinement invocation to pass an explicit exploration strategy.
tools/gui/Cargo.toml	Update repository URL metadata.
crates/vpg/src/zielonka.rs	Enable solution verification in Zielonka solver randomized test.
crates/vpg/src/verify.rs	Refactor/strengthen solution verification and add solitaire-game tests.
crates/vpg/src/translate.rs	Fix regular-formula translation to use least/greatest fixpoints correctly for diamond/box.
crates/vpg/src/parity_games/random_game.rs	Minor cleanups/formatting in random parity game generation and tests.
crates/utilities/README.md	README grammar fix.
crates/unsafety/README.md	README grammar/spelling fixes.
crates/symbolic/src/random_bdd.rs	Factor out cube construction and return OutOfMemory directly.
crates/sharedmutex/README.md	README license formatting tweak.
crates/sabre/src/utilities/substitution.rs	Replace misleading TODO with accurate buffer reuse comment.
crates/sabre/src/utilities/data_substitution.rs	Same comment cleanup as substitution utility.
crates/sabre/README.md	README license formatting tweak.
crates/refinement/src/refinement.rs	New refinement variants + preprocessing logic, counterexample routing, and randomized refinement tests.
crates/refinement/src/lib.rs	Export new impossible futures module.
crates/refinement/src/impossible_futures.rs	New impossible futures refinement implementation.
crates/refinement/src/failures_refinement.rs	Refactor to a generic antichain-based refinement core + stable failures refusal checking + example-based test.
crates/refinement/src/counterexample_formula.rs	Add formula generation for stable failures / impossible futures; factor weak-trace formula builder.
crates/refinement/src/antichain.rs	Add basic antichain utility methods and metrics accessor.
crates/reduction/src/weak_bisimulation.rs	Thread “state mapping” through tau-loop elimination and weak bisimulation APIs.
crates/reduction/src/sort_topological.rs	Narrow test imports for clarity.
crates/reduction/src/simple_block_partition.rs	Formatting/cleanup and allow block_number outside tests.
crates/reduction/src/signatures.rs	Change tau-loop elimination to return mapped state alongside reordered LTS.
crates/reduction/src/signature_refinement.rs	Thread “state mapping” through branching/weak signature refinement APIs and tests.
crates/reduction/src/scc_decomposition.rs	Narrow test imports for clarity.
crates/reduction/src/reduce.rs	Adapt reduction pipeline to updated weak/branching APIs with state mapping.
crates/reduction/src/quotient.rs	Strengthen branching quotient representative selection and add divergence detection + tests.
crates/reduction/src/compare.rs	Adapt compare pipeline to updated reduction APIs; add permutation-equivalence test.
crates/reduction/src/block_partition.rs	Remove debug print and minor formatting.
crates/number/README.md	Fix Markdown heading levels.
crates/lts/src/reachability.rs	New reachability analysis utility (DFS) + reachable-count helper.
crates/lts/src/random_lts.rs	Random LTS generation tweaks and new mutate_lts helper used by refinement tests.
crates/lts/src/product_lts.rs	Narrow test imports for clarity.
crates/lts/src/lts_builder_fast.rs	Support mapping configured hidden labels to tau in builder label interning.
crates/lts/src/lts_builder.rs	Same hidden-label-to-tau mapping for memory-optimized builder.
crates/lts/src/lts.rs	Formatting-only change.
crates/lts/src/lib.rs	Export new reachability module.
crates/lts/src/labelled_transition_system.rs	Introduce from_raw_parts, strengthen invariants, and fix new_from_permutation by rebuilding transition arrays.
crates/lts/src/io_lts.rs	Narrow test imports for clarity.
crates/lts/src/io_aut.rs	Narrow test imports/formatting.
crates/lts/src/incoming_transitions.rs	Narrow test imports/formatting.
crates/collections/src/vecset.rs	Add difference, extend, FromIterator, and improve subset check implementation.
crates/collections/src/scc_decomposition.rs	Add debug assertion documenting dense-graph assumption.
crates/collections/src/indexed_partition.rs	Document dense-element assumption.
crates/aterm/README.md	README license formatting tweak.
README.md	Remove mention of 3rd-party directory from license section.
Cargo.toml	Update workspace repository URL metadata.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.