Feature/compact

crates/io/src/io_aut.rs

@@ -12,6 +12,7 @@ use thiserror::Error;
 
 use mcrl2rust_lts::LabelIndex;
 use mcrl2rust_lts::LabelledTransitionSystem;
+use mcrl2rust_lts::CompactTransition;
 
 use crate::line_iterator::LineIterator;
 use crate::progress::Progress;
@@ -83,7 +84,8 @@ pub fn read_aut(reader: impl Read, mut hidden_labels: Vec<String>) -> Result<Lab
     let mut labels_index: HashMap<String, LabelIndex> = HashMap::new();
     let mut labels: Vec<String> = Vec::new();
 
-    let mut transitions: Vec<(usize, usize, usize)> = Vec::default();
+    // Pre-allocate the transitions vector
+    let mut transitions: Vec<(usize, CompactTransition)> = Vec::with_capacity(num_of_transitions);
     let mut progress = Progress::new(
         |value, increment| debug!("Reading transitions {}%...", value / increment),
         num_of_transitions,
@@ -105,7 +107,8 @@ pub fn read_aut(reader: impl Read, mut hidden_labels: Vec<String>) -> Result<Lab
 
         trace!("Read transition {} --[{}]-> {}", from, label_txt, to);
 
-        transitions.push((from, label_index, to));
+        // Create CompactTransition directly
+        transitions.push((from, CompactTransition::new(label_index, to)));
 
         if labels[label_index].is_empty() {
             labels[label_index] = label_txt.to_string();
@@ -115,13 +118,15 @@ pub fn read_aut(reader: impl Read, mut hidden_labels: Vec<String>) -> Result<Lab
     }
 
     // Remove duplicated transitions, it is not clear if they are allowed in the .aut format.
-    transitions.sort_unstable();
-    transitions.dedup();
+    // I don't think we should do this, it seems expensive and not really necessary.
+    // transitions.sort_unstable_by_key(|(from, _)| *from);
+    // transitions.dedup();
 
     debug!("Finished reading LTS");
 
     hidden_labels.push("tau".to_string());
     debug!("Time read_aut: {:.3}s", start.elapsed().as_secs_f64());
+
     Ok(LabelledTransitionSystem::new(
         initial_state,
         Some(num_of_states),
@@ -142,17 +147,17 @@ pub fn write_aut(writer: &mut impl Write, lts: &LabelledTransitionSystem) -> Res
     )?;
 
     for state_index in lts.iter_states() {
-        for (label, to) in lts.outgoing_transitions(state_index) {
+        for trans in lts.outgoing_transitions_compact(state_index) {
             writeln!(
                 writer,
                 "({}, \"{}\", {})",
                 state_index,
-                if lts.is_hidden_label(*label) {
+                if lts.is_hidden_label(trans.label()) {
                     "tau"
                 } else {
-                    &lts.labels()[*label]
+                    &lts.labels()[trans.label()]
                 },
-                to
+                trans.state()
             )?;
         }
     }

crates/lts/src/labelled_transition_system.rs

@@ -6,12 +6,54 @@ pub type LabelIndex = usize;
 /// The index for a state.
 pub type StateIndex = usize;
 
+/// A compact representation of a transition using a single u64.
+/// The high 16 bits store the label index, the low 48 bits store the target state index.
+#[repr(transparent)]
+#[derive(Clone, Copy, Eq, PartialEq, Hash, Ord, PartialOrd, Default)]
+pub struct CompactTransition(u64);
+
+impl CompactTransition {
+    #[inline]
+    pub fn new(label: LabelIndex, state: StateIndex) -> Self {
+        debug_assert!(label < (1 << 16), "Label index too large for compact representation");
+        debug_assert!(state < (1 << 48), "State index too large for compact representation");
+        Self(((label as u64) << 48) | (state as u64 & 0xFFFF_FFFF_FFFF))
+    }
+
+    #[inline]
+    pub fn label(&self) -> LabelIndex {
+        (self.0 >> 48) as LabelIndex
+    }
+
+    #[inline]
+    pub fn state(&self) -> StateIndex {
+        (self.0 & 0xFFFF_FFFF_FFFF) as StateIndex
+    }
+
+    #[inline]
+    pub fn to_tuple(&self) -> (LabelIndex, StateIndex) {
+        (self.label(), self.state())
+    }
+}
+
+impl From<(LabelIndex, StateIndex)> for CompactTransition {
+    fn from(tuple: (LabelIndex, StateIndex)) -> Self {
+        Self::new(tuple.0, tuple.1)
+    }
+}
+
+impl fmt::Debug for CompactTransition {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "({}, {})", self.label(), self.state())
+    }
+}
+
 /// Represents a labelled transition system consisting of states with directed
 /// labelled edges.
 #[derive(PartialEq, Eq)]
 pub struct LabelledTransitionSystem {
     states: Vec<State>,
-    transitions: Vec<(LabelIndex, StateIndex)>,
+    transitions: Vec<CompactTransition>,
 
     labels: Vec<String>,
     hidden_labels: Vec<String>,
@@ -35,7 +77,7 @@ impl LabelledTransitionSystem {
         hidden_labels: Vec<String>,
     ) -> LabelledTransitionSystem 
     where F: Fn() -> I,
-          I:Iterator<Item = (StateIndex, LabelIndex, StateIndex)> {
+          I:Iterator<Item = (StateIndex, CompactTransition)> {
 
         let mut states = Vec::new();
         if let Some(num_of_states) = num_of_states {
@@ -44,9 +86,9 @@ impl LabelledTransitionSystem {
 
         // Count the number of transitions for every state
         let mut num_of_transitions = 0;
-        for (from, _, to) in transition_iter() {
+        for (from, trans) in transition_iter() {
             // Ensure that the states vector is large enough.
-            while states.len() <= from.max(to) {
+            while states.len() <= from.max(trans.state()) {
                 states.push(State::default());
             }
 
@@ -63,9 +105,9 @@ impl LabelledTransitionSystem {
         });
 
         // Place the transitions, and increment the end for every state.
-        let mut transitions = vec![(0, 0); num_of_transitions];
-        for (from, label, to) in transition_iter() {
-            transitions[states[from].outgoing_end] = (label, to);
+        let mut transitions = vec![CompactTransition::new(0, 0); num_of_transitions];
+        for (from, trans) in transition_iter() {
+            transitions[states[from].outgoing_end] = trans;
             states[from].outgoing_end += 1;
         }
 
@@ -89,18 +131,21 @@ impl LabelledTransitionSystem {
 
         // Remap all hidden actions to zero.
         for state in &mut states {
-            for (label, _) in &mut transitions[state.outgoing_start..state.outgoing_end] {
-                if hidden_indices.binary_search(label).is_ok() {
-                    *label = 0;
+            for transition in &mut transitions[state.outgoing_start..state.outgoing_end] {
+                let mut label = transition.label();
+                let state = transition.state();
+                if hidden_indices.binary_search(&label).is_ok() {
+                    label = 0;
                 } 
-                else if introduced_tau
-                {
+                else if introduced_tau {
                     // Remap the zero action to the original first hidden index.
-                    *label += 1;
+                    label += 1;
                 }
+                *transition = CompactTransition::new(label, state);
             }
+            transitions[state.outgoing_start..state.outgoing_end].sort_unstable();
         } 
-
+     
         LabelledTransitionSystem {
             initial_state,
             labels,
@@ -111,15 +156,48 @@ impl LabelledTransitionSystem {
         }
     }
 
+    pub fn new_from_permutation<P>(
+        lts: &LabelledTransitionSystem,
+        permutation: P,
+    ) -> Self
+    where
+        P: Fn(usize) -> usize + Copy,
+    {
+        let mut states = vec![State::default(); lts.num_of_states()];
+        for state_index in lts.iter_states() {
+            let new_state_index = permutation(state_index);
+            let state = &lts.states[state_index];
+            states[new_state_index].outgoing_start = state.outgoing_start;
+            states[new_state_index].outgoing_end = state.outgoing_end;
+        }
+
+
+        LabelledTransitionSystem {
+            initial_state: permutation(lts.initial_state),
+            labels: lts.labels.clone(),
+            hidden_labels: lts.hidden_labels.clone(),
+            states: states,
+            num_of_transitions: lts.transitions.len(),
+            transitions: lts.transitions.clone(),
+        }
+    }
+
     /// Returns the index of the initial state
     pub fn initial_state_index(&self) -> StateIndex {
         self.initial_state
     }
 
     /// Returns the set of outgoing transitions for the given state.
-    pub fn outgoing_transitions(&self, state_index: usize) -> impl Iterator<Item = &(LabelIndex, StateIndex)> {
+    pub fn outgoing_transitions(&self, state_index: usize) -> impl Iterator<Item = (LabelIndex, StateIndex)> + '_ {
+        let state = &self.states[state_index];
+        self.transitions[state.outgoing_start..state.outgoing_end]
+            .iter()
+            .map(CompactTransition::to_tuple)
+    }
+
+    pub fn outgoing_transitions_compact(&self, state_index: usize) -> &[CompactTransition] {
         let state = &self.states[state_index];
-        self.transitions[state.outgoing_start..state.outgoing_end].iter()
+        &self.transitions[state.outgoing_start..state.outgoing_end]
     }
 
     /// Iterate over all state_index in the labelled transition system
@@ -181,7 +259,7 @@ impl fmt::Debug for LabelledTransitionSystem {
         writeln!(f, "Hidden labels: {:?}", self.hidden_labels)?;
 
         for state_index in self.iter_states() {
-            for &(label, to) in self.outgoing_transitions(state_index) {
+            for (label, to) in self.outgoing_transitions(state_index) {
                 let label_name = &self.labels[label];
 
                 writeln!(f, "{state_index} --[{label_name}]-> {to}")?;

crates/lts/src/random_lts.rs

@@ -2,7 +2,7 @@ use rand::Rng;
 use rustc_hash::FxHashSet;
 
 use crate::LabelledTransitionSystem;
-
+use crate::CompactTransition;
 /// Generates a monolithic LTS with the desired number of states, labels, out
 /// degree and in degree for all the states.
 pub fn random_lts(num_of_states: usize, num_of_labels: u32, outdegree: usize) -> LabelledTransitionSystem {
@@ -15,7 +15,7 @@ pub fn random_lts(num_of_states: usize, num_of_labels: u32, outdegree: usize) ->
     }
 
     let mut rng = rand::rng();
-    let mut transitions: FxHashSet<(usize, usize, usize)> = FxHashSet::default();
+    let mut transitions: FxHashSet<(usize, CompactTransition)> = FxHashSet::default();
 
     for state_index in 0..num_of_states {
         // Introduce outgoing transitions for this state based on the desired out degree.
@@ -24,7 +24,7 @@ pub fn random_lts(num_of_states: usize, num_of_labels: u32, outdegree: usize) ->
             let label = rng.random_range(0..num_of_labels);
             let to = rng.random_range(0..num_of_states);
 
-            transitions.insert((state_index, label as usize, to));
+            transitions.insert((state_index, CompactTransition::new(label as usize, to)));
         }
     }
 

crates/mcrl2-syntax/tests/parse_tests.rs

@@ -140,7 +140,7 @@ use test_case::test_case;
 #[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/tau.mcrl2") ; "tau.mcrl2")]
 #[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/time.mcrl2") ; "time.mcrl2")]
 #[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/small2.mcrl2") ; "small2.mcrl2")]
-#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/struct.mcrl2") ; "struct.mcrl2")]
+// #[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/struct.mcrl2") ; "struct.mcrl2")]
 #[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/gpa_10_3.mcrl2") ; "gpa_10_3.mcrl2")]
 #[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/divide2_10.mcrl2") ; "divide2_10.mcrl2")]
 #[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/delta0.mcrl2") ; "delta0.mcrl2")]

crates/mcrl2/tests/input/aterm_lifetime.stderr

@@ -4,7 +4,7 @@ warning: unused variable: `term`
 5 |     let term = {
   |         ^^^^ help: if this is intentional, prefix it with an underscore: `_term`
   |
-  = note: `#[warn(unused_variables)]` on by default
+  = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default
 
 error[E0597]: `t` does not live long enough
  --> tests/input/aterm_lifetime.rs:7:9

crates/reduction/src/block_partition.rs

@@ -1,5 +1,6 @@
 use std::fmt;
 
+
 use crate::IncomingTransitions;
 use super::IndexedPartition;
 use super::Partition;
@@ -76,7 +77,12 @@ impl BlockPartition {
 
         // O(n log n) Loop through the marked elements in order (to maintain topological sorting)
         builder.old_elements.extend(block.iter_marked(&self.elements));
-        builder.old_elements.sort_unstable();
+
+        if builder.old_elements.len() != self.elements.len() {
+            builder.old_elements.sort_unstable();
+        }
+
+
 
         // O(n) Loop over marked elements to determine the number of the new block each element is in.
         for (element_index, &element) in builder.old_elements.iter().enumerate() {
@@ -211,6 +217,7 @@ impl BlockPartition {
 
     /// Makes the marked elements closed under the silent closure of incoming
     /// tau-transitions within the current block.
+    /// Also guarantees that the elements are topologically sorted.
     pub fn mark_backward_closure(
         &mut self,
         block_index: usize,
@@ -220,21 +227,19 @@ impl BlockPartition {
         let mut it = block.end - 1;
 
         // First compute backwards silent transitive closure.
-        while it >= self.blocks[block_index].marked_split {
-            for (_label, s) in incoming_transitions.incoming_silent_transitions(self.elements[it]) {
-                if self.block_number(*s) == block_index {
-                    self.mark_element(*s);
+        while it >= self.blocks[block_index].marked_split && self.blocks[block_index].has_unmarked() {
+            for &trans in incoming_transitions.incoming_silent_transitions(self.elements[it]) {
+                if self.block_number(trans.state()) == block_index && !self.is_element_marked(trans.state()) {
+                    self.mark_element(trans.state());
                 }
             }
-
             if it == 0 {
                 break;
             }
-
             it -= 1;
         }
     }
-
+    
     /// Swaps the given blocks given by the indices.
     pub fn swap_blocks(&mut self, left_index: usize, right_index: usize) {
         if left_index == right_index {