diff --git a/crates/reduction/src/signature_refinement.rs b/crates/reduction/src/signature_refinement.rs index ce38309..6647700 100644 --- a/crates/reduction/src/signature_refinement.rs +++ b/crates/reduction/src/signature_refinement.rs @@ -15,6 +15,9 @@ 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::weak_bisim_signature_sorted_top; use crate::BlockPartition; use crate::BlockPartitionBuilder; use crate::IncomingTransitions; @@ -47,7 +50,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 +111,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 +143,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 +178,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 +339,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 +378,19 @@ 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. + let slice = arena.alloc_slice_copy(&builder); + state_to_signature[state_index] = Signature::new(slice); + } + } + + 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..4cef30c 100644 --- a/crates/reduction/src/signatures.rs +++ b/crates/reduction/src/signatures.rs @@ -214,6 +214,106 @@ 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. +/// 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, + 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( + 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..afaf4de 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)] @@ -51,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> { @@ -61,13 +66,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) && !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) + } 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 +90,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)?);