Added naive (and less naive) signature that computes weak bisimilarity

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<F>(lts: &LabelledTransitionSystem, mut signature: F) -> IndexedPartition
+fn signature_refinement_naive<F, const WEAK: bool>(lts: &LabelledTransitionSystem, mut signature: F) -> IndexedPartition
 where
     F: FnMut(usize, &IndexedPartition, &Vec<Signature>, &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, &lts,&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

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) {

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<ExitCode, Box<dyn Error>> {
@@ -61,21 +66,32 @@ fn main() -> Result<ExitCode, Box<dyn Error>> {
     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(&lts, &branching_bisim_sigref(&lts, &mut timing), true)
+        } else {
+            read_aut(&file, cli.tau.unwrap_or_default())?
+        }
+    };
+
     let partition: IndexedPartition = match cli.equivalence {
         Equivalence::StrongBisim => strong_bisim_sigref(&lts, &mut timing),
         Equivalence::StrongBisimNaive => strong_bisim_sigref_naive(&lts, &mut timing),
         Equivalence::BranchingBisim => branching_bisim_sigref(&lts, &mut timing),
         Equivalence::BranchingBisimNaive => branching_bisim_sigref_naive(&lts, &mut timing),
+        Equivalence::WeakBisim => weak_bisim_sigref_naive(&lts, &mut timing)
     };
 
     let mut quotient_time = timing.start("quotient");
     let quotient_lts = quotient_lts(
         &lts,
         &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)?);