Implement Jan Friso's strong bisimulation refinement

[mlaveaux]

Done:

• Introduce a quotienting procedure (both naive and optimised) to validate the results of symbolic refinement.
• Introduce a conversion from a symbolic BDD LTS to a concrete LTS. This was only implemented for LDDs.
• Finish the procedure described by Jan Friso Groote.
• We should also fix the original strong bisimulation refinement, see The symbolic bisimulation implementation in merc-sym is not correct #88

[Copilot]

Pull request overview

This PR extends the toolchain and core crates to support additional refinement and composition workflows, including wiring in a new (work-in-progress) symbolic strong bisimulation refinement, adding an LTS combine command (hide/allow/comm over parallel composition), and refactoring parity-game solving utilities (predecessor abstraction + strategy abstraction) plus related data-structure updates (multiset actions, subset-aware partitions).

Changes:

• Add a new symbolic strong bisimulation refinement entry point and expose it in merc-sym reduce via an equivalence selector.
• Introduce lts combine and supporting multi-action parsing/communication/allow/hide logic, plus streaming AUT output support.
• Refactor parity game utilities (Zielonka strategies via Strat, predecessor access via Pred), and introduce VecBag + subset-aware IndexedPartition for multiset/actions and subgraph partitions.

Reviewed changes

Copilot reviewed 33 out of 37 changed files in this pull request and generated 11 comments.

Show a summary per file

File	Description
tools/sym/src/main.rs	Adds equivalence selector for reduction and calls new refinement routine.
tools/lts/src/main.rs	Adds combine subcommand; updates conversions to handle fallible relabelling.
tools/lts/src/combine.rs	Implements parallel composition + hide/allow/comm pipeline and iterators.
tools/lts/Cargo.toml	Adds dependencies needed for combine implementation.
crates/vpg/src/zielonka.rs	Refactors Zielonka solver to generic strategy representation (Strat).
crates/vpg/src/verify.rs	Minor import ordering + improved panic formatting.
crates/vpg/src/variability_translate.rs	Formatting/import adjustments in translation + tests.
crates/vpg/src/translate.rs	Formatting/import adjustments in translation + tests.
crates/vpg/src/strategy.rs	Introduces Strat trait with Strategy and () implementations.
crates/vpg/src/project_vpg.rs	Formatting-only change.
crates/vpg/src/project_fts.rs	Import ordering + formatting in iterator construction.
crates/vpg/src/parity_games/variability_parity_game.rs	Formatting-only whitespace change.
crates/vpg/src/parity_games/variability_make_total.rs	Formatting-only change.
crates/vpg/src/parity_games/solitaire_game.rs	Introduces Subgame + uses Pred to reuse predecessors in solving.
crates/vpg/src/parity_games/random_game.rs	Formatting-only whitespace change.
crates/vpg/src/parity_games/predecessors.rs	Adds Pred trait and implements it for Predecessors (+ tests).
crates/vpg/src/parity_games/io_vpg.rs	Test import fixes.
crates/vpg/src/parity_games/io_pg.rs	Test import fixes.
crates/vpg/src/parity_games/builder.rs	Minor formatting for closure formatting.
crates/vpg/src/modal_equation_system.rs	Import ordering and test import adjustment.
crates/vpg/src/feature_transition_system.rs	Makes relabelling fallible and propagates error.
crates/syntax/src/syntax_tree.rs	Renames Comm to CommExpr; adds helpers on MultiActionLabel.
crates/syntax/src/syntax_tree_display.rs	Updates display impl/imports for CommExpr.
crates/syntax/src/parse.rs	Adds parsing helpers for hide/allow/comm CLI arguments.
crates/syntax/src/consume.rs	Exposes parsers for action sets / comm sets; switches to CommExpr.
crates/symbolic/src/refine.rs	Adds new symbolic strong bisimulation refinement module (currently incomplete).
crates/symbolic/src/lib.rs	Exports new refine module.
crates/symbolic/src/convert_ldd.rs	Minor doc/import cleanup for symbolic conversion.
crates/reduction/src/partition.rs	Adjusts combine_partition initialization (now clones left).
crates/lts/src/multi_action.rs	Switches multi-actions to multiset (VecBag), adds utility methods.
crates/lts/src/labelled_transition_system.rs	Makes relabel fallible (Result) to support parse failures.
crates/lts/src/io_aut_stream.rs	Adds documentation for streaming AUT writer.
crates/collections/src/vecbag.rs	Introduces VecBag multiset container.
crates/collections/src/scc_decomposition.rs	Uses subset-aware IndexedPartition for SCC computation.
crates/collections/src/lib.rs	Exports vecbag module.
crates/collections/src/indexed_partition.rs	Adds subset-aware partitions with NOT_IN_PARTITION.
Cargo.lock	Updates dependency graph for new workspace deps.

Comments suppressed due to low confidence (1)

crates/reduction/src/partition.rs:48

• IndexedPartition can now contain NOT_IN_PARTITION entries, but combine_partition still iterates over every element and feeds block.value() into StateIndex::new(...). For NOT_IN_PARTITION this will produce an invalid StateIndex and can panic or corrupt the combined partition. Consider skipping elements where block.value() == NOT_IN_PARTITION (leaving them as NOT_IN_PARTITION in the result) or otherwise defining how excluded elements should be handled.

pub fn combine_partition<P: Partition>(left: IndexedPartition, right: &P) -> IndexedPartition {
    let mut combined_partition = left.clone();

    for (element_index, block) in left.partition().iter().enumerate() {
        let new_block = right.block_number(StateIndex::new(block.value()));

        combined_partition.set_block(element_index, new_block);
    }

---

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

[Copilot]

parse_allow_action_names parses using Rule::ActIdSet but then feeds the parse tree to Mcrl2Parser::MultActIdSet. The grammar has a dedicated MultActIdSet rule, so this mismatch will reject valid allow-sets or misparse input. Parse with Rule::MultActIdSet (and keep the error message aligned).

[Copilot]

U_clone = U.clone() is now unconditional. In the compute_strategy = false path (S = ()), this clone is still executed even though ()'s extend_arbitrary ignores the arguments, which can add avoidable allocations in deep recursion. Consider making the clone conditional again (based on compute_strategy) or otherwise structuring the code so the no-strategy specialization doesn’t require cloning U.