From 73a0e9c9b0cd8fe769a07ae53ab9462d0d8e3ea6 Mon Sep 17 00:00:00 2001 From: Jan Martens Date: Wed, 1 Oct 2025 12:56:24 +0200 Subject: [PATCH 1/3] Very naive, yet not so slow implementation of weak bisimilarity. --- crates/reduction/src/signature_refinement.rs | 47 ++++++++++++++-- crates/reduction/src/signatures.rs | 57 ++++++++++++++++++++ tools/ltsinfo/src/main.rs | 17 +++++- 3 files changed, 115 insertions(+), 6 deletions(-) diff --git a/crates/reduction/src/signature_refinement.rs b/crates/reduction/src/signature_refinement.rs index ce38309..20e8880 100644 --- a/crates/reduction/src/signature_refinement.rs +++ b/crates/reduction/src/signature_refinement.rs @@ -15,6 +15,8 @@ use crate::branching_bisim_signature_sorted; use crate::combine_partition; use crate::preprocess_branching; use crate::strong_bisim_signature; +use crate::weak_bisim_signature_sorted; +use crate::weak_bisim_signature_sorted_taus; use crate::BlockPartition; use crate::BlockPartitionBuilder; use crate::IncomingTransitions; @@ -47,7 +49,7 @@ pub fn strong_bisim_sigref(lts: &LabelledTransitionSystem, timing: &mut Timing) /// Computes a strong bisimulation partitioning using signature refinement pub fn strong_bisim_sigref_naive(lts: &LabelledTransitionSystem, timing: &mut Timing) -> IndexedPartition { let mut time = timing.start("reduction"); - let partition = signature_refinement_naive(lts, |state_index, partition, _, builder| { + let partition = signature_refinement_naive::<_, false>(lts, |state_index, partition, _, builder| { strong_bisim_signature(state_index, lts, partition, builder); }); @@ -108,7 +110,7 @@ pub fn branching_bisim_sigref(lts: &LabelledTransitionSystem, timing: &mut Timin debug_assert_eq!( partition, - signature_refinement_naive(&preprocessed_lts, |state_index, partition, _, builder| { + signature_refinement_naive::<_, false>(&preprocessed_lts, |state_index, partition, _, builder| { branching_bisim_signature( state_index, &preprocessed_lts, @@ -140,7 +142,7 @@ pub fn branching_bisim_sigref_naive(lts: &LabelledTransitionSystem, timing: &mut let mut visited = FxHashSet::default(); let mut stack = Vec::new(); - let partition = signature_refinement_naive( + let partition = signature_refinement_naive::<_, false>( &preprocessed_lts, |state_index, partition, state_to_signature, builder| { branching_bisim_signature_sorted(state_index, &preprocessed_lts, partition, state_to_signature, builder); @@ -175,6 +177,30 @@ pub fn branching_bisim_sigref_naive(lts: &LabelledTransitionSystem, timing: &mut combined_partition } +/// Computes a branching bisimulation partitioning using signature refinement without dirty blocks. +pub fn weak_bisim_sigref_naive(lts: &LabelledTransitionSystem, timing: &mut Timing) -> IndexedPartition { + let mut timepre = timing.start("preprocess"); + let (preprocessed_lts, preprocess_partition) = preprocess_branching(lts); + timepre.finish(); + + let mut time = timing.start("reduction"); + + let partition = signature_refinement_naive::<_, true>( + &preprocessed_lts, + |state_index, partition, state_to_signature, builder| { + weak_bisim_signature_sorted(state_index, &preprocessed_lts, partition, state_to_signature, builder) + }, + ); + time.finish(); + + // Combine the SCC partition with the branching bisimulation partition. + let combined_partition = combine_partition(preprocess_partition, &partition); + + trace!("Final partition {combined_partition}"); + combined_partition +} + + /// General signature refinement algorithm that accepts an arbitrary signature /// /// The signature function is called for each state and should fill the @@ -312,12 +338,13 @@ where partition } + /// General signature refinement algorithm that accepts an arbitrary signature /// /// The signature function is called for each state and should fill the /// signature builder with the signature of the state. It consists of the /// current partition, the signatures per state for the next partition. -fn signature_refinement_naive(lts: &LabelledTransitionSystem, mut signature: F) -> IndexedPartition +fn signature_refinement_naive(lts: &LabelledTransitionSystem, mut signature: F) -> IndexedPartition where F: FnMut(usize, &IndexedPartition, &Vec, &mut SignatureBuilder), { @@ -350,6 +377,18 @@ where // Remove the current signatures. arena.reset(); + if WEAK { + for state_index in lts.iter_states() { + weak_bisim_signature_sorted_taus(state_index, <s,&partition, &state_to_signature, &mut builder); + + trace!("State {state_index} signature {:?}", builder); + + // Keep track of the index for every state, either use the arena to allocate space or simply borrow the value. + state_to_signature[state_index] = Signature::new(&builder); + } + } + + for state_index in lts.iter_states() { // Compute the signature of a single state diff --git a/crates/reduction/src/signatures.rs b/crates/reduction/src/signatures.rs index e207d63..83baf87 100644 --- a/crates/reduction/src/signatures.rs +++ b/crates/reduction/src/signatures.rs @@ -214,6 +214,63 @@ pub fn branching_bisim_signature_inductive( builder.dedup(); } +/// The input lts must contain no tau-cycles. +pub fn weak_bisim_signature_sorted( + state_index: StateIndex, + lts: &LabelledTransitionSystem, + partition: &impl Partition, + state_to_signature: &[Signature], + builder: &mut SignatureBuilder, +) { + builder.clear(); + builder.push((0, partition.block_number(state_index))); // Add the inert tau transition to itself. + for &(label_index, to) in lts.outgoing_transitions(state_index) { + let to_block = partition.block_number(to); + + if lts.is_hidden_label(label_index) { + // Inert tau transition, take signature from the outgoing tau-transition. + builder.extend(state_to_signature[to].as_slice()); + } else { + builder.push((label_index, to_block)); + for (label_after,color) in state_to_signature[to].as_slice() { + if lts.is_hidden_label(*label_after) { + builder.push((label_index,*color)); + } + } + } + } + + // Compute the flat signature, which has Hash and is more compact. + builder.sort_unstable(); + builder.dedup(); +} + +/// The input lts must contain no tau-cycles. +/// This computes only tau signatures. +pub fn weak_bisim_signature_sorted_taus( + state_index: StateIndex, + lts: &LabelledTransitionSystem, + partition: &impl Partition, + state_to_signature: &[Signature], + builder: &mut SignatureBuilder, +) { + builder.clear(); + builder.push((0, partition.block_number(state_index))); // Add the inert tau transition to itself. + for &(label_index, to) in lts.outgoing_transitions(state_index) { + if lts.is_hidden_label(label_index) { + let to_block = partition.block_number(to); + + // Inert tau transition, take signature from the outgoing tau-transition. + builder.extend(state_to_signature[to].as_slice()); + builder.push((label_index, to_block)); + } + } + // Compute the flat signature, which has Hash and is more compact. + builder.sort_unstable(); + builder.dedup(); +} + + /// Perform the preprocessing necessary for branching bisimulation with the /// sorted signature see `branching_bisim_signature_sorted`. pub fn preprocess_branching(lts: &LabelledTransitionSystem) -> (LabelledTransitionSystem, IndexedPartition) { diff --git a/tools/ltsinfo/src/main.rs b/tools/ltsinfo/src/main.rs index 4c93f06..364809d 100644 --- a/tools/ltsinfo/src/main.rs +++ b/tools/ltsinfo/src/main.rs @@ -14,6 +14,7 @@ use mcrl2rust_reduction::branching_bisim_sigref_naive; use mcrl2rust_reduction::quotient_lts; use mcrl2rust_reduction::strong_bisim_sigref; use mcrl2rust_reduction::strong_bisim_sigref_naive; +use mcrl2rust_reduction::weak_bisim_sigref_naive; use mcrl2rust_reduction::IndexedPartition; use mcrl2rust_utilities::Timing; @@ -35,6 +36,7 @@ enum Equivalence { StrongBisimNaive, BranchingBisim, BranchingBisimNaive, + WeakBisim, } #[derive(clap::Parser, Debug)] @@ -61,13 +63,23 @@ fn main() -> Result> { let file = File::open(cli.filename)?; let mut timing = Timing::new(); - let lts = read_aut(&file, cli.tau.unwrap_or_default())?; + let lts = { + if matches!(cli.equivalence, Equivalence::WeakBisim) { + let lts = read_aut(&file, cli.tau.unwrap_or_default())?; + timing.start("branching bisim"); + quotient_lts(<s, &branching_bisim_sigref(<s, &mut timing), true) + } else { + read_aut(&file, cli.tau.unwrap_or_default())? + } + }; + let partition: IndexedPartition = match cli.equivalence { Equivalence::StrongBisim => strong_bisim_sigref(<s, &mut timing), Equivalence::StrongBisimNaive => strong_bisim_sigref_naive(<s, &mut timing), Equivalence::BranchingBisim => branching_bisim_sigref(<s, &mut timing), Equivalence::BranchingBisimNaive => branching_bisim_sigref_naive(<s, &mut timing), + Equivalence::WeakBisim => weak_bisim_sigref_naive(<s, &mut timing) }; let mut quotient_time = timing.start("quotient"); @@ -75,7 +87,8 @@ fn main() -> Result> { <s, &partition, matches!(cli.equivalence, Equivalence::BranchingBisim) - || matches!(cli.equivalence, Equivalence::BranchingBisimNaive), + || matches!(cli.equivalence, Equivalence::BranchingBisimNaive) + || matches!(cli.equivalence, Equivalence::WeakBisim) ); if let Some(file) = cli.output { let mut writer = BufWriter::new(File::create(file)?); From db9fe52acb8f86e7f35ee40770eeac41eaf04678 Mon Sep 17 00:00:00 2001 From: Jan Martens Date: Wed, 1 Oct 2025 15:29:12 +0200 Subject: [PATCH 2/3] less naive weak bisimilarity --- crates/reduction/src/signature_refinement.rs | 3 +- crates/reduction/src/signatures.rs | 42 ++++++++++++++++++++ tools/ltsinfo/src/main.rs | 5 ++- 3 files changed, 48 insertions(+), 2 deletions(-) diff --git a/crates/reduction/src/signature_refinement.rs b/crates/reduction/src/signature_refinement.rs index 20e8880..6cd3145 100644 --- a/crates/reduction/src/signature_refinement.rs +++ b/crates/reduction/src/signature_refinement.rs @@ -17,6 +17,7 @@ use crate::preprocess_branching; use crate::strong_bisim_signature; use crate::weak_bisim_signature_sorted; use crate::weak_bisim_signature_sorted_taus; +use crate::weak_bisim_signature_sorted_top; use crate::BlockPartition; use crate::BlockPartitionBuilder; use crate::IncomingTransitions; @@ -188,7 +189,7 @@ pub fn weak_bisim_sigref_naive(lts: &LabelledTransitionSystem, timing: &mut Timi let partition = signature_refinement_naive::<_, true>( &preprocessed_lts, |state_index, partition, state_to_signature, builder| { - weak_bisim_signature_sorted(state_index, &preprocessed_lts, partition, state_to_signature, builder) + weak_bisim_signature_sorted_top(state_index, &preprocessed_lts, partition, state_to_signature, builder) }, ); time.finish(); diff --git a/crates/reduction/src/signatures.rs b/crates/reduction/src/signatures.rs index 83baf87..de19a0d 100644 --- a/crates/reduction/src/signatures.rs +++ b/crates/reduction/src/signatures.rs @@ -245,6 +245,48 @@ pub fn weak_bisim_signature_sorted( builder.dedup(); } + +/// The input lts must contain no tau-cycles. +/// We only store top elements w.r.t. the topological sort in the signature +/// I assume this is correct, but am not completely sure. +pub fn weak_bisim_signature_sorted_top( + state_index: StateIndex, + lts: &LabelledTransitionSystem, + partition: &impl Partition, + state_to_signature: &[Signature], + builder: &mut SignatureBuilder, +) { + builder.clear(); + builder.push((0, partition.block_number(state_index))); // Add the inert tau transition to itself. + let mut filter: Vec<(usize,usize)> = vec![]; + + for &(label_index, to) in lts.outgoing_transitions(state_index) { + let to_block = partition.block_number(to); + if lts.is_hidden_label(label_index) { + // Inert tau transition, take signature from the outgoing tau-transition. + builder.extend(state_to_signature[to].as_slice()); + } else { + builder.push((label_index, to_block)); + for (_label_after,color) in state_to_signature[to].as_slice().iter().take_while(|(l,_)| !lts.is_hidden_label(*l)) { + if *color != to_block { + filter.push((label_index,*color)); + } + } + filter.sort_unstable(); + filter.dedup(); + } + } + + // Compute the flat signature, which has Hash and is more compact. + filter.sort_unstable(); + filter.dedup(); + + builder.retain(|x| !filter.contains(x)); + builder.sort_unstable(); + builder.dedup(); +} + + /// The input lts must contain no tau-cycles. /// This computes only tau signatures. pub fn weak_bisim_signature_sorted_taus( diff --git a/tools/ltsinfo/src/main.rs b/tools/ltsinfo/src/main.rs index 364809d..afaf4de 100644 --- a/tools/ltsinfo/src/main.rs +++ b/tools/ltsinfo/src/main.rs @@ -53,6 +53,9 @@ struct Cli { #[arg(long)] time: bool, + + #[arg(long, help = "Disable preprocessing the LTS by branching bisimulation minimization before computing weak bisimilarity.")] + weakonly: bool, } fn main() -> Result> { @@ -65,7 +68,7 @@ fn main() -> Result> { let mut timing = Timing::new(); let lts = { - if matches!(cli.equivalence, Equivalence::WeakBisim) { + if matches!(cli.equivalence, Equivalence::WeakBisim) && !cli.weakonly { let lts = read_aut(&file, cli.tau.unwrap_or_default())?; timing.start("branching bisim"); quotient_lts(<s, &branching_bisim_sigref(<s, &mut timing), true) From 8cace8a5ee181d357ba8feba43a80932ffb22f71 Mon Sep 17 00:00:00 2001 From: Jan Martens Date: Thu, 2 Oct 2025 12:39:35 +0200 Subject: [PATCH 3/3] switched to more naive, but correct method --- crates/reduction/src/signature_refinement.rs | 5 +++-- crates/reduction/src/signatures.rs | 1 + 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/crates/reduction/src/signature_refinement.rs b/crates/reduction/src/signature_refinement.rs index 6cd3145..6647700 100644 --- a/crates/reduction/src/signature_refinement.rs +++ b/crates/reduction/src/signature_refinement.rs @@ -189,7 +189,7 @@ pub fn weak_bisim_sigref_naive(lts: &LabelledTransitionSystem, timing: &mut Timi let partition = signature_refinement_naive::<_, true>( &preprocessed_lts, |state_index, partition, state_to_signature, builder| { - weak_bisim_signature_sorted_top(state_index, &preprocessed_lts, partition, state_to_signature, builder) + weak_bisim_signature_sorted(state_index, &preprocessed_lts, partition, state_to_signature, builder) }, ); time.finish(); @@ -385,7 +385,8 @@ where trace!("State {state_index} signature {:?}", builder); // Keep track of the index for every state, either use the arena to allocate space or simply borrow the value. - state_to_signature[state_index] = Signature::new(&builder); + let slice = arena.alloc_slice_copy(&builder); + state_to_signature[state_index] = Signature::new(slice); } } diff --git a/crates/reduction/src/signatures.rs b/crates/reduction/src/signatures.rs index de19a0d..4cef30c 100644 --- a/crates/reduction/src/signatures.rs +++ b/crates/reduction/src/signatures.rs @@ -249,6 +249,7 @@ pub fn weak_bisim_signature_sorted( /// The input lts must contain no tau-cycles. /// We only store top elements w.r.t. the topological sort in the signature /// I assume this is correct, but am not completely sure. +/// [WIP] this currently not correct. pub fn weak_bisim_signature_sorted_top( state_index: StateIndex, lts: &LabelledTransitionSystem,