Implemented the naive weak bisimulation algorithm proposed by Eduardo #42

mlaveaux · 2025-12-06T15:25:02Z

This is a weak bisimulation algorithm based on partition refinement due to Eduardo, without explicitly computing the signatures explicitly.

Copilot

Pull request overview

This PR implements a naive weak bisimulation algorithm based on partition refinement, proposed by Eduardo Costa Martins. The implementation avoids explicitly computing signatures for efficiency.

Key changes:

Adds a new weak_bisimulation module implementing the partition refinement algorithm
Introduces SimpleBlockPartition data structure for managing block partitions during reduction
Integrates the new algorithm into the existing reduction and comparison infrastructure

Reviewed changes

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

Show a summary per file

File	Description
crates/reduction/src/weak_bisimulation.rs	New file implementing the core weak bisimulation algorithm with partition refinement
crates/reduction/src/simple_block_partition.rs	New data structure for managing block partitions with split operations
crates/reduction/src/reduce.rs	Implements the `WeakBisim` equivalence case using the new algorithm
crates/reduction/src/lib.rs	Exports the new modules
crates/reduction/src/compare.rs	Integrates weak bisimulation for LTS comparison

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

Copilot · 2025-12-06T15:44:28Z

crates/reduction/src/simple_block_partition.rs

+    fn block_number(&self, state_index: StateIndex) -> BlockIndex {
+        for (block_index, block) in self.blocks.iter().enumerate() {
+            for element in block.iter(&self.elements) {
+                if element == state_index {
+                    return BlockIndex::new(block_index);
+                }
+            }
+        }
+
+        panic!("State index {:?} not found in partition {:?}", state_index, self);
+    }


This implementation has O(n*m) complexity where n is the number of blocks and m is the average block size. This could be optimized by maintaining a reverse mapping from state indices to block indices, making lookups O(1) instead of requiring iteration through all blocks and their elements.

crates/reduction/src/simple_block_partition.rs

crates/reduction/src/weak_bisimulation.rs

crates/reduction/src/simple_block_partition.rs

crates/reduction/src/compare.rs

crates/reduction/src/weak_bisimulation.rs

crates/reduction/src/simple_block_partition.rs

Copilot

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.

Copilot

Copilot reviewed 5 out of 5 changed files in this pull request and generated 9 comments.

Copilot · 2025-12-06T20:35:26Z

crates/reduction/src/weak_bisimulation.rs

+                );
+
+                for block_prime in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {
+                    // This cannot be a reference since the blocks are updated.


The comment "This cannot be a reference since the blocks are updated" is misleading. The block_prime variable is a BlockIndex (which is a Copy type), not a reference to a block. The comment seems to be explaining why we can't hold a reference to the actual block data structure (from blocks.block()), but the code doesn't attempt to do that. Consider clarifying or removing this comment.

Suggested change

// This cannot be a reference since the blocks are updated.

Copilot · 2025-12-06T20:35:26Z

crates/reduction/src/simple_block_partition.rs

+/// A block stores a subset of the elements in a partition. It uses start,
+/// middle and end to indicate a range start..end of elements in the partition.
+/// The middle is used such that marked_split..end are the marked elements. This
+/// is useful to be able to split off new blocks cheaply.
+///
+/// Invariant: start <= middle <= end && start < end.


The documentation mentions "start, middle and end" and "marked_split..end" fields, but the SimpleBlock struct only has begin, end, and stable fields. This appears to be outdated documentation, possibly copied from a different block implementation that uses a middle marker for efficient splitting. Update the documentation to accurately describe this implementation's approach using begin and end ranges.

Suggested change

/// A block stores a subset of the elements in a partition. It uses start,

/// middle and end to indicate a range start..end of elements in the partition.

/// The middle is used such that marked_split..end are the marked elements. This

/// is useful to be able to split off new blocks cheaply.

///

/// Invariant: start <= middle <= end && start < end.

/// A block stores a subset of the elements in a partition. It uses `begin` and

/// `end` to indicate a contiguous range of elements in the partition, represented

/// by the indices `begin..end` into the partition's element list.

///

/// Invariant: begin <= end && begin < end.

Copilot · 2025-12-06T20:35:26Z

crates/reduction/src/weak_bisimulation.rs

+        for transition in lts.outgoing_transitions(s) {
+            if transition.label == label {
+                // s.act_mark := true iff a != tau && tau_mark[t]
+                if !lts.is_hidden_label(transition.label) && tau_mark[*transition.to] {
+                    act_mark.set(
+                        *s,
+                        true,
+                    );


The condition !lts.is_hidden_label(transition.label) is redundant here since transition.label == label (from line 114). This is equivalent to checking !lts.is_hidden_label(label), which could be moved outside the loop for better clarity and efficiency. Consider restructuring this logic to check the label type once before the loop.

Suggested change

for transition in lts.outgoing_transitions(s) {

if transition.label == label {

// s.act_mark := true iff a != tau && tau_mark[t]

if !lts.is_hidden_label(transition.label) && tau_mark[*transition.to] {

act_mark.set(

*s,

true,

);

if !lts.is_hidden_label(label) {

for transition in lts.outgoing_transitions(s) {

if transition.label == label {

// s.act_mark := true iff a != tau && tau_mark[t]

if tau_mark[*transition.to] {

act_mark.set(

*s,

true,

);

}

Copilot · 2025-12-06T20:35:27Z

crates/reduction/src/weak_bisimulation.rs

+/// Sets s.act_mark to true iff exists t: S. s =!a=> t
+/// If a = tau, then also updates s.tau_mark


The comment uses mathematical notation "s =!a=> t" but doesn't explain what it means. For readers unfamiliar with weak bisimulation theory, consider expanding this to explain that "s =!a=> t" represents a weak transition (zero or more tau transitions, followed by an 'a' transition, followed by zero or more tau transitions) from state s to state t.

Suggested change

/// Sets s.act_mark to true iff exists t: S. s =!a=> t

/// If a = tau, then also updates s.tau_mark

/// Sets s.act_mark to true iff there exists t ∈ S such that s =!a=> t.

/// Here, "s =!a=> t" denotes a weak transition: there is a sequence of zero or more tau (silent) transitions from s,

/// followed by an 'a' transition, followed by zero or more tau transitions, leading to t.

/// If a = tau, then also updates s.tau_mark.

Copilot · 2025-12-06T20:35:27Z

crates/reduction/src/simple_block_partition.rs

+/// A block stores a subset of the elements in a partition. It uses start,
+/// middle and end to indicate a range start..end of elements in the partition.
+/// The middle is used such that marked_split..end are the marked elements. This
+/// is useful to be able to split off new blocks cheaply.
+///
+/// Invariant: start <= middle <= end && start < end.


The invariant documentation references a "middle" field that doesn't exist in the struct. The actual invariant should be begin < end (as enforced by the debug_assert on line 149). Update this comment to reflect the actual struct fields.

Suggested change

/// A block stores a subset of the elements in a partition. It uses start,

/// middle and end to indicate a range start..end of elements in the partition.

/// The middle is used such that marked_split..end are the marked elements. This

/// is useful to be able to split off new blocks cheaply.

///

/// Invariant: start <= middle <= end && start < end.

/// A block stores a subset of the elements in a partition. It uses `begin` and

/// `end` to indicate a range `begin..end` of elements in the partition.

///

/// Invariant: begin < end.

Copilot · 2025-12-06T20:35:27Z

crates/reduction/src/weak_bisimulation.rs

+    for t in lts.iter_states() {
+        // t.tau_mark := t.act_mark if a == tau
+        if lts.is_hidden_label(label) {
+            tau_mark.set(*t, act_mark[*t]);


The tau_mark bitvector is never cleared and persists across different blocks and outer loop iterations. On line 129, tau_mark is set when processing the tau label for one block, but this value persists when processing other blocks and in subsequent outer loop iterations. This could lead to incorrect tau-reachability information being used. Consider clearing tau_mark at appropriate points (e.g., before processing each block, or at the start of compute_weak_act when lts.is_hidden_label(label)).

Copilot · 2025-12-06T20:35:27Z

crates/reduction/src/simple_block_partition.rs

+    fn block_number(&self, state_index: StateIndex) -> BlockIndex {
+        for (block_index, block) in self.blocks.iter().enumerate() {
+            for element in block.iter(&self.elements) {
+                if element == state_index {
+                    return BlockIndex::new(block_index);
+                }
+            }
+        }
+
+        panic!("State index {:?} not found in partition {:?}", state_index, self);
+    }


The block_number implementation uses a linear search through all blocks and their elements, resulting in O(n*m) complexity where n is the number of blocks and m is the average block size. This could be a significant performance bottleneck since partition refinement algorithms frequently query block membership. Consider maintaining an auxiliary state-to-block mapping (similar to IndexedPartition) for O(1) lookups, or document this performance characteristic if the linear search is intentional for the "naive" implementation.

Copilot · 2025-12-06T20:35:27Z

crates/reduction/src/weak_bisimulation.rs

+/// Apply weak bisimulation reduction
+pub fn weak_bisimulation(lts: impl LTS, timing: &mut Timing) -> (LabelledTransitionSystem, SimpleBlockPartition) {
+    let mut time_pre = timing.start("preprocessing");
+    let scc_partition = tau_scc_decomposition(&lts);


The scc_partition variable is computed but never used. The preprocess_branching function (line 32) internally calls tau_scc_decomposition as well, making this line redundant. Consider removing this unused variable.

Suggested change

let scc_partition = tau_scc_decomposition(&lts);

Copilot · 2025-12-06T20:35:28Z

crates/reduction/src/weak_bisimulation.rs

+            let expected = reduce_lts(lts.clone(), Equivalence::WeakBisim, &mut timing);
+            let reduced = reduce_lts(lts, Equivalence::WeakBisimSigref, &mut timing);
+
+            assert_eq!(expected.num_of_states(), reduced.num_of_states());
+            assert_eq!(expected.num_of_transitions(), reduced.num_of_transitions());
+
+            println!("Expected: {expected:?}");
+            println!("Reduced: {reduced:?}");
+
+            assert!(compare_lts(Equivalence::StrongBisim, expected, &reduced, &mut timing));


The variable names expected and reduced are misleading. Line 165 uses Equivalence::WeakBisim (the new implementation being added in this PR) and assigns it to expected, while line 166 uses Equivalence::WeakBisimSigref (the reference implementation) and assigns it to reduced. These names should be swapped, or better yet, use more descriptive names like new_impl and reference_impl to clearly indicate which is the implementation under test.

Suggested change

let expected = reduce_lts(lts.clone(), Equivalence::WeakBisim, &mut timing);

let reduced = reduce_lts(lts, Equivalence::WeakBisimSigref, &mut timing);

assert_eq!(expected.num_of_states(), reduced.num_of_states());

assert_eq!(expected.num_of_transitions(), reduced.num_of_transitions());

println!("Expected: {expected:?}");

println!("Reduced: {reduced:?}");

assert!(compare_lts(Equivalence::StrongBisim, expected, &reduced, &mut timing));

let new_impl = reduce_lts(lts.clone(), Equivalence::WeakBisim, &mut timing);

let reference_impl = reduce_lts(lts, Equivalence::WeakBisimSigref, &mut timing);

assert_eq!(new_impl.num_of_states(), reference_impl.num_of_states());

assert_eq!(new_impl.num_of_transitions(), reference_impl.num_of_transitions());

println!("New implementation: {new_impl:?}");

println!("Reference implementation: {reference_impl:?}");

assert!(compare_lts(Equivalence::StrongBisim, new_impl, &reference_impl, &mut timing));

mlaveaux self-assigned this Dec 6, 2025

mlaveaux added the enhancement New feature or request label Dec 6, 2025

mlaveaux requested a review from Copilot December 6, 2025 15:36

Copilot started reviewing on behalf of mlaveaux December 6, 2025 15:42 View session

Copilot AI reviewed Dec 6, 2025

View reviewed changes

mlaveaux force-pushed the feature/weak-bisim branch 2 times, most recently from 4730728 to 07a9994 Compare December 6, 2025 19:00

mlaveaux added 2 commits December 6, 2025 20:27

Implemented the naive weak bisimulation algorithm proposed by Eduardo

6bcfc8a

Fixed several suggestions on the pull request.

7bc03a6

mlaveaux force-pushed the feature/weak-bisim branch from 07a9994 to 7bc03a6 Compare December 6, 2025 19:28

mlaveaux requested a review from Copilot December 6, 2025 19:28

Copilot AI reviewed Dec 6, 2025

View reviewed changes

Copilot started reviewing on behalf of mlaveaux December 6, 2025 19:59 View session

mlaveaux requested a review from Copilot December 6, 2025 20:26

Copilot started reviewing on behalf of mlaveaux December 6, 2025 20:28 View session

Copilot AI reviewed Dec 6, 2025

View reviewed changes

		/// Sets s.act_mark to true iff exists t: S. s =!a=> t
		/// If a = tau, then also updates s.tau_mark

-/// Sets s.act_mark to true iff exists t: S. s =!a=> t
-/// If a = tau, then also updates s.tau_mark
+/// Sets s.act_mark to true iff there exists t ∈ S such that s =!a=> t.
+/// Here, "s =!a=> t" denotes a weak transition: there is a sequence of zero or more tau (silent) transitions from s,
+/// followed by an 'a' transition, followed by zero or more tau transitions, leading to t.
+/// If a = tau, then also updates s.tau_mark.

Implemented the naive weak bisimulation algorithm proposed by Eduardo #42

Are you sure you want to change the base?

Implemented the naive weak bisimulation algorithm proposed by Eduardo #42

Uh oh!

Conversation

mlaveaux commented Dec 6, 2025

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants