Added --verify-solution for the zielonka solver #70

mlaveaux · 2026-02-10T15:05:49Z

Added algorithms to verify the solution of zielonka.

* Made a feature transition system a generalisation of a labelled transition system by adding a FeaturedLabel. This allows us to merge the translations to a VPG/PG into one as well.

Copilot

Pull request overview

This PR introduces infrastructure to verify Zielonka solver outputs and refactors core parity-game/LTS structures to carry edge labels more uniformly across the codebase.

Changes:

Add a verify_solution implementation and a randomized Zielonka solver test that uses it.
Refactor PG to expose outgoing edges via a shared Edge<label,to> abstraction (enabling labelled edges for VPGs).
Rework feature transition system labels to embed feature expressions into the label type, plus assorted doc/CLI help text cleanups.

Reviewed changes

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

Show a summary per file

File	Description
tools/vpg/src/main.rs	Doc/help text adjustment (but no `--verify-solution` flag wiring present).
tools/sym/src/main.rs	Small formatting simplification around timing/reading.
tools/rewrite/src/main.rs	CLI doc/help text cleanup; adds help text for output argument.
tools/lts/src/main.rs	CLI help text cleanup; minor wording change (introduces a grammar issue).
tools/gui/ltsgraph/src/main.rs	Improves CLI `about` text and argument docs for the GUI tool.
crates/vpg/src/zielonka.rs	Updates edge iteration to new `Edge` API; adds randomized test calling `verify_solution`.
crates/vpg/src/verify.rs	New parity-game solution verification logic and a `SubGame` adapter.
crates/vpg/src/variability_zielonka.rs	Migrates from config-edge iterator to the unified `outgoing_edges` + `label()`.
crates/vpg/src/variability_translate.rs	Refactors to use shared `Translation` and featured labels.
crates/vpg/src/translate.rs	Generalizes `Translation` to support labelled edges via a labelling callback.
crates/vpg/src/reachability.rs	Updates reachability traversal for new `Edge` API.
crates/vpg/src/project.rs	Updates VPG projection to use `Edge::label()` for configuration BDDs.
crates/vpg/src/parity_games/variability_predecessors.rs	Updates predecessor construction for new `Edge` API.
crates/vpg/src/parity_games/variability_parity_game.rs	Removes VPG-specific edge type; implements `PG::outgoing_edges` returning labelled `Edge`.
crates/vpg/src/parity_games/variability_make_total.rs	Updates totalization logic to use `Edge::label()` for configs.
crates/vpg/src/parity_games/predecessors.rs	Updates predecessor construction for new `Edge` API.
crates/vpg/src/parity_games/parity_game.rs	Extends `PG` with associated label type and adds shared `Edge` struct; updates debug output.
crates/vpg/src/parity_games/io_vpg.rs	Updates VPG writer to use `Edge::label()`.
crates/vpg/src/parity_games/io_pg.rs	Generalizes `.pg` writer to accept any `PG`; adapts for new `Edge` API.
crates/vpg/src/parity_games/display_dot.rs	Updates dot output to handle `Edge` iterator.
crates/vpg/src/lib.rs	Exposes new `verify` module publicly.
crates/vpg/src/feature_transition_system.rs	Embeds feature expressions into a `FeaturedLabel` type; changes `FeatureTransitionSystem` to be generic over label.
crates/symbolic/src/io_symbolic_lts.rs	Wraps reader in `BufReader` before binary ATerm reading.
crates/reduction/src/simple_block_partition.rs	Adds a release-mode panic guard to `block_number`.
crates/reduction/src/signature_refinement.rs	Minor lifetime/type annotation tweak around `transmute`.
crates/lts/src/lts.rs	Adds documentation for default `TransitionLabel::is_tau_label`.
crates/io/src/bitstream.rs	Condenses bitstream precondition docs into single-line doc comments.
crates/data/src/sort_terms.rs	Introduces `BasicSort` term and adjusts unknown sort construction.
crates/data/src/data_terms.rs	Expands `DataSymbols` to cover more mCRL2-like symbols and adds helpers (incl. basic sort checks).
crates/collections/src/lib.rs	Adds and re-exports new `block_partition` module.
crates/collections/src/indexed_partition.rs	Improves documentation for `set_block` semantics.
crates/collections/src/compressed_vec.rs	Clarifies drop semantics in documentation.
crates/collections/src/block_partition.rs	Adds a new `BlockPartition` abstraction with `SimpleBlock` implementation and tests.

Copilot · 2026-02-10T15:34:29Z

crates/vpg/src/verify.rs

+        let mut winning_set = bitvec![usize, Lsb0; 0; pg.num_of_vertices()];
+
+        for priority in 0..pg.highest_priority().value() {
+            if Player::from_priority(&(Priority::new(priority))) != player {
+                // Skip priorities that do not belong to the current player
+                continue;
+            }
+
+            // Restrict the game according to the strategy and the current priority.
+            trace!("Restricting game for player {} with priority {}", player, priority);
+            let restricted_game = SubGame::new(pg, player, &strategy[player.to_index()], Priority::new(priority));
+
+            let _predecessors = Predecessors::new(&restricted_game);
+
+            let scc_partition = scc_decomposition(&AsGraph(&restricted_game), |_, _, _| true);
+
+            // For every strongly connected component, check if it is winning for the player
+            for block in 0..scc_partition.num_of_blocks() {
+                for element in 0..scc_partition.len() {
+                    if scc_partition.partition()[element] == block {
+                        let vertex = VertexIndex::new(element);
+
+                        if restricted_game.priority(vertex) == player.to_index() {
+                            // This SCC contains a vertex with the current priority, so it is winning for the player
+                            winning_set.set(vertex.value(), true);
+                        }
+                    }
+                }
+            }
+        }
+
+        if winning_set != solution[player.to_index()] {
+            panic!("The proposed winning set for player {} is incorrect", player);


verify_solution appears to compute a player's winning set by iterating priorities, building a SubGame, and then marking vertices based on SCC membership and a rewritten priority check. This does not correspond to a correct parity-game strategy verification (e.g., checking that the induced game under the strategy satisfies the parity condition on all reachable cycles / SCC minima), and it also doesn’t restrict verification to the claimed winning region. Consider reworking verification to the standard approach: restrict to the claimed winning set, restrict player-owned vertices by the strategy, compute SCCs in the resulting graph, and check the minimum priority in each reachable SCC has the correct parity for the player (and that opponent vertices stay inside the region).

Suggested change

let mut winning_set = bitvec![usize, Lsb0; 0; pg.num_of_vertices()];

for priority in 0..pg.highest_priority().value() {

if Player::from_priority(&(Priority::new(priority))) != player {

// Skip priorities that do not belong to the current player

continue;

}

// Restrict the game according to the strategy and the current priority.

trace!("Restricting game for player {} with priority {}", player, priority);

let restricted_game = SubGame::new(pg, player, &strategy[player.to_index()], Priority::new(priority));

let _predecessors = Predecessors::new(&restricted_game);

let scc_partition = scc_decomposition(&AsGraph(&restricted_game), |_, _, _| true);

// For every strongly connected component, check if it is winning for the player

for block in 0..scc_partition.num_of_blocks() {

for element in 0..scc_partition.len() {

if scc_partition.partition()[element] == block {

let vertex = VertexIndex::new(element);

if restricted_game.priority(vertex) == player.to_index() {

// This SCC contains a vertex with the current priority, so it is winning for the player

winning_set.set(vertex.value(), true);

}

}

}

}

}

if winning_set != solution[player.to_index()] {

panic!("The proposed winning set for player {} is incorrect", player);

// The claimed winning region for this player.

let region: &Set = &solution[player.to_index()];

// Determine the opponent.

let opponent = match player {

Player::Even => Player::Odd,

Player::Odd => Player::Even,

};

let graph = AsGraph(pg);

// 1) Check that the opponent cannot escape the claimed winning region:

// for every opponent-owned vertex in the region, all outgoing edges

// must stay within the region.

for v_idx in 0..pg.num_of_vertices() {

if !region[v_idx] {

continue;

}

let v = VertexIndex::new(v_idx);

if pg.owner(v) != opponent {

continue;

}

for (_label, w) in graph.outgoing_edges(v) {

let w_idx = w.index();

if !region

.get(w_idx)

.expect("Vertex must be in the region bit-vector")

{

panic!(

"Opponent can escape the claimed winning region of player {} from vertex {}",

player,

v.value()

);

}

}

}

// 2) Compute SCCs in the subgraph induced by the claimed winning region.

// Edges are only kept if both endpoints are inside the region.

let scc_partition = scc_decomposition(&graph, |_, src, dst| {

let src_idx = src.index();

let dst_idx = dst.index();

// Only keep edges completely inside the region.

*region

.get(src_idx)

.expect("Vertex must be in the region bit-vector")

&& *region

.get(dst_idx)

.expect("Vertex must be in the region bit-vector")

});

// 3) For each SCC that intersects the region, compute the minimum

// priority and check that its parity matches the player.

let num_blocks = scc_partition.num_of_blocks();

let mut block_min_priority: Vec<Option<Priority>> = vec![None; num_blocks];

for v_idx in 0..scc_partition.len() {

if !region[v_idx] {

continue;

}

let block = scc_partition.partition()[v_idx];

let v = VertexIndex::new(v_idx);

let prio = pg.priority(v);

match &mut block_min_priority[block] {

None => {

block_min_priority[block] = Some(prio);

}

Some(current_min) => {

if prio < *current_min {

*current_min = prio;

}

}

}

}

for (block, min_prio_opt) in block_min_priority.into_iter().enumerate() {

if let Some(min_prio) = min_prio_opt {

let winning_player = Player::from_priority(&min_prio);

if winning_player != player {

panic!(

"SCC {} inside the claimed winning region of player {} \

has minimum priority {} with wrong parity",

block,

player,

min_prio.value()

);

}

}

Copilot · 2026-02-10T15:34:30Z

crates/vpg/src/verify.rs

+
+        let mut winning_set = bitvec![usize, Lsb0; 0; pg.num_of_vertices()];
+
+        for priority in 0..pg.highest_priority().value() {


The loop for priority in 0..pg.highest_priority().value() skips the highest priority value because the upper bound is exclusive. If you intend to consider all priorities up to the maximum, this should iterate inclusively.

Suggested change

for priority in 0..pg.highest_priority().value() {

for priority in 0..=pg.highest_priority().value() {

Copilot · 2026-02-10T15:34:30Z

crates/vpg/src/verify.rs

+                .get(*edge.to())
+                .expect("Vertex must be in the restricted set")
+                == true
+                && (self.game.owner(edge.to()) != self.player || self.strategy.get(vertex_index) == Some(&edge.to()))


SubGame::outgoing_edges checks self.game.owner(edge.to()) != self.player when deciding whether to enforce the strategy. Strategy choice should depend on the owner of the source vertex (vertex_index), not the owner of the destination, otherwise many edges will be incorrectly filtered/kept.

Suggested change

&& (self.game.owner(edge.to()) != self.player || self.strategy.get(vertex_index) == Some(&edge.to()))

&& (self.game.owner(vertex_index) != self.player

|| self.strategy.get(vertex_index) == Some(&edge.to()))

Copilot · 2026-02-10T15:34:30Z

crates/vpg/src/verify.rs

+    /// The game that is being restricted.
+    game: &'a G,
+
+    /// The minimum priority in the sub-game.


The doc comment says max_priority is the "minimum priority" in the sub-game, but the implementation restricts to priority(vertex) <= max_priority and uses it as an upper bound. Update the documentation (or rename the field) to match the behavior.

Suggested change

/// The minimum priority in the sub-game.

/// The maximum priority included in the sub-game.

Copilot · 2026-02-10T15:34:31Z

crates/vpg/src/feature_transition_system.rs

+impl<L: TransitionLabel> TransitionLabel for FeaturedLabel<L> {
+    delegate::delegate! {
+        to self.label {
+            fn matches_label(&self, label: &str) -> bool;
+        }
+    }
+
+    fn from_index(_i: usize) -> Self {
+        panic!("Cannot create FeaturedLabel from index");
+    }
+
+    fn tau_label() -> Self {
+        panic!("Cannot create FeaturedLabel from index");
+    }
+}


FeaturedLabel implements TransitionLabel, but tau_label() and from_index() panic, and is_tau_label() will use the default implementation which calls Self::tau_label()—so any generic code calling is_tau_label() on a FeaturedLabel will panic (e.g., LTS builders and product construction). Consider overriding is_tau_label() to delegate to the inner label, and avoid panicking implementations if FeaturedLabel can flow into generic LTS code.

Copilot · 2026-02-10T15:34:32Z

crates/vpg/src/verify.rs

+        if self.game.priority(vertex) == self.max_priority {
+            // Return the priority for the current player.
+            Priority::new(self.player.to_index())
+        } else {
+            // Return the priority for the opponent.
+            Priority::new(self.player.opponent().to_index())
+        }


SubGame::priority collapses priorities to 0/1 based on whether the original priority equals max_priority. This destroys the parity structure (and makes SCC parity checks meaningless). Verification should use the original priorities (or compute SCC minima on the original priorities) rather than rewriting them like this.

Suggested change

if self.game.priority(vertex) == self.max_priority {

// Return the priority for the current player.

Priority::new(self.player.to_index())

} else {

// Return the priority for the opponent.

Priority::new(self.player.opponent().to_index())

}

// Preserve the original priority structure of the underlying game.

self.game.priority(vertex)

Copilot · 2026-02-10T15:34:32Z

crates/vpg/src/feature_transition_system.rs

+    // Find the associated feature for each label and relabel the LTS accordingly.
+    let aut = aut.relabel(|label| {
+        let associated_feature = feature_labels[original_labels
+            .iter()
+            .position(|orig| *orig == label)
+            .expect("label must have an associated feature")]
+        .clone();


read_fts relabels by doing original_labels.iter().position(|orig| *orig == label) for each label, which makes relabelling O(n^2) in the number of labels. Building a HashMap<label, feature_expr> (or iterating by index) would avoid repeated linear scans and improve scalability for large label sets.

Suggested change

// Find the associated feature for each label and relabel the LTS accordingly.

let aut = aut.relabel(|label| {

let associated_feature = feature_labels[original_labels

.iter()

.position(|orig| *orig == label)

.expect("label must have an associated feature")]

.clone();

// Build a mapping from each original label to its associated feature for efficient lookup.

let feature_map: HashMap<TransitionLabel, BDDFunction> = original_labels

.iter()

.cloned()

.zip(feature_labels.iter().cloned())

.collect();

// Find the associated feature for each label and relabel the LTS accordingly.

let aut = aut.relabel(|label| {

let associated_feature = feature_map

.get(&label)

.expect("label must have an associated feature")

.clone();

Copilot · 2026-02-10T15:34:32Z

crates/collections/src/block_partition.rs

+    /// Create an initial partition where all the states are in a single block
+    /// 0. And all the elements in the block are marked.
+    pub fn new(num_of_elements: usize) -> Self {
+        debug_assert!(num_of_elements > 0, "Cannot partition the empty set");


BlockPartition::new uses debug_assert!(num_of_elements > 0, ...), which is skipped in release builds. If empty partitions are invalid, this should be a regular assert! (or handled explicitly), otherwise release builds can create an invalid initial block.

Suggested change

debug_assert!(num_of_elements > 0, "Cannot partition the empty set");

assert!(num_of_elements > 0, "Cannot partition the empty set");

Copilot · 2026-02-10T15:34:33Z

tools/lts/src/main.rs

 }

-/// Checks whether the given implementation LTS refines the given specification LTS modulo various preorders.
+/// Checks whether the given implementation LTS refines the given specification LTS modulo various refinement relation.


Grammar: "various refinement relation" should be plural ("relations") to match "various" and the enum-based selection that follows.

Suggested change

/// Checks whether the given implementation LTS refines the given specification LTS modulo various refinement relation.

/// Checks whether the given implementation LTS refines the given specification LTS modulo various refinement relations.

Copilot · 2026-02-10T15:34:33Z

tools/vpg/src/main.rs

+/// A command line tool for variability parity games
 #[derive(clap::Parser, Debug)]
 #[command(
    arg_required_else_help = true


PR title/description mention adding a --verify-solution flag for the Zielonka solver, but there’s no corresponding CLI option or usage in this diff (and no verify-solution occurrences in the codebase). Either the flag wiring is missing, or the PR description/title should be adjusted to reflect that this adds a library verifier + tests only.

Copilot AI review requested due to automatic review settings February 10, 2026 15:05

Copilot started reviewing on behalf of mlaveaux February 10, 2026 15:17 View session

mlaveaux added 9 commits February 10, 2026 16:26

Added an initial attempt at verifying the zielonka solver strategy.

1ed4f65

Changed various comments

3f59c0a

This operation should not be used in release

87d7e70

Added a generic block partition

5b43e2d

Added various default symbols.

ccdd69a

Added a generic label to a PG to share code between VPGs and PGs.

288811d

* Made a feature transition system a generalisation of a labelled transition system by adding a FeaturedLabel. This allows us to merge the translations to a VPG/PG into one as well.

Pushed the changes to the PG trait throughout the crate

d20ed7d

Fixed the vpg translation.

9491456

Fixed clippy warnings

66b40bc

Copilot AI reviewed Feb 10, 2026

View reviewed changes

Fixed project, and change the place where the commands are documented

867953f

mlaveaux force-pushed the feature/verify branch from 354f89d to 867953f Compare February 10, 2026 15:52

mlaveaux added the enhancement New feature or request label Feb 10, 2026

mlaveaux self-assigned this Feb 10, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Added --verify-solution for the zielonka solver #70

Added --verify-solution for the zielonka solver #70

Uh oh!

mlaveaux commented Feb 10, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Feb 10, 2026

Uh oh!

Copilot AI Feb 10, 2026

Uh oh!

Copilot AI Feb 10, 2026

Uh oh!

Copilot AI Feb 10, 2026

Uh oh!

Copilot AI Feb 10, 2026

Uh oh!

Copilot AI Feb 10, 2026

Uh oh!

Copilot AI Feb 10, 2026

Uh oh!

Copilot AI Feb 10, 2026

Uh oh!

Copilot AI Feb 10, 2026

Uh oh!

Copilot AI Feb 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant


		let mut winning_set = bitvec![usize, Lsb0; 0; pg.num_of_vertices()];

		for priority in 0..pg.highest_priority().value() {

	for priority in 0..pg.highest_priority().value() {
	for priority in 0..=pg.highest_priority().value() {

	&& (self.game.owner(edge.to()) != self.player \|\| self.strategy.get(vertex_index) == Some(&edge.to()))
	&& (self.game.owner(vertex_index) != self.player
	\|\| self.strategy.get(vertex_index) == Some(&edge.to()))

	/// The minimum priority in the sub-game.
	/// The maximum priority included in the sub-game.

	debug_assert!(num_of_elements > 0, "Cannot partition the empty set");
	assert!(num_of_elements > 0, "Cannot partition the empty set");

	/// Checks whether the given implementation LTS refines the given specification LTS modulo various refinement relation.
	/// Checks whether the given implementation LTS refines the given specification LTS modulo various refinement relations.

Added --verify-solution for the zielonka solver #70

Are you sure you want to change the base?

Added --verify-solution for the zielonka solver #70

Uh oh!

Conversation

mlaveaux commented Feb 10, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant