Added a symbolic signature refinement algorithm

Cargo.toml

@@ -8,7 +8,7 @@ version = "1.0.0"
 
 # Add debug information to the release binaries.
 [profile.release]
-lto = "fat"
+lto = "thin"
 panic = "abort"
 debug = "line-tables-only"
 split-debuginfo= "packed"
@@ -63,7 +63,6 @@ hashbrown = "0.16"
 html-escape = "0.2"
 itertools = "0.14"
 log = { version = "0.4", features = ["kv"] }
-mt-kahypar = "0.2"
 num = "0.4"
 oxidd = { version = "0.11", features = ["manager-pointer"] }
 oxidd-dump = "0.6"

README.md

@@ -18,7 +18,9 @@ Various tools have been implemented so far:
  - `merc-vpg` can be used to solve (variability) parity games in the [PGSolver](https://github.com/tcsprojects/pgsolver) `.pg` format, and a slightly extended variability parity game `.vpg` format. Furthermore, it can generate variability parity games for model checking modal mu-calculus on LTSs.
  - `merc-pbes` can identify symmetries in parameterised boolean equation systems [PBES](https://doi.org/10.1016%2Fj.tcs.2005.06.016), located in the `tools/mcrl2` workspace.
  - `merc-ltsgraph` is a GUI tool to visualize LTSs, located in the `tools/gui` workspace.
- - `merc-sym` can explore a symbolic state space given in Sylvan's binary `.ldd` format, or the mCRL2 symbolic binary `.sym` format. It can also compute orderings using MINCE when the `kahypar` feature is enabled.
+ - `merc-sym` can explore a symbolic state space given in Sylvan's binary `.ldd`
+   format, or the mCRL2 symbolic binary `.sym` format. It can also compute
+   variable orderings using MINCE when the `kahypar` feature is enabled.
 
 Various crates are also published on [crates.io](https://crates.io/users/mlaveaux), see the [crates](./crates) directory for an overview.
 

crates/ldd/src/test_utility.rs

@@ -1,8 +1,9 @@
 //! Functions in this module are only relevant for testing purposes.
 
 use rand::Rng;
-use rand::RngExt;
 use std::collections::HashSet;
+
+use rand::RngExt;
 use streaming_iterator::StreamingIterator;
 
 use crate::Ldd;

crates/symbolic/Cargo.toml

@@ -11,8 +11,6 @@ rust-version.workspace = true
 version.workspace = true
 
 [features]
-# Enable kahypar support to enable the MINCE algorithm, only works on Linux and macOS.
-kahypar = ["dep:mt-kahypar"]
 # Derive additional traits for clap.
 clap = ["dep:clap"]
 # Enables keeping track of various performance metrics.
@@ -28,9 +26,9 @@ merc_lts.workspace = true
 merc_utilities.workspace = true
 
 clap = { workspace = true, optional = true }
+duct.workspace = true
 itertools.workspace = true
 log.workspace = true
-mt-kahypar = { workspace = true, optional = true }
 oxidd-core.workspace = true
 oxidd-dump.workspace = true
 oxidd.workspace = true

crates/symbolic/data/kahypar.ini

@@ -0,0 +1,71 @@
+# general
+mode=direct
+objective=cut
+seed=-1
+cmaxnet=1000
+vcycles=0
+quiet=1
+# main -> preprocessing -> min hash sparsifier
+p-use-sparsifier=true
+p-sparsifier-min-median-he-size=28
+p-sparsifier-max-hyperedge-size=1200
+p-sparsifier-max-cluster-size=10
+p-sparsifier-min-cluster-size=2
+p-sparsifier-num-hash-func=5
+p-sparsifier-combined-num-hash-func=100
+# main -> preprocessing -> community detection
+p-detect-communities=true
+p-detect-communities-in-ip=true
+p-reuse-communities=false
+p-max-louvain-pass-iterations=150
+p-min-eps-improvement=0.0001
+p-louvain-edge-weight=hybrid
+# main -> coarsening
+c-type=ml_style
+c-s=1
+c-t=160
+# main -> coarsening -> rating
+c-rating-score=heavy_edge 
+c-rating-use-communities=true
+c-rating-heavy_node_penalty=no_penalty
+c-rating-acceptance-criterion=best_prefer_unmatched
+c-fixed-vertex-acceptance-criterion=fixed_vertex_allowed
+# main -> initial partitioning
+i-mode=recursive
+i-technique=multi
+# initial partitioning -> coarsening
+i-c-type=ml_style
+i-c-s=1
+i-c-t=150
+# initial partitioning -> coarsening -> rating
+i-c-rating-score=heavy_edge 
+i-c-rating-use-communities=true
+i-c-rating-heavy_node_penalty=no_penalty
+i-c-rating-acceptance-criterion=best_prefer_unmatched
+i-c-fixed-vertex-acceptance-criterion=fixed_vertex_allowed
+# initial partitioning -> initial partitioning
+i-algo=pool
+i-runs=200
+# initial partitioning -> bin packing
+i-bp-algorithm=worst_fit
+i-bp-heuristic-prepacking=false
+i-bp-early-restart=true
+i-bp-late-restart=true
+# initial partitioning -> local search
+i-r-type=twoway_fm
+i-r-runs=-1
+i-r-fm-stop=simple
+i-r-fm-stop-i=50
+# main -> local search
+r-type=kway_fm_hyperflow_cutter
+r-runs=-1
+r-fm-stop=adaptive_opt
+r-fm-stop-alpha=1
+r-fm-stop-i=350
+# local_search -> flow scheduling and heuristics
+r-flow-execution-policy=exponential
+# local_search -> hyperflowcutter configuration
+r-hfc-size-constraint=mf-style
+r-hfc-scaling=16
+r-hfc-distance-based-piercing=true
+r-hfc-mbc=true

crates/symbolic/src/dependency_graph.rs

@@ -1,5 +1,7 @@
 use std::fmt;
 
+use log::trace;
+
 /// Represents a dependency graph between variables used in symbolic transition relations.
 pub struct DependencyGraph {
     /// The list of relations in the dependency graph.
@@ -25,6 +27,32 @@ impl DependencyGraph {
         }
     }
 
+    /// Restrict the dependency graph to the given vertices, and reorder them according to the given order.
+    pub fn reorder(&self, vertices: &[usize]) -> Self {
+        let mut new_relations = Vec::with_capacity(self.relations.len());
+
+        for relation in &self.relations {
+            let mut new_read_vars: Vec<usize> = relation
+                .read_vars()
+                .filter_map(|var| vertices.iter().position(|&v| v == var))
+                .collect();
+
+            let mut new_write_vars: Vec<usize> = relation
+                .write_vars()
+                .filter_map(|var| vertices.iter().position(|&v| v == var))
+                .collect();
+
+            new_read_vars.sort_unstable();
+            new_write_vars.sort_unstable();
+
+            if !new_read_vars.is_empty() || !new_write_vars.is_empty() {
+                new_relations.push(Relation::new(new_read_vars, new_write_vars));
+            }
+        }
+
+        DependencyGraph::new(new_relations)
+    }
+
     /// Returns the number of vertices in the dependency graph.
     pub fn num_of_vertices(&self) -> usize {
         self.num_of_vertices
@@ -39,11 +67,21 @@ impl DependencyGraph {
     pub fn relations(&self) -> impl Iterator<Item = &Relation> {
         self.relations.iter()
     }
+
+    /// Returns the total span of all relations in the dependency graph.
+    pub fn total_span(&self) -> usize {
+        self.relations.iter().map(|rel| rel.span()).sum()
+    }
 }
 
 impl fmt::Debug for DependencyGraph {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        writeln!(f, "DependencyGraph with {} vertices:", self.num_of_vertices)?;
+        writeln!(
+            f,
+            "graph with {} vertices, and {} hyper-edges",
+            self.num_of_vertices,
+            self.relations.len()
+        )?;
         for (i, relation) in self.relations.iter().enumerate() {
             writeln!(f, "  {}: {:?}", i, relation)?;
         }
@@ -73,6 +111,20 @@ impl Relation {
     pub fn write_vars(&self) -> impl Iterator<Item = usize> + '_ {
         self.write_vars.iter().copied()
     }
+
+    /// Returns the span of the relation, i.e., the range between the minimum and maximum
+    /// variable indices used by this relation.
+    pub fn span(&self) -> usize {
+        let min_read = self.read_vars.iter().min().copied().unwrap_or(usize::MAX);
+        let max_read = self.read_vars.iter().max().copied().unwrap_or(0);
+        let min_write = self.write_vars.iter().min().copied().unwrap_or(usize::MAX);
+        let max_write = self.write_vars.iter().max().copied().unwrap_or(0);
+
+        let min_var = min_read.min(min_write);
+        let max_var = max_read.max(max_write);
+
+        if max_var >= min_var { max_var - min_var + 1 } else { 0 }
+    }
 }
 
 impl fmt::Debug for Relation {
@@ -81,14 +133,18 @@ impl fmt::Debug for Relation {
     }
 }
 
-/// Parses a dependency graph as output by
+/// Parses a dependency graph as output by the `--info` option of both
 /// [lpreach](https://mcrl2.org/web/user_manual/tools/release/lpsreach.html) and
-/// [pbessolvesymbolic](https://mcrl2.org/web/user_manual/tools/release/pbessolvesymbolic.html)
-/// flag `--info`.
+/// [pbessolvesymbolic](https://mcrl2.org/web/user_manual/tools/release/pbessolvesymbolic.html).
 pub fn parse_compacted_dependency_graph(input: &str) -> DependencyGraph {
+    trace!("Parsing dependency graph:\n{}", input);
     let mut relations = Vec::new();
 
     for line in input.lines() {
+        if line == "read/write patterns compacted" {
+            continue;
+        }
+
         // Keep only pattern characters, ignoring indices/whitespace
         let pattern: Vec<char> = line.chars().filter(|c| matches!(c, '+' | '-' | 'r' | 'w')).collect();