From 0f6bd2321e524847d54a0ab031d0741c6c12982b Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Thu, 18 Dec 2025 22:01:56 +0100 Subject: [PATCH 01/40] Changed boost-include-only to the upstream directory --- .gitmodules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitmodules b/.gitmodules index 111c9c36..1d61476e 100644 --- a/.gitmodules +++ b/.gitmodules @@ -3,7 +3,7 @@ url = https://github.com/mCRL2org/mCRL2.git [submodule "3rd-party/boost-include-only"] path = 3rd-party/boost-include-only - url = https://github.com/mlaveaux/boost-include-only.git + url = https://github.com/MERCorg/boost-include-only.git [submodule "3rd-party/cpptrace"] path = 3rd-party/cpptrace url = https://github.com/jeremy-rifkin/cpptrace.git From fbb627e384e0b13a312ee8bc4ba96be830236404 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 19 Dec 2025 15:20:13 +0100 Subject: [PATCH 02/40] Parse permutations in cycle notation --- tools/mcrl2/pbes/src/permutation.rs | 65 +++++++++++++++++++++++++++-- 1 file changed, 61 insertions(+), 4 deletions(-) diff --git a/tools/mcrl2/pbes/src/permutation.rs b/tools/mcrl2/pbes/src/permutation.rs index bb04ff83..d2c0855f 100644 --- a/tools/mcrl2/pbes/src/permutation.rs +++ b/tools/mcrl2/pbes/src/permutation.rs @@ -32,13 +32,16 @@ impl Permutation { // Sort by domain for deterministic representation. mapping.sort_unstable_by_key(|(d, _)| *d); // debug_assert!(mapping.iter().all(|(from, to)| from != to), "Mapping should not contain identity mappings."); - debug_assert!(mapping.iter().duplicates().count() == 0, "Mapping should not contain duplicate domain entries."); + debug_assert!( + mapping.iter().duplicates().count() == 0, + "Mapping should not contain duplicate domain entries." + ); Permutation { mapping } } /// Parse a permutation from a string input of the form "[0->2, 1->0, 2->1]". - pub fn from_input(line: &str) -> Result { + pub fn from_mapping_notation(line: &str) -> Result { // Remove the surrounding brackets if present. let trimmed_input = line.trim(); let input_no_brackets = @@ -83,6 +86,47 @@ impl Permutation { Ok(Permutation::from_mapping(pairs)) } + /// Parse a permutation in cycle notation, e.g., (0 2 1)(3 4). + pub fn from_cycle_notation(cycle_notation: &str) -> Result { + let mut mapping: Vec<(usize, usize)> = Vec::new(); + + // Split the input into cycles by finding all '(...)' groups + for cycle_str in cycle_notation.split('(').skip(1) { + // Find the closing parenthesis + let cycle_content = cycle_str + .split(')') + .next() + .ok_or_else(|| MercError::from("Invalid cycle notation: missing closing ')'"))?; + + // Skip empty cycles + if cycle_content.trim().is_empty() { + continue; + } + + // Parse all numbers in this cycle + let cycle_elements: Result, MercError> = cycle_content + .split_whitespace() + .map(|num_str| { + num_str + .parse::() + .map_err(|_| MercError::from(format!("Invalid number in cycle notation: {}", num_str))) + }) + .collect(); + + let cycle_elements = cycle_elements?; + + // Create mappings for the current cycle (each element maps to the next) + let len = cycle_elements.len(); + for i in 0..len { + let from = cycle_elements[i]; + let to = cycle_elements[(i + 1) % len]; + mapping.push((from, to)); + } + } + + Ok(Permutation::from_mapping(mapping)) + } + /// Construct a new permutation by concatenating two (disjoint) permutations. pub fn concat(self, other: &Permutation) -> Permutation { debug_assert!( @@ -109,6 +153,11 @@ impl Permutation { key // It is the identity on unspecified elements. } + /// Returns an iterator over the domain of this permutation. + pub fn domain(&self) -> impl Iterator + '_ { + self.mapping.iter().map(|(d, _)| *d) + } + /// Check whether this permutation is the identity permutation. pub fn is_identity(&self) -> bool { self.mapping.iter().all(|(d, v)| d == v) @@ -211,19 +260,27 @@ mod tests { #[test] fn test_permutation_from_input() { - let permutation = Permutation::from_input("[0-> 2, 1 ->0, 2->1]").unwrap(); + let permutation = Permutation::from_mapping_notation("[0-> 2, 1 ->0, 2->1]").unwrap(); assert!(permutation.mapping == vec![(0, 2), (1, 0), (2, 1)]); } #[test] fn test_cycle_notation() { - let permutation = Permutation::from_input("[0->2, 1->0, 2->1, 3->4, 4->3]").unwrap(); + let permutation = Permutation::from_mapping_notation("[0->2, 1->0, 2->1, 3->4, 4->3]").unwrap(); println!("{:?}", permutation.mapping); assert_eq!(permutation.to_string(), "(0 2 1)(3 4)"); } + #[test] + fn test_cycle_notation_parsing() { + let permutation = Permutation::from_cycle_notation("(0 2 1)(3 4)").unwrap(); + println!("{:?}", permutation.mapping); + + assert_eq!(permutation.mapping, vec![(0, 2), (1, 0), (2, 1), (3, 4), (4, 3)]); + } + #[test] fn test_permutation_group() { let indices = vec![0, 3, 5]; From 078e7140f326d0ac942fac4fc24e1b482624aebb Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 19 Dec 2025 15:21:40 +0100 Subject: [PATCH 03/40] Allow cycle notation for the now --permutation option. Improved printing somewhat. --- tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h | 7 +++-- tools/mcrl2/crates/mcrl2-sys/src/pbes.rs | 2 +- tools/mcrl2/crates/mcrl2/src/pbes.rs | 9 +++++- tools/mcrl2/pbes/src/main.rs | 20 +++++++++++-- tools/mcrl2/pbes/src/symmetry.rs | 38 ++++++++++++++++++++---- 5 files changed, 62 insertions(+), 14 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h index 50f2821c..03f3e0ac 100644 --- a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h @@ -72,10 +72,11 @@ rust::String mcrl2_pbes_to_string(const pbes& pbesspec) } inline -rust::String mcrl2_pbes_expression_to_string(const atermpp::aterm& expr) +rust::String mcrl2_pbes_expression_to_string(const atermpp::detail::_aterm& expr) { + atermpp::unprotected_aterm_core tmp(&expr); std::stringstream ss; - ss << expr; + ss << atermpp::down_cast(tmp); return ss.str(); } @@ -309,7 +310,7 @@ const atermpp::detail::_aterm* mcrl2_srf_summand_variable(const srf_summand& sum inline const atermpp::detail::_aterm* mcrl2_srf_summand_condition(const srf_summand& summand) { - return atermpp::detail::address(summand.variable()); + return atermpp::detail::address(summand.condition()); } std::unique_ptr mcrl2_pbes_expression_replace_variables(const atermpp::detail::_aterm& expr, const rust::Vec& sigma); diff --git a/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs b/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs index b0051c72..97f9acd0 100644 --- a/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs @@ -154,6 +154,6 @@ pub mod ffi { pi: &Vec, ) -> UniquePtr; - fn mcrl2_pbes_expression_to_string(expression: &aterm) -> String; + fn mcrl2_pbes_expression_to_string(expression: &_aterm) -> String; } } diff --git a/tools/mcrl2/crates/mcrl2/src/pbes.rs b/tools/mcrl2/crates/mcrl2/src/pbes.rs index 3c686508..a4a34b8a 100644 --- a/tools/mcrl2/crates/mcrl2/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2/src/pbes.rs @@ -17,6 +17,7 @@ use mcrl2_sys::pbes::ffi::mcrl2_local_control_flow_graph_vertices; use mcrl2_sys::pbes::ffi::mcrl2_pbes_data_specification; use mcrl2_sys::pbes::ffi::mcrl2_pbes_expression_replace_propositional_variables; use mcrl2_sys::pbes::ffi::mcrl2_pbes_expression_replace_variables; +use mcrl2_sys::pbes::ffi::mcrl2_pbes_expression_to_string; use mcrl2_sys::pbes::ffi::mcrl2_pbes_is_propositional_variable; use mcrl2_sys::pbes::ffi::mcrl2_pbes_to_srf_pbes; use mcrl2_sys::pbes::ffi::mcrl2_pbes_to_string; @@ -411,7 +412,7 @@ impl fmt::Debug for SrfSummand { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!( f, - "Summand(condition: {:?}, variable: {:?})", + "Summand(condition: {}, variable: {})", self.condition(), self.variable() ) @@ -464,6 +465,12 @@ impl PbesExpression { } } +impl fmt::Display for PbesExpression { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", mcrl2_pbes_expression_to_string(self.term.get())) + } +} + impl fmt::Debug for PbesExpression { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "{}", self.term) diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index 353ecace..6cfdab4d 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -59,12 +59,13 @@ struct SymmetryArgs { format: Option, /// Pass a single permutation in cycles notation to check for begin a (syntactic) symmetry + #[arg(long)] permutation: Option, + /// Partition data parameters into their sorts before considering their permutation groups #[arg( long, - default_value_t = false, - help = "Partition data parameters into their sorts before considering their permutation groups" + default_value_t = false )] partition_data_sorts: bool, } @@ -97,7 +98,20 @@ fn main() -> Result { let algorithm = SymmetryAlgorithm::new(&pbes, false)?; if let Some(permutation) = &args.permutation { - let pi = Permutation::from_input(permutation)?; + let pi = if permutation.contains("[") { + Permutation::from_mapping_notation(permutation)? + } else { + Permutation::from_cycle_notation(permutation)? + }; + + if let Err(x) = algorithm.is_valid_permutation(&pi) { + info!("The given permutation is not valid:\n\t - {}", + x + ); + return Ok(ExitCode::FAILURE); + } + + info!("Checking permutation: {}", pi); if algorithm.check_symmetry(&pi) { println!("true"); } else { diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 551c46b9..52904da1 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -32,13 +32,16 @@ use crate::permutation::permutation_group_size; /// Implements symmetry detection for PBESs. pub struct SymmetryAlgorithm { - state_graph: PbesStategraph, // Needs to be kept alive while the control flow graphs are used. + /// Needs to be kept alive while the control flow graphs are used. + state_graph: PbesStategraph, - parameters: Vec, // The parameters of the unified SRF PBES. + /// The parameters of the unified SRF PBES. + parameters: Vec, - all_control_flow_parameters: Vec, // Keeps track of all parameters identified as control flow parameters. + all_control_flow_parameters: Vec, - srf: SrfPbes, // The SRF PBES after unifying parameters. + /// The SRF PBES after unifying parameters. + srf: SrfPbes, /// Keep track of some progress messages. num_of_checked_candidates: Cell, @@ -71,8 +74,8 @@ impl SymmetryAlgorithm { }; info!( - "Unified parameters: {:?}", - parameters.iter().map(|p| (p.name(), p.sort())).format(", ") + "Unified parameters: {}", + parameters.iter().format(", ") ); let state_graph = PbesStategraph::run(&srf.to_pbes())?; @@ -147,6 +150,29 @@ impl SymmetryAlgorithm { combined_candidates.map(|(alpha, beta)| alpha.concat(&beta)) } + /// Checks whether the given permutation is valid, meaning that control flow parameters are mapped to control flow parameters. + pub fn is_valid_permutation(&self, pi: &Permutation) -> Result<(), MercError> { + // Check that all control flow parameters are mapped to control flow parameters. + for index in pi.domain() { + let mapped_index = pi.value(index); + if self.all_control_flow_parameters.contains(&index) != self.all_control_flow_parameters.contains(&mapped_index) { + return Err(format!( + "A parameter at index {} is mapped to parameter at index {}, but they are not both control flow parameters.", + index, mapped_index + ).into()); + } + + if index >= self.parameters.len() || mapped_index >= self.parameters.len() { + return Err(format!( + "A parameter at index {} is mapped to parameter at index {}, but the PBES only has {} parameters.", + index, mapped_index, self.parameters.len() + ).into()); + } + } + + Ok(()) + } + /// Performs the syntactic check defined as symcheck in the paper. pub fn check_symmetry(&self, pi: &Permutation) -> bool { for equation in self.srf.equations() { From 07c585a9407ab1c9018e15aa12f7e876b603ba1f Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 24 Dec 2025 19:44:43 +0100 Subject: [PATCH 04/40] Fixed several suggestions --- tools/mcrl2/pbes/src/main.rs | 6 ++---- tools/mcrl2/pbes/src/symmetry.rs | 1 + 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index 6cfdab4d..538afe0f 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -98,16 +98,14 @@ fn main() -> Result { let algorithm = SymmetryAlgorithm::new(&pbes, false)?; if let Some(permutation) = &args.permutation { - let pi = if permutation.contains("[") { + let pi = if permutation.trim_start().starts_with("[") { Permutation::from_mapping_notation(permutation)? } else { Permutation::from_cycle_notation(permutation)? }; if let Err(x) = algorithm.is_valid_permutation(&pi) { - info!("The given permutation is not valid:\n\t - {}", - x - ); + info!("The given permutation is not valid: {x}"); return Ok(ExitCode::FAILURE); } diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 52904da1..5838a6e0 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -38,6 +38,7 @@ pub struct SymmetryAlgorithm { /// The parameters of the unified SRF PBES. parameters: Vec, + /// The indices of all control flow parameters in the PBES. all_control_flow_parameters: Vec, /// The SRF PBES after unifying parameters. From 1f5157d7a53cafda413a82edeaf1606114fcaa27 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sun, 4 Jan 2026 22:03:03 +0100 Subject: [PATCH 05/40] Added a proper partitioning function, also to be used for other filters. --- tools/mcrl2/pbes/src/main.rs | 6 ++-- tools/mcrl2/pbes/src/permutation.rs | 1 + tools/mcrl2/pbes/src/symmetry.rs | 56 +++++++++++++++++------------ 3 files changed, 37 insertions(+), 26 deletions(-) diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index 538afe0f..0ddf9ff7 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -58,16 +58,16 @@ struct SymmetryArgs { #[arg(long, short('i'), value_enum)] format: Option, - /// Pass a single permutation in cycles notation to check for begin a (syntactic) symmetry + /// Pass a single permutation in cycles notation to check whether it is a symmetry. #[arg(long)] permutation: Option, - /// Partition data parameters into their sorts before considering their permutation groups + /// Partition data parameters into their sorts before considering their permutation groups. #[arg( long, default_value_t = false )] - partition_data_sorts: bool, + partition_data_sorts: bool, } fn main() -> Result { diff --git a/tools/mcrl2/pbes/src/permutation.rs b/tools/mcrl2/pbes/src/permutation.rs index d2c0855f..25af8301 100644 --- a/tools/mcrl2/pbes/src/permutation.rs +++ b/tools/mcrl2/pbes/src/permutation.rs @@ -159,6 +159,7 @@ impl Permutation { } /// Check whether this permutation is the identity permutation. + #[cfg(test)] pub fn is_identity(&self) -> bool { self.mapping.iter().all(|(d, v)| d == v) } diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 5838a6e0..27280e28 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -256,30 +256,14 @@ impl SymmetryAlgorithm { // Groups the data parameters by their sort. let (mut number_of_permutations, all_data_groups) = if partition_data_sorts { - let same_sort_parameters = { - let mut result: Vec> = Vec::new(); - - for (index, param) in self.parameters.iter().enumerate() { - if self.all_control_flow_parameters.contains(&index) { - // Skip control flow parameters. - continue; - } - - let sort = param.sort(); - if let Some(group) = result.iter_mut().find(|g: &&mut Vec<_>| { - if let Some(first) = g.first() { - first.sort() == sort - } else { - false - } - }) { - group.push(param.clone()); - } else { - result.push(vec![param.clone()]); - } + let same_sort_parameters = partition(self.parameters.iter().enumerate().filter_map(|(index, param)| { + if self.all_control_flow_parameters.contains(&index) { + // Skip control flow parameters. + None + } else { + Some(param) } - result - }; + }), |lhs, rhs| lhs.sort() == rhs.sort()); let mut number_of_permutations = 1usize; let mut all_data_groups: Box> = Box::new(iter::empty()); // Default value is overwritten in first iteration. @@ -640,6 +624,32 @@ impl SymmetryAlgorithm { } } +/// Partition a vector into a number of sets based on a predicate. +fn partition(elements: I, predicate: P) -> Vec> +where + I: Iterator, + P: Fn(&T, &T) -> bool, + T: Clone, +{ + let mut result: Vec> = Vec::new(); + + for element in elements { + + if let Some(group) = result.iter_mut().find(|g: &&mut Vec<_>| { + if let Some(first) = g.first() { + predicate(first, &element) + } else { + false + } + }) { + group.push(element.clone()); + } else { + result.push(vec![element.clone()]); + } + } + result +} + /// Returns the index of the variable that the control flow graph considers fn variable_index(cfg: &ControlFlowGraph) -> usize { // Check that all the vertices have the same variable assigned for consistency From cdd965b3b2f6a3e5bf1fe4957151afedeab28a43 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 6 Jan 2026 21:53:29 +0100 Subject: [PATCH 06/40] Added the pbes expression variants --- .../mcrl2/crates/mcrl2/src/data_expression.rs | 247 +++++++++++---- .../mcrl2/crates/mcrl2/src/pbes_expression.rs | 280 ++++++++++++++++++ 2 files changed, 468 insertions(+), 59 deletions(-) create mode 100644 tools/mcrl2/crates/mcrl2/src/pbes_expression.rs diff --git a/tools/mcrl2/crates/mcrl2/src/data_expression.rs b/tools/mcrl2/crates/mcrl2/src/data_expression.rs index 54c46862..27616569 100644 --- a/tools/mcrl2/crates/mcrl2/src/data_expression.rs +++ b/tools/mcrl2/crates/mcrl2/src/data_expression.rs @@ -1,3 +1,4 @@ +use mcrl2_macros::mcrl2_derive_terms; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_abstraction; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_application; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_data_expression; @@ -6,8 +7,7 @@ use mcrl2_sys::data::ffi::mcrl2_data_expression_is_machine_number; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_untyped_identifier; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_variable; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_where_clause; - -use mcrl2_macros::mcrl2_derive_terms; +use mcrl2_sys::data::ffi::mcrl2_data_expression_to_string; use mcrl2_sys::data::ffi::mcrl2_is_data_sort_expression; use crate::ATermRef; @@ -69,11 +69,11 @@ pub fn is_sort_expression(term: &ATermRef<'_>) -> bool { // This module is only used internally to run the proc macro. #[mcrl2_derive_terms] mod inner { + use super::*; + use std::fmt; - use mcrl2_macros::mcrl2_ignore; use mcrl2_macros::mcrl2_term; - use mcrl2_sys::data::ffi::mcrl2_data_expression_to_string; use crate::ATerm; use crate::ATermArgs; @@ -81,13 +81,6 @@ mod inner { use crate::ATermString; use crate::Markable; use crate::Todo; - use crate::is_abstraction; - use crate::is_application; - use crate::is_data_expression; - use crate::is_function_symbol; - use crate::is_machine_number; - use crate::is_sort_expression; - use crate::is_variable; /// Represents a data::data_expression from the mCRL2 toolset. /// A data expression can be any of: @@ -108,12 +101,6 @@ mod inner { } impl DataExpression { - /// Creates a new data::data_expression from the given term. - #[mcrl2_ignore] - pub fn new(term: ATerm) -> Self { - Self { term } - } - /// Returns the head symbol a data expression /// - function symbol f -> f /// - application f(t_0, ..., t_n) -> f @@ -170,7 +157,7 @@ mod inner { } else if is_variable(&self.term) { write!(f, "{}", DataVariableRef::from(self.term.copy())) } else if is_machine_number(&self.term) { - write!(f, "{}", MachineNumberRef::from(self.term.copy())) + write!(f, "{}", DataMachineNumberRef::from(self.term.copy())) } else { write!(f, "{}", self.term) } @@ -184,13 +171,6 @@ mod inner { } impl DataVariable { - /// Creates a new data::variable from the given aterm. - #[mcrl2_ignore] - pub fn new(term: ATerm) -> Self { - debug_assert!(is_variable(&term.copy())); - DataVariable { term } - } - /// Returns the name of the variable. pub fn name(&self) -> ATermString { ATermString::new(self.term.arg(0).protect()) @@ -215,13 +195,6 @@ mod inner { } impl DataApplication { - /// Creates a new data::application from the given term. - #[mcrl2_ignore] - pub(crate) fn new(term: ATerm) -> Self { - debug_assert!(is_application(&term.copy())); - DataApplication { term } - } - /// Returns the head symbol a data application pub fn data_function_symbol(&self) -> DataFunctionSymbolRef<'_> { self.term.arg(0).upgrade(&self.term).into() @@ -272,15 +245,6 @@ mod inner { term: ATerm, } - impl DataAbstraction { - /// Creates a new data::abstraction from the given term. - #[mcrl2_ignore] - pub(crate) fn new(term: ATerm) -> Self { - debug_assert!(is_abstraction(&term.copy())); - DataAbstraction { term } - } - } - /// Represents a data::function_symbol from the mCRL2 toolset. #[mcrl2_term(is_function_symbol)] pub struct DataFunctionSymbol { @@ -288,13 +252,6 @@ mod inner { } impl DataFunctionSymbol { - /// Creates a new data::function_symbol from the given term. - #[mcrl2_ignore] - pub(crate) fn new(term: ATerm) -> Self { - debug_assert!(is_function_symbol(&term.copy())); - DataFunctionSymbol { term } - } - /// Returns the sort of the function symbol. pub fn sort(&self) -> SortExpressionRef<'_> { self.term.arg(1).into() @@ -324,13 +281,6 @@ mod inner { } impl SortExpression { - /// Creates a new data::sort_expression from the given term. - #[mcrl2_ignore] - pub fn new(term: ATerm) -> Self { - debug_assert!(is_sort_expression(&term.copy())); - SortExpression { term } - } - /// Returns the name of the sort. pub fn name(&self) -> &str { // We only change the lifetime, but that is fine since it is derived from the current term. @@ -346,28 +296,207 @@ mod inner { /// Represents a data::machine_number from the mCRL2 toolset. #[mcrl2_term(is_machine_number)] - struct MachineNumber { + pub struct DataMachineNumber { pub term: ATerm, } - impl MachineNumber { + impl DataMachineNumber { /// Obtain the underlying value of a machine number. pub fn value(&self) -> u64 { 0 } } - impl fmt::Display for MachineNumber { + impl fmt::Display for DataMachineNumber { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "{}", self.value()) } } + + /// Represents a data::where_clause from the mCRL2 toolset. + #[mcrl2_term(is_where_clause)] + pub struct DataWhereClause { + pub term: ATerm, + } + + /// Represents a data::untyped_identifier from the mCRL2 toolset. + #[mcrl2_term(is_untyped_identifier)] + pub struct DataUntypedIdentifier { + pub term: ATerm, + } + } pub use inner::*; +// Allowed conversions impl From for DataExpression { fn from(var: DataVariable) -> Self { - DataExpression::new(var.into()) + Self::new(var.into()) + } +} + +impl From for DataExpression { + fn from(var: DataAbstraction) -> Self { + Self::new(var.into()) + } +} + +impl From for DataExpression { + fn from(var: DataApplication) -> Self { + Self::new(var.into()) + } +} + +impl From for DataExpression { + fn from(var: DataFunctionSymbol) -> Self { + Self::new(var.into()) + } +} + +impl From for DataExpression { + fn from(var: DataMachineNumber) -> Self { + Self::new(var.into()) + } +} + +impl From for DataExpression { + fn from(var: DataWhereClause) -> Self { + Self::new(var.into()) + } +} + +impl From for DataExpression { + fn from(var: DataUntypedIdentifier) -> Self { + Self::new(var.into()) + } +} + +// Reference variants +impl<'a> From> for DataExpressionRef<'a> { + fn from(var: DataVariableRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataExpressionRef<'a> { + fn from(var: DataAbstractionRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataExpressionRef<'a> { + fn from(var: DataApplicationRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataExpressionRef<'a> { + fn from(var: DataFunctionSymbolRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataExpressionRef<'a> { + fn from(var: DataMachineNumberRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataExpressionRef<'a> { + fn from(var: DataWhereClauseRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataExpressionRef<'a> { + fn from(var: DataUntypedIdentifierRef<'a>) -> Self { + Self::new(var.into()) + } +} + +// Allowed conversions +impl From for DataVariable { + fn from(var: DataExpression) -> Self { + Self::new(var.into()) + } +} + +impl From for DataAbstraction { + fn from(var: DataExpression) -> Self { + Self::new(var.into()) + } +} + +impl From for DataApplication { + fn from(var: DataExpression) -> Self { + Self::new(var.into()) + } +} + +impl From for DataFunctionSymbol { + fn from(var: DataExpression) -> Self { + Self::new(var.into()) + } +} + +impl From for DataMachineNumber { + fn from(var: DataExpression) -> Self { + Self::new(var.into()) } } + +impl From for DataWhereClause { + fn from(var: DataExpression) -> Self { + Self::new(var.into()) + } +} + +impl From for DataUntypedIdentifier { + fn from(var: DataExpression) -> Self { + Self::new(var.into()) + } +} + +// Reference variants +impl<'a> From> for DataVariableRef<'a> { + fn from(var: DataExpressionRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataAbstractionRef<'a> { + fn from(var: DataExpressionRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataApplicationRef<'a> { + fn from(var: DataExpressionRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataFunctionSymbolRef<'a> { + fn from(var: DataExpressionRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataMachineNumberRef<'a> { + fn from(var: DataExpressionRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataWhereClauseRef<'a> { + fn from(var: DataExpressionRef<'a>) -> Self { + Self::new(var.into()) + } +} + +impl<'a> From> for DataUntypedIdentifierRef<'a> { + fn from(var: DataExpressionRef<'a>) -> Self { + Self::new(var.into()) + } +} \ No newline at end of file diff --git a/tools/mcrl2/crates/mcrl2/src/pbes_expression.rs b/tools/mcrl2/crates/mcrl2/src/pbes_expression.rs new file mode 100644 index 00000000..a5453878 --- /dev/null +++ b/tools/mcrl2/crates/mcrl2/src/pbes_expression.rs @@ -0,0 +1,280 @@ +use mcrl2_macros::mcrl2_derive_terms; +use mcrl2_sys::pbes::ffi::mcrl2_pbes_expression_to_string; +use mcrl2_sys::pbes::ffi::mcrl2_pbes_is_not; +use mcrl2_sys::pbes::ffi::mcrl2_pbes_is_pbes_expression; +use mcrl2_sys::pbes::ffi::mcrl2_pbes_is_propositional_variable_instantiation; + +use crate::ATermRef; + +/// Checks if this term is a data variable. +pub fn is_pbes_expression(term: &ATermRef<'_>) -> bool { + mcrl2_pbes_is_pbes_expression(term.get()) +} + +pub fn is_pbes_propositional_variable_instantiation(term: &ATermRef<'_>) -> bool { + mcrl2_pbes_is_propositional_variable_instantiation(term.get()) +} + +pub fn is_pbes_not(term: &ATermRef<'_>) -> bool { + mcrl2_pbes_is_not(term.get()) +} + +pub fn is_pbes_and(term: &ATermRef<'_>) -> bool { + mcrl2_sys::pbes::ffi::mcrl2_pbes_is_and(term.get()) +} + +pub fn is_pbes_or(term: &ATermRef<'_>) -> bool { + mcrl2_sys::pbes::ffi::mcrl2_pbes_is_or(term.get()) +} + +pub fn is_pbes_imp(term: &ATermRef<'_>) -> bool { + mcrl2_sys::pbes::ffi::mcrl2_pbes_is_imp(term.get()) +} + +pub fn is_pbes_forall(term: &ATermRef<'_>) -> bool { + mcrl2_sys::pbes::ffi::mcrl2_pbes_is_forall(term.get()) +} + +pub fn is_pbes_exists(term: &ATermRef<'_>) -> bool { + mcrl2_sys::pbes::ffi::mcrl2_pbes_is_exists(term.get()) +} + +// This module is only used internally to run the proc macro. +#[mcrl2_derive_terms] +mod inner { + use super::*; + + use std::fmt; + + use mcrl2_macros::mcrl2_term; + + use crate::ATerm; + use crate::ATermRef; + use crate::Markable; + use crate::Todo; + use crate::is_pbes_expression; + + /// mcrl2::pbes_system::pbes_expression + #[mcrl2_term(is_pbes_expression)] + pub struct PbesExpression { + term: ATerm, + } + + impl fmt::Display for PbesExpression { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", mcrl2_pbes_expression_to_string(self.term.get())) + } + } + + /// Represents a mcrl2::pbes_system::propositional_variable_instantiation + #[mcrl2_term(is_pbes_propositional_variable_instantiation)] + pub struct PbesPropositionalVariableInstantiation { + term: ATerm, + } + + /// Represents a mcrl2::pbes_system::not + #[mcrl2_term(is_pbes_not)] + pub struct PbesNot { + term: ATerm, + } + + /// Represents a mcrl2::pbes_system::and_ + #[mcrl2_term(is_pbes_and)] + pub struct PbesAnd { + term: ATerm, + } + + /// Represents a mcrl2::pbes_system::or_ + #[mcrl2_term(is_pbes_or)] + pub struct PbesOr { + term: ATerm, + } + + /// Represents a mcrl2::pbes_system::imp + #[mcrl2_term(is_pbes_imp)] + pub struct PbesImp { + term: ATerm, + } + + /// Represents a mcrl2::pbes_system::forall + #[mcrl2_term(is_pbes_forall)] + pub struct PbesForall { + term: ATerm, + } + + /// Represents a mcrl2::pbes_system::exists + #[mcrl2_term(is_pbes_exists)] + pub struct PbesExists { + term: ATerm, + } +} + +pub use inner::*; + +impl From for PbesExpression { + fn from(inst: PbesPropositionalVariableInstantiation) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesExpression { + fn from(inst: PbesNot) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesExpression { + fn from(inst: PbesAnd) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesExpression { + fn from(inst: PbesOr) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesExpression { + fn from(inst: PbesImp) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesExpression { + fn from(inst: PbesForall) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesExpression { + fn from(inst: PbesExists) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesExpressionRef<'a> { + fn from(inst: PbesPropositionalVariableInstantiationRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesExpressionRef<'a> { + fn from(inst: PbesNotRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesExpressionRef<'a> { + fn from(inst: PbesAndRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesExpressionRef<'a> { + fn from(inst: PbesOrRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesExpressionRef<'a> { + fn from(inst: PbesImpRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesExpressionRef<'a> { + fn from(inst: PbesForallRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesExpressionRef<'a> { + fn from(inst: PbesExistsRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesPropositionalVariableInstantiation { + fn from(inst: PbesExpression) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesNot { + fn from(inst: PbesExpression) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesAnd { + fn from(inst: PbesExpression) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesOr { + fn from(inst: PbesExpression) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesImp { + fn from(inst: PbesExpression) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesForall { + fn from(inst: PbesExpression) -> Self { + Self::new(inst.into()) + } +} + +impl From for PbesExists { + fn from(inst: PbesExpression) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesPropositionalVariableInstantiationRef<'a> { + fn from(inst: PbesExpressionRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesNotRef<'a> { + fn from(inst: PbesExpressionRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesAndRef<'a> { + fn from(inst: PbesExpressionRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesOrRef<'a> { + fn from(inst: PbesExpressionRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesImpRef<'a> { + fn from(inst: PbesExpressionRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesForallRef<'a> { + fn from(inst: PbesExpressionRef<'a>) -> Self { + Self::new(inst.into()) + } +} + +impl<'a> From> for PbesExistsRef<'a> { + fn from(inst: PbesExpressionRef<'a>) -> Self { + Self::new(inst.into()) + } +} From b963dcb92253f189fefa4318b13385e0b5538b5f Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 6 Jan 2026 21:54:06 +0100 Subject: [PATCH 07/40] Added visitor for the pbes expression --- tools/mcrl2/crates/mcrl2/src/visitor.rs | 168 +++++++++++++++++++----- 1 file changed, 138 insertions(+), 30 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2/src/visitor.rs b/tools/mcrl2/crates/mcrl2/src/visitor.rs index f44216e4..34d8eb6e 100644 --- a/tools/mcrl2/crates/mcrl2/src/visitor.rs +++ b/tools/mcrl2/crates/mcrl2/src/visitor.rs @@ -1,70 +1,178 @@ -use crate::DataAbstraction; -use crate::DataApplication; +use crate::DataAbstractionRef; +use crate::DataApplicationRef; use crate::DataExpression; -use crate::DataFunctionSymbol; -use crate::DataVariable; +use crate::DataExpressionRef; +use crate::DataFunctionSymbolRef; +use crate::DataMachineNumberRef; +use crate::DataUntypedIdentifierRef; +use crate::DataVariableRef; +use crate::DataWhereClauseRef; +use crate::PbesAndRef; +use crate::PbesExistsRef; +use crate::PbesExpression; +use crate::PbesForallRef; +use crate::PbesImpRef; +use crate::PbesNotRef; +use crate::PbesOrRef; +use crate::PbesPropositionalVariableInstantiationRef; use crate::is_abstraction; use crate::is_application; use crate::is_function_symbol; use crate::is_machine_number; +use crate::is_pbes_and; +use crate::is_pbes_exists; +use crate::is_pbes_forall; +use crate::is_pbes_imp; +use crate::is_pbes_not; +use crate::is_pbes_or; +use crate::is_pbes_propositional_variable_instantiation; use crate::is_untyped_identifier; use crate::is_variable; use crate::is_where_clause; pub trait DataExpressionVisitor { - fn visit_variable(&mut self, var: &DataVariable) -> DataExpression { - DataExpression::from(var.clone()) + fn visit_variable(&mut self, var: &DataVariableRef<'_>) -> DataExpression { + DataExpression::from(var.protect()) } - fn visit_application(&mut self, _app: &DataApplication) -> DataExpression { - unimplemented!() + fn visit_application(&mut self, appl: &DataApplicationRef<'_>) -> DataExpression { + DataExpression::from(appl.protect()) } - fn visit_abstraction(&mut self, _abs: &DataAbstraction) -> DataExpression { - unimplemented!() + fn visit_abstraction(&mut self, abstraction: &DataAbstractionRef<'_>) -> DataExpression { + DataExpression::from(abstraction.protect()) } - fn visit_function_symbol(&mut self, _fs: &DataFunctionSymbol) -> DataExpression { - unimplemented!() + fn visit_function_symbol(&mut self, function_symbol: &DataFunctionSymbolRef<'_>) -> DataExpression { + DataExpression::from(function_symbol.protect()) } - fn visit(&mut self, expr: &DataExpression) -> DataExpression { + fn visit_where_clause(&mut self, where_: &DataWhereClauseRef<'_>) -> DataExpression { + DataExpression::from(where_.protect()) + } + + fn visit_machine_number(&mut self, number: &DataMachineNumberRef<'_>) -> DataExpression { + DataExpression::from(number.protect()) + } + + fn visit_untyped_identifier(&mut self, identifier: &DataUntypedIdentifierRef<'_>) -> DataExpression { + DataExpression::from(identifier.protect()) + } + + fn visit(&mut self, expr: &DataExpressionRef<'_>) -> DataExpression { if is_variable(&expr.copy()) { - self.visit_variable(&DataVariable::new(expr.protect())) + self.visit_variable(&DataVariableRef::from(expr.copy())) } else if is_application(&expr.copy()) { - self.visit_application(&DataApplication::new(expr.protect())) + self.visit_application(&DataApplicationRef::from(expr.copy())) } else if is_abstraction(&expr.copy()) { - self.visit_abstraction(&DataAbstraction::new(expr.protect())) + self.visit_abstraction(&DataAbstractionRef::from(expr.copy())) } else if is_function_symbol(&expr.copy()) { - self.visit_function_symbol(&DataFunctionSymbol::new(expr.protect())) + self.visit_function_symbol(&DataFunctionSymbolRef::from(expr.copy())) } else if is_where_clause(&expr.copy()) { - unimplemented!(); + self.visit_where_clause(&DataWhereClauseRef::from(expr.copy())) } else if is_machine_number(&expr.copy()) { - unimplemented!(); + self.visit_machine_number(&DataMachineNumberRef::from(expr.copy())) } else if is_untyped_identifier(&expr.copy()) { - unimplemented!(); + self.visit_untyped_identifier(&DataUntypedIdentifierRef::from(expr.copy())) } else { - unimplemented!(); + unreachable!("Unknown data expression type"); + } + } +} + +pub trait PbesExpressionVisitor { + fn visit_propositional_variable_instantiation( + &mut self, + inst: &PbesPropositionalVariableInstantiationRef<'_>, + ) -> PbesExpression { + PbesExpression::from(inst.protect()) + } + + fn visit_not(&mut self, or: &PbesNotRef<'_>) -> PbesExpression { + PbesExpression::from(or.protect()) + } + + fn visit_and(&mut self, and: &PbesAndRef<'_>) -> PbesExpression { + PbesExpression::from(and.protect()) + } + + fn visit_or(&mut self, or: &PbesOrRef<'_>) -> PbesExpression { + PbesExpression::from(or.protect()) + } + + fn visit_imp(&mut self, imp: &PbesImpRef<'_>) -> PbesExpression { + PbesExpression::from(imp.protect()) + } + + fn visit_forall(&mut self, forall: &PbesForallRef<'_>) -> PbesExpression { + PbesExpression::from(forall.protect()) + } + + fn visit_exists(&mut self, exists: &PbesExistsRef<'_>) -> PbesExpression { + PbesExpression::from(exists.protect()) + } + + fn visit(&mut self, expr: &PbesExpression) -> PbesExpression { + if is_pbes_propositional_variable_instantiation(&expr.copy()) { + self.visit_propositional_variable_instantiation(&PbesPropositionalVariableInstantiationRef::from( + expr.copy(), + )) + } else if is_pbes_not(&expr.copy()) { + self.visit_not(&PbesNotRef::from(expr.copy())) + } else if is_pbes_and(&expr.copy()) { + self.visit_and(&PbesAndRef::from(expr.copy())) + } else if is_pbes_or(&expr.copy()) { + self.visit_or(&PbesOrRef::from(expr.copy())) + } else if is_pbes_imp(&expr.copy()) { + self.visit_imp(&PbesImpRef::from(expr.copy())) + } else if is_pbes_forall(&expr.copy()) { + self.visit_forall(&PbesForallRef::from(expr.copy())) + } else if is_pbes_exists(&expr.copy()) { + self.visit_exists(&PbesExistsRef::from(expr.copy())) + } else { + unreachable!("Unknown pbes expression type"); } } } /// Replaces data variables in the given data expression according to the /// provided substitution function. -pub fn data_expression_replace_variables( - expr: &DataExpression, - f: &impl Fn(&DataVariable) -> DataExpression, -) -> DataExpression { - struct ReplaceVariableBuilder<'a> { - apply: &'a dyn Fn(&DataVariable) -> DataExpression, +pub fn data_expression_replace_variables(expr: &DataExpressionRef<'_>, f: &F) -> DataExpression +where + F: Fn(&DataVariableRef<'_>) -> DataExpression, +{ + struct ReplaceVariableBuilder<'a, F> { + apply: &'a F, } - impl<'a> DataExpressionVisitor for ReplaceVariableBuilder<'a> { - fn visit_variable(&mut self, var: &DataVariable) -> DataExpression { - (self.apply)(var) + impl<'a, F> DataExpressionVisitor for ReplaceVariableBuilder<'a, F> + where + F: Fn(&DataVariableRef<'_>) -> DataExpression, + { + fn visit_variable(&mut self, var: &DataVariableRef<'_>) -> DataExpression { + (*self.apply)(var) } } let mut builder = ReplaceVariableBuilder { apply: f }; builder.visit(expr) } + + +pub fn pbes_expression_pvi(expr: &PbesExpression) -> Vec { + struct PviChecker; + + impl PbesExpressionVisitor for PviChecker { + fn visit_propositional_variable_instantiation( + &mut self, + _inst: &PbesPropositionalVariableInstantiationRef<'_>, + ) -> PbesExpression { + // Found a propositional variable instantiation, return true. + PbesExpression::from(_inst.protect()) + } + } + + let mut checker = PviChecker; + let result = checker.visit(expr); + is_pbes_propositional_variable_instantiation(&result.copy()) +} \ No newline at end of file From 379c2d45f37f593689e87b2e4527b040c9bd55a6 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 6 Jan 2026 21:54:34 +0100 Subject: [PATCH 08/40] Removed the original PbesExpression --- tools/mcrl2/crates/mcrl2/src/global_lock.rs | 2 +- tools/mcrl2/crates/mcrl2/src/lib.rs | 6 +++-- tools/mcrl2/crates/mcrl2/src/pbes.rs | 27 +-------------------- 3 files changed, 6 insertions(+), 29 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2/src/global_lock.rs b/tools/mcrl2/crates/mcrl2/src/global_lock.rs index 9116932c..8926f3bd 100644 --- a/tools/mcrl2/crates/mcrl2/src/global_lock.rs +++ b/tools/mcrl2/crates/mcrl2/src/global_lock.rs @@ -10,4 +10,4 @@ pub fn lock_global() -> GlobalLockGuard { } /// This is the global mutex used to guard non thread safe FFI functions. -pub(crate) static GLOBAL_MUTEX: LazyLock> = LazyLock::new(|| Mutex::new(())); \ No newline at end of file +pub(crate) static GLOBAL_MUTEX: LazyLock> = LazyLock::new(|| Mutex::new(())); diff --git a/tools/mcrl2/crates/mcrl2/src/lib.rs b/tools/mcrl2/crates/mcrl2/src/lib.rs index d3cc0539..eeeeca7f 100644 --- a/tools/mcrl2/crates/mcrl2/src/lib.rs +++ b/tools/mcrl2/crates/mcrl2/src/lib.rs @@ -1,17 +1,19 @@ //! These are Rust wrappers around the mCRL2 classes mod atermpp; -mod data_expression; mod data; +mod data_expression; mod global_lock; mod log; mod pbes; +mod pbes_expression; mod visitor; pub use atermpp::*; -pub use data_expression::*; pub use data::*; +pub use data_expression::*; pub use global_lock::*; pub use log::*; pub use pbes::*; +pub use pbes_expression::*; pub use visitor::*; diff --git a/tools/mcrl2/crates/mcrl2/src/pbes.rs b/tools/mcrl2/crates/mcrl2/src/pbes.rs index a4a34b8a..3dad7fc2 100644 --- a/tools/mcrl2/crates/mcrl2/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2/src/pbes.rs @@ -17,7 +17,6 @@ use mcrl2_sys::pbes::ffi::mcrl2_local_control_flow_graph_vertices; use mcrl2_sys::pbes::ffi::mcrl2_pbes_data_specification; use mcrl2_sys::pbes::ffi::mcrl2_pbes_expression_replace_propositional_variables; use mcrl2_sys::pbes::ffi::mcrl2_pbes_expression_replace_variables; -use mcrl2_sys::pbes::ffi::mcrl2_pbes_expression_to_string; use mcrl2_sys::pbes::ffi::mcrl2_pbes_is_propositional_variable; use mcrl2_sys::pbes::ffi::mcrl2_pbes_to_srf_pbes; use mcrl2_sys::pbes::ffi::mcrl2_pbes_to_string; @@ -48,6 +47,7 @@ use crate::ATermString; use crate::DataExpression; use crate::DataSpecification; use crate::DataVariable; +use crate::PbesExpression; use crate::lock_global; /// mcrl2::pbes_system::pbes @@ -452,31 +452,6 @@ impl fmt::Debug for PropositionalVariable { } } -/// mcrl2::pbes_system::pbes_expression -#[derive(Clone, Eq, PartialEq)] -pub struct PbesExpression { - term: ATerm, -} - -impl PbesExpression { - /// Creates a new pbes expression from the given term. - fn new(term: ATerm) -> Self { - PbesExpression { term } - } -} - -impl fmt::Display for PbesExpression { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - write!(f, "{}", mcrl2_pbes_expression_to_string(self.term.get())) - } -} - -impl fmt::Debug for PbesExpression { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - write!(f, "{}", self.term) - } -} - /// Replace variables in the given PBES expression according to the given substitution sigma. pub fn replace_variables(expr: &PbesExpression, sigma: Vec<(DataExpression, DataExpression)>) -> PbesExpression { // Do not into_iter here, as we need to keep sigma alive for the call. From 2a241038c170845422cdfb5ef142e77d619e01c9 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 6 Jan 2026 21:54:53 +0100 Subject: [PATCH 09/40] Made ATermString a proper aterm --- .../crates/mcrl2/src/atermpp/aterm_string.rs | 44 +++++++++++-------- 1 file changed, 26 insertions(+), 18 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs index 6c40bce9..b62d3b63 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs @@ -1,32 +1,40 @@ use std::fmt; -use crate::ATerm; +use mcrl2_macros::mcrl2_derive_terms; -/// Represents an atermpp::aterm_string from the mCRL2 toolset. -#[derive(PartialEq, Eq)] -pub struct ATermString { - term: ATerm, +use crate::ATermRef; + +pub fn is_aterm_string(term: &ATermRef<'_>) -> bool { + term.get_head_symbol().arity() == 0 } -impl ATermString { - /// Creates a new `ATermString` from the given term. - pub fn new(term: ATerm) -> Self { - Self { term } - } +#[mcrl2_derive_terms] +mod inner { + use mcrl2_macros::mcrl2_term; - /// Returns the string value. - pub fn str(&self) -> String { - // The Rust::Str should ensure that this is a valid string. - self.term.get_head_symbol().name().to_string() + use crate::ATerm; + use crate::ATermRef; + use crate::Markable; + use crate::Todo; + use crate::is_aterm_string; + + /// Represents an atermpp::aterm_string from the mCRL2 toolset. + #[mcrl2_term(is_aterm_string)] + pub struct ATermString { + term: ATerm, } -} -impl fmt::Debug for ATermString { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - write!(f, "{}", self.str()) + impl ATermString { + /// Returns the string value. + pub fn str(&self) -> String { + // The Rust::Str should ensure that this is a valid string. + self.term.get_head_symbol().name().to_string() + } } } +pub use inner::*; + impl fmt::Display for ATermString { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "{}", self.str()) From b59b400aac776c0a85652e63e81241142e1ce500 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 6 Jan 2026 21:55:00 +0100 Subject: [PATCH 10/40] Added new for all terms --- .../crates/mcrl2-macros/src/mcrl2_derive_terms.rs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/tools/mcrl2/crates/mcrl2-macros/src/mcrl2_derive_terms.rs b/tools/mcrl2/crates/mcrl2-macros/src/mcrl2_derive_terms.rs index c8240b85..d9f7defa 100644 --- a/tools/mcrl2/crates/mcrl2-macros/src/mcrl2_derive_terms.rs +++ b/tools/mcrl2/crates/mcrl2-macros/src/mcrl2_derive_terms.rs @@ -60,6 +60,13 @@ pub(crate) fn mcrl2_derive_terms_impl(_attributes: TokenStream, input: TokenStre let name_ref = format_ident!("{}Ref", object.ident); let generated: TokenStream = quote!( impl #name { + pub fn new(term: ATerm) -> #name { + #assertion; + #name { + term: term.into(), + } + } + pub fn copy<'a>(&'a self) -> #name_ref<'a> { self.term.copy().into() } @@ -120,6 +127,13 @@ pub(crate) fn mcrl2_derive_terms_impl(_attributes: TokenStream, input: TokenStre } impl<'a> #name_ref<'a> { + pub fn new(term: ATermRef<'a>) -> #name_ref<'a> { + #assertion; + #name_ref { + term: term.into(), + } + } + pub fn copy<'b>(&'b self) -> #name_ref<'b> { self.term.copy().into() } From fa59f076972e699e8a001b1c014fe1d6d5d38a9e Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 6 Jan 2026 21:55:17 +0100 Subject: [PATCH 11/40] Added recognizers for al lthe pbes expressions --- tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h | 58 +++++++++++++++++++ tools/mcrl2/crates/mcrl2-sys/src/pbes.rs | 14 ++++- tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs | 2 +- 3 files changed, 70 insertions(+), 4 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h index 03f3e0ac..6cb624c9 100644 --- a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h @@ -317,6 +317,64 @@ std::unique_ptr mcrl2_pbes_expression_replace_variables(const at std::unique_ptr mcrl2_pbes_expression_replace_propositional_variables(const atermpp::detail::_aterm& expr, const rust::Vec& pi); +/// mcrl2::pbes_system::pbes_expression + +inline +bool mcrl2_pbes_is_pbes_expression(const atermpp::detail::_aterm& variable) +{ + atermpp::unprotected_aterm_core tmp(&variable); + return pbes_system::is_pbes_expression(atermpp::down_cast(tmp)); +} + +inline +bool mcrl2_pbes_is_propositional_variable_instantiation(const atermpp::detail::_aterm& variable) +{ + atermpp::unprotected_aterm_core tmp(&variable); + return pbes_system::is_propositional_variable_instantiation(atermpp::down_cast(tmp)); +} + +inline +bool mcrl2_pbes_is_not(const atermpp::detail::_aterm& variable) +{ + atermpp::unprotected_aterm_core tmp(&variable); + return pbes_system::is_not(atermpp::down_cast(tmp)); +} + +inline +bool mcrl2_pbes_is_and(const atermpp::detail::_aterm& variable) +{ + atermpp::unprotected_aterm_core tmp(&variable); + return pbes_system::is_and(atermpp::down_cast(tmp)); +} + +inline +bool mcrl2_pbes_is_or(const atermpp::detail::_aterm& variable) +{ + atermpp::unprotected_aterm_core tmp(&variable); + return pbes_system::is_or(atermpp::down_cast(tmp)); +} + +inline +bool mcrl2_pbes_is_imp(const atermpp::detail::_aterm& variable) +{ + atermpp::unprotected_aterm_core tmp(&variable); + return pbes_system::is_imp(atermpp::down_cast(tmp)); +} + +inline +bool mcrl2_pbes_is_forall(const atermpp::detail::_aterm& variable) +{ + atermpp::unprotected_aterm_core tmp(&variable); + return pbes_system::is_forall(atermpp::down_cast(tmp)); +} + +inline +bool mcrl2_pbes_is_exists(const atermpp::detail::_aterm& variable) +{ + atermpp::unprotected_aterm_core tmp(&variable); + return pbes_system::is_exists(atermpp::down_cast(tmp)); +} + } // namespace mcrl2::pbes_system #endif // MCRL2_SYS_CPP_PBES_H \ No newline at end of file diff --git a/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs b/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs index 97f9acd0..06ce448a 100644 --- a/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs @@ -69,6 +69,8 @@ pub mod ffi { input: &stategraph_equation, ) -> UniquePtr>; + fn mcrl2_pbes_is_propositional_variable(expression: &_aterm) -> bool; + /// Returns the propositional variable of a pbes equation fn mcrl2_stategraph_equation_variable(equation: &stategraph_equation) -> *const _aterm; @@ -133,9 +135,6 @@ pub mod ffi { /// Returns the equations of the given srf_pbes. fn mcrl2_srf_pbes_equations(result: Pin<&mut CxxVector>, input: &srf_pbes); - /// Returns the variable of the given srf_equation. - fn mcrl2_pbes_is_propositional_variable(input: &_aterm) -> bool; - fn mcrl2_srf_summand_condition(summand: &srf_summand) -> *const _aterm; fn mcrl2_srf_summand_variable(summand: &srf_summand) -> *const _aterm; @@ -155,5 +154,14 @@ pub mod ffi { ) -> UniquePtr; fn mcrl2_pbes_expression_to_string(expression: &_aterm) -> String; + + fn mcrl2_pbes_is_pbes_expression(expression: &_aterm) -> bool; + fn mcrl2_pbes_is_propositional_variable_instantiation(expression: &_aterm) -> bool; + fn mcrl2_pbes_is_not(term: &_aterm) -> bool; + fn mcrl2_pbes_is_and(term: &_aterm) -> bool; + fn mcrl2_pbes_is_or(term: &_aterm) -> bool; + fn mcrl2_pbes_is_imp(term: &_aterm) -> bool; + fn mcrl2_pbes_is_forall(term: &_aterm) -> bool; + fn mcrl2_pbes_is_exists(term: &_aterm) -> bool; } } diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs index bd3fd452..19bcc7bf 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs @@ -19,8 +19,8 @@ use mcrl2_sys::atermpp::ffi::mcrl2_aterm_is_list; use mcrl2_sys::atermpp::ffi::mcrl2_aterm_print; use mcrl2_sys::cxx::Exception; use mcrl2_sys::cxx::UniquePtr; -use merc_utilities::PhantomUnsend; use merc_collections::ProtectionIndex; +use merc_utilities::PhantomUnsend; use crate::atermpp::SymbolRef; use crate::atermpp::THREAD_TERM_POOL; From 43a17a355ddb83bc30c881c6e26a08b154c4cc36 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 6 Jan 2026 22:53:47 +0100 Subject: [PATCH 12/40] Added various accessor functions --- .../mcrl2/crates/mcrl2/src/data_expression.rs | 13 ++-- .../mcrl2/crates/mcrl2/src/pbes_expression.rs | 74 ++++++++++++++++++- tools/mcrl2/crates/mcrl2/src/visitor.rs | 49 ++++++++---- tools/mcrl2/pbes/src/main.rs | 13 ++-- tools/mcrl2/pbes/src/symmetry.rs | 74 +++++++++++-------- 5 files changed, 166 insertions(+), 57 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2/src/data_expression.rs b/tools/mcrl2/crates/mcrl2/src/data_expression.rs index 27616569..29ace48d 100644 --- a/tools/mcrl2/crates/mcrl2/src/data_expression.rs +++ b/tools/mcrl2/crates/mcrl2/src/data_expression.rs @@ -79,6 +79,7 @@ mod inner { use crate::ATermArgs; use crate::ATermRef; use crate::ATermString; + use crate::ATermStringRef; use crate::Markable; use crate::Todo; @@ -132,9 +133,9 @@ mod inner { /// Returns the arguments of a data expression /// - function symbol f -> [] /// - application f(t_0, ..., t_n) -> [t_0, ..., t_n] - pub fn data_sort(&self) -> SortExpression { + pub fn data_sort(&self) -> SortExpressionRef<'_> { if is_function_symbol(&self.term) { - DataFunctionSymbolRef::from(self.term.copy()).sort().protect() + self.data } else if is_variable(&self.term) { DataVariableRef::from(self.term.copy()).sort() } else { @@ -172,13 +173,13 @@ mod inner { impl DataVariable { /// Returns the name of the variable. - pub fn name(&self) -> ATermString { - ATermString::new(self.term.arg(0).protect()) + pub fn name(&self) -> ATermStringRef<'_> { + self.term.arg(0).into() } /// Returns the sort of the variable. - pub fn sort(&self) -> SortExpression { - SortExpression::new(self.term.arg(1).protect()) + pub fn sort(&self) -> SortExpressionRef<'_> { + self.term.arg(1).into() } } diff --git a/tools/mcrl2/crates/mcrl2/src/pbes_expression.rs b/tools/mcrl2/crates/mcrl2/src/pbes_expression.rs index a5453878..dc449b9a 100644 --- a/tools/mcrl2/crates/mcrl2/src/pbes_expression.rs +++ b/tools/mcrl2/crates/mcrl2/src/pbes_expression.rs @@ -6,7 +6,7 @@ use mcrl2_sys::pbes::ffi::mcrl2_pbes_is_propositional_variable_instantiation; use crate::ATermRef; -/// Checks if this term is a data variable. +/// Returns true iff the given term is a PBES expression. pub fn is_pbes_expression(term: &ATermRef<'_>) -> bool { mcrl2_pbes_is_pbes_expression(term.get()) } @@ -49,7 +49,10 @@ mod inner { use mcrl2_macros::mcrl2_term; use crate::ATerm; + use crate::ATermListRef; use crate::ATermRef; + use crate::ATermStringRef; + use crate::DataExpressionRef; use crate::Markable; use crate::Todo; use crate::is_pbes_expression; @@ -72,41 +75,110 @@ mod inner { term: ATerm, } + impl PbesPropositionalVariableInstantiation { + /// Returns the name of the PVI. + pub fn name(&self) -> ATermStringRef<'_> { + self.arg(0).into() + } + + /// Returns the arguments of the PVI. + pub fn arguments(&self) -> ATermListRef<'_, DataExpressionRef<'_>> { + self.arg(1).into() + } + } + /// Represents a mcrl2::pbes_system::not #[mcrl2_term(is_pbes_not)] pub struct PbesNot { term: ATerm, } + impl PbesNot { + /// Returns the body of the not expression. + pub fn body(&self) -> PbesExpressionRef<'_> { + self.arg(0).into() + } + } + /// Represents a mcrl2::pbes_system::and_ #[mcrl2_term(is_pbes_and)] pub struct PbesAnd { term: ATerm, } + impl PbesAnd { + /// Returns the lhs of the and expression. + pub fn lhs(&self) -> PbesExpressionRef<'_> { + self.arg(0).into() + } + + /// Returns the rhs of the and expression. + pub fn rhs(&self) -> PbesExpressionRef<'_> { + self.arg(1).into() + } + } + /// Represents a mcrl2::pbes_system::or_ #[mcrl2_term(is_pbes_or)] pub struct PbesOr { term: ATerm, } + impl PbesOr { + /// Returns the lhs of the or expression. + pub fn lhs(&self) -> PbesExpressionRef<'_> { + self.arg(0).into() + } + + /// Returns the rhs of the or expression. + pub fn rhs(&self) -> PbesExpressionRef<'_> { + self.arg(1).into() + } + } + /// Represents a mcrl2::pbes_system::imp #[mcrl2_term(is_pbes_imp)] pub struct PbesImp { term: ATerm, } + impl PbesImp { + /// Returns the lhs of the imp expression. + pub fn lhs(&self) -> PbesExpressionRef<'_> { + self.arg(0).into() + } + + /// Returns the rhs of the imp expression. + pub fn rhs(&self) -> PbesExpressionRef<'_> { + self.arg(1).into() + } + } + /// Represents a mcrl2::pbes_system::forall #[mcrl2_term(is_pbes_forall)] pub struct PbesForall { term: ATerm, } + impl PbesForall { + /// Returns the body of the not expression. + pub fn body(&self) -> PbesExpressionRef<'_> { + self.arg(1).into() + } + } + /// Represents a mcrl2::pbes_system::exists #[mcrl2_term(is_pbes_exists)] pub struct PbesExists { term: ATerm, } + + impl PbesExists { + /// Returns the body of the not expression. + pub fn body(&self) -> PbesExpressionRef<'_> { + self.arg(1).into() + } + } } pub use inner::*; diff --git a/tools/mcrl2/crates/mcrl2/src/visitor.rs b/tools/mcrl2/crates/mcrl2/src/visitor.rs index 34d8eb6e..bd71254d 100644 --- a/tools/mcrl2/crates/mcrl2/src/visitor.rs +++ b/tools/mcrl2/crates/mcrl2/src/visitor.rs @@ -10,10 +10,12 @@ use crate::DataWhereClauseRef; use crate::PbesAndRef; use crate::PbesExistsRef; use crate::PbesExpression; +use crate::PbesExpressionRef; use crate::PbesForallRef; use crate::PbesImpRef; use crate::PbesNotRef; use crate::PbesOrRef; +use crate::PbesPropositionalVariableInstantiation; use crate::PbesPropositionalVariableInstantiationRef; use crate::is_abstraction; use crate::is_application; @@ -31,11 +33,13 @@ use crate::is_variable; use crate::is_where_clause; pub trait DataExpressionVisitor { - fn visit_variable(&mut self, var: &DataVariableRef<'_>) -> DataExpression { - DataExpression::from(var.protect()) + fn visit_variable(&mut self, var: &DataVariableRef<'_>) -> Option { + None } - fn visit_application(&mut self, appl: &DataApplicationRef<'_>) -> DataExpression { + fn visit_application(&mut self, appl: &DataApplicationRef<'_>) -> Option) -> PbesExpression { - PbesExpression::from(or.protect()) + fn visit_not(&mut self, not: &PbesNotRef<'_>) -> PbesExpression { + self.visit(¬.body()); + PbesExpression::from(not.protect()) } fn visit_and(&mut self, and: &PbesAndRef<'_>) -> PbesExpression { + self.visit(&and.lhs()); + self.visit(&and.rhs()); PbesExpression::from(and.protect()) } fn visit_or(&mut self, or: &PbesOrRef<'_>) -> PbesExpression { + self.visit(&or.lhs()); + self.visit(&or.rhs()); PbesExpression::from(or.protect()) } fn visit_imp(&mut self, imp: &PbesImpRef<'_>) -> PbesExpression { + self.visit(&imp.lhs()); + self.visit(&imp.rhs()); PbesExpression::from(imp.protect()) } fn visit_forall(&mut self, forall: &PbesForallRef<'_>) -> PbesExpression { + self.visit(&forall.body()); PbesExpression::from(forall.protect()) } fn visit_exists(&mut self, exists: &PbesExistsRef<'_>) -> PbesExpression { + self.visit(&exists.body()); PbesExpression::from(exists.protect()) } - fn visit(&mut self, expr: &PbesExpression) -> PbesExpression { + fn visit(&mut self, expr: &PbesExpressionRef<'_>) -> PbesExpression { if is_pbes_propositional_variable_instantiation(&expr.copy()) { self.visit_propositional_variable_instantiation(&PbesPropositionalVariableInstantiationRef::from( expr.copy(), @@ -158,21 +171,29 @@ where builder.visit(expr) } +/// Returns all the PVIs occurring in the given PBES expression. +pub fn pbes_expression_pvi(expr: &PbesExpressionRef<'_>) -> Vec { + let mut result = Vec::new(); -pub fn pbes_expression_pvi(expr: &PbesExpression) -> Vec { - struct PviChecker; + struct PviChecker<'a> { + result: &'a mut Vec, + } - impl PbesExpressionVisitor for PviChecker { + impl PbesExpressionVisitor for PviChecker<'_> { fn visit_propositional_variable_instantiation( &mut self, - _inst: &PbesPropositionalVariableInstantiationRef<'_>, + inst: &PbesPropositionalVariableInstantiationRef<'_>, ) -> PbesExpression { // Found a propositional variable instantiation, return true. - PbesExpression::from(_inst.protect()) + self.result.push(PbesPropositionalVariableInstantiation::from(inst.protect())); + PbesExpression::from(inst.protect()) } } - let mut checker = PviChecker; - let result = checker.visit(expr); - is_pbes_propositional_variable_instantiation(&result.copy()) + let mut checker = PviChecker { + result: &mut result, + }; + + checker.visit(expr); + result } \ No newline at end of file diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index 0ddf9ff7..76dbfec7 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -63,11 +63,12 @@ struct SymmetryArgs { permutation: Option, /// Partition data parameters into their sorts before considering their permutation groups. - #[arg( - long, - default_value_t = false - )] - partition_data_sorts: bool, + #[arg(long, default_value_t = false)] + partition_data_sorts: bool, + + /// Partition data parameters based on their updates. + #[arg(long, default_value_t = false)] + partition_data_updates: bool, } fn main() -> Result { @@ -116,7 +117,7 @@ fn main() -> Result { println!("false"); } } else { - for candidate in algorithm.candidates(args.partition_data_sorts) { + for candidate in algorithm.candidates(args.partition_data_sorts, args.partition_data_updates) { info!("Found candidate: {}", candidate); if algorithm.check_symmetry(&candidate) { diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 27280e28..fa2ca4db 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -21,8 +21,8 @@ use mcrl2::SrfPbes; use mcrl2::StategraphEquation; use mcrl2::replace_propositional_variables; use mcrl2::replace_variables; -use merc_io::TimeProgress; use merc_io::LargeFormatter; +use merc_io::TimeProgress; use merc_utilities::MercError; use crate::clone_iterator::CloneIterator; @@ -36,13 +36,13 @@ pub struct SymmetryAlgorithm { state_graph: PbesStategraph, /// The parameters of the unified SRF PBES. - parameters: Vec, + parameters: Vec, /// The indices of all control flow parameters in the PBES. all_control_flow_parameters: Vec, /// The SRF PBES after unifying parameters. - srf: SrfPbes, + srf: SrfPbes, /// Keep track of some progress messages. num_of_checked_candidates: Cell, @@ -74,10 +74,7 @@ impl SymmetryAlgorithm { Vec::new() }; - info!( - "Unified parameters: {}", - parameters.iter().format(", ") - ); + info!("Unified parameters: {}", parameters.iter().format(", ")); let state_graph = PbesStategraph::run(&srf.to_pbes())?; let all_control_flow_parameters = state_graph @@ -104,7 +101,9 @@ impl SymmetryAlgorithm { } /// Returns compliant permutations. - pub fn candidates(&self, partition_data_sorts: bool) -> impl Iterator + '_ { + /// + /// See [clique_candidates] for the parameters. + pub fn candidates(&self, partition_data_sorts: bool, partition_data_updates: bool) -> impl Iterator + '_ { let cliques = self.cliques(); for clique in &cliques { @@ -122,7 +121,7 @@ impl SymmetryAlgorithm { let mut number_of_candidates = 1usize; for clique in &cliques { - let (number_of_permutations, candidates) = self.clique_candidates(clique.clone(), partition_data_sorts); + let (number_of_permutations, candidates) = self.clique_candidates(clique.clone(), partition_data_sorts, partition_data_updates); info!( "Maximum number of permutations for clique {:?}: {}", clique, @@ -156,7 +155,9 @@ impl SymmetryAlgorithm { // Check that all control flow parameters are mapped to control flow parameters. for index in pi.domain() { let mapped_index = pi.value(index); - if self.all_control_flow_parameters.contains(&index) != self.all_control_flow_parameters.contains(&mapped_index) { + if self.all_control_flow_parameters.contains(&index) + != self.all_control_flow_parameters.contains(&mapped_index) + { return Err(format!( "A parameter at index {} is mapped to parameter at index {}, but they are not both control flow parameters.", index, mapped_index @@ -166,8 +167,11 @@ impl SymmetryAlgorithm { if index >= self.parameters.len() || mapped_index >= self.parameters.len() { return Err(format!( "A parameter at index {} is mapped to parameter at index {}, but the PBES only has {} parameters.", - index, mapped_index, self.parameters.len() - ).into()); + index, + mapped_index, + self.parameters.len() + ) + .into()); } } @@ -242,6 +246,7 @@ impl SymmetryAlgorithm { &self, I: Vec, partition_data_sorts: bool, + partition_data_updates: bool, ) -> (usize, Box + '_>) { // Determine the parameter indices involved in the clique let control_flow_parameter_indices: Vec = I @@ -256,14 +261,17 @@ impl SymmetryAlgorithm { // Groups the data parameters by their sort. let (mut number_of_permutations, all_data_groups) = if partition_data_sorts { - let same_sort_parameters = partition(self.parameters.iter().enumerate().filter_map(|(index, param)| { - if self.all_control_flow_parameters.contains(&index) { - // Skip control flow parameters. - None - } else { - Some(param) - } - }), |lhs, rhs| lhs.sort() == rhs.sort()); + let same_sort_parameters = partition( + self.parameters.iter().enumerate().filter_map(|(index, param)| { + if self.all_control_flow_parameters.contains(&index) { + // Skip control flow parameters. + None + } else { + Some(param) + } + }), + |lhs, rhs| lhs.sort() == rhs.sort(), + ); let mut number_of_permutations = 1usize; let mut all_data_groups: Box> = Box::new(iter::empty()); // Default value is overwritten in first iteration. @@ -282,8 +290,8 @@ impl SymmetryAlgorithm { // Compute the product of the current data group with the already concatenated ones. let number_of_parametes = parameter_indices.len(); if number_of_permutations == 1 { - all_data_groups = Box::new(permutation_group(parameter_indices)) - as Box>; + all_data_groups = + Box::new(permutation_group(parameter_indices)) as Box>; } else { all_data_groups = Box::new( all_data_groups @@ -630,11 +638,10 @@ where I: Iterator, P: Fn(&T, &T) -> bool, T: Clone, -{ +{ let mut result: Vec> = Vec::new(); for element in elements { - if let Some(group) = result.iter_mut().find(|g: &&mut Vec<_>| { if let Some(first) = g.first() { predicate(first, &element) @@ -726,18 +733,25 @@ mod tests { let _ = test_logger(); let pbes = Pbes::from_text(include_str!("../../../../examples/pbes/c.text.pbes")).unwrap(); - let algorithm = SymmetryAlgorithm::new(&pbes, false).unwrap(); let cliques = algorithm.cliques(); - assert_eq!(cliques.len(), 1, "There should be exactly one clique in example c.text.pbes."); + assert_eq!( + cliques.len(), + 1, + "There should be exactly one clique in example c.text.pbes." + ); let mut symmetries: Vec = algorithm .candidates(false) .filter(|pi| algorithm.check_symmetry(pi)) .collect(); - assert_eq!(symmetries.len(), 2, "There should be exactly two symmetries in example c.text.pbes."); + assert_eq!( + symmetries.len(), + 2, + "There should be exactly two symmetries in example c.text.pbes." + ); // Sort symmetries for consistent comparison symmetries.sort_by_key(|pi| pi.to_string()); @@ -750,9 +764,9 @@ mod tests { // Check that we have the (1 3)(2 4) permutation assert!( - symmetries.iter().any(|pi| { - pi.value(0) == 2 && pi.value(2) == 0 && pi.value(1) == 3 && pi.value(3) == 1 - }), + symmetries + .iter() + .any(|pi| { pi.value(0) == 2 && pi.value(2) == 0 && pi.value(1) == 3 && pi.value(3) == 1 }), "Expected to find the (0 2)(1 3) permutation" ); } From 01a348609a18010c2aacdf49144e8355f822437e Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 6 Jan 2026 22:53:55 +0100 Subject: [PATCH 13/40] Added ATermListRef --- .../crates/mcrl2/src/atermpp/aterm_list.rs | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs index ee8d2e91..808209f9 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs @@ -151,3 +151,20 @@ mod tests { assert_eq!(values[3], ATerm::from_string("i").unwrap()); } } + +// TODO: This should be generated by a macro + +pub struct ATermListRef<'a, T> { + term: ATermRef<'a>, + _marker: PhantomData, +} + +impl<'a, T> From> for ATermListRef<'a, T> { + fn from(value: ATermRef<'a>) -> Self { + debug_assert!(value.is_list(), "Term is not a list: {:?}", value); + ATermListRef { + term: value, + _marker: PhantomData, + } + } +} \ No newline at end of file From f4c89c75efdbf3cb5326d2938dad18659f7d1ed9 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 6 Jan 2026 22:54:09 +0100 Subject: [PATCH 14/40] Added better Debug for terms --- .../mcrl2-macros/src/mcrl2_derive_terms.rs | 17 +++++++++++++++-- .../crates/mcrl2/src/atermpp/aterm_string.rs | 7 +++++++ 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2-macros/src/mcrl2_derive_terms.rs b/tools/mcrl2/crates/mcrl2-macros/src/mcrl2_derive_terms.rs index d9f7defa..79e9b54d 100644 --- a/tools/mcrl2/crates/mcrl2-macros/src/mcrl2_derive_terms.rs +++ b/tools/mcrl2/crates/mcrl2-macros/src/mcrl2_derive_terms.rs @@ -36,7 +36,7 @@ pub(crate) fn mcrl2_derive_terms_impl(_attributes: TokenStream, input: TokenStre // Add the expected derive macros to the input struct. object .attrs - .push(parse_quote!(#[derive(Clone, Default, Debug, Hash, PartialEq, Eq, PartialOrd, Ord)])); + .push(parse_quote!(#[derive(Clone, Default, Hash, PartialEq, Eq, PartialOrd, Ord)])); // ALL structs in this module must contain the term. assert!( @@ -121,7 +121,13 @@ pub(crate) fn mcrl2_derive_terms_impl(_attributes: TokenStream, input: TokenStre } } - #[derive(Default, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] + impl ::std::fmt::Debug for #name { + fn fmt(&self, f: &mut ::std::fmt::Formatter<'_>) -> ::std::fmt::Result { + write!(f, "{:?}", self.term) + } + } + + #[derive(Default, Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct #name_ref<'a> { pub(crate) term: ATermRef<'a> } @@ -185,6 +191,13 @@ pub(crate) fn mcrl2_derive_terms_impl(_attributes: TokenStream, input: TokenStre 1 } } + + impl ::std::fmt::Debug for #name_ref<'_> { + fn fmt(&self, f: &mut ::std::fmt::Formatter<'_>) -> ::std::fmt::Result { + write!(f, "{:?}", self.term) + } + } + ); added.push(Item::Verbatim(generated)); diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs index b62d3b63..889b7629 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs @@ -40,3 +40,10 @@ impl fmt::Display for ATermString { write!(f, "{}", self.str()) } } + +impl fmt::Display for ATermStringRef<'_> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.str()) + } +} + From 731fb279c886e75196a98f2551b548510b75e625 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 7 Jan 2026 21:46:40 +0100 Subject: [PATCH 15/40] Only search the first symmetry, annd instead made finding all symmetries an option --- tools/mcrl2/pbes/src/main.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index 76dbfec7..829701ec 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -62,6 +62,10 @@ struct SymmetryArgs { #[arg(long)] permutation: Option, + /// Search for all symmetries instead of only the first one. + #[arg(long, default_value_t = false)] + all_symmetries: bool, + /// Partition data parameters into their sorts before considering their permutation groups. #[arg(long, default_value_t = false)] partition_data_sorts: bool, @@ -122,6 +126,11 @@ fn main() -> Result { if algorithm.check_symmetry(&candidate) { info!("Found symmetry: {}", candidate); + + if !args.all_symmetries { + // Only search for the first symmetry + return Ok(ExitCode::SUCCESS); + } } } } From e5fc2d3ab7ac681e77436f672fcc1791196399e6 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 7 Jan 2026 21:48:13 +0100 Subject: [PATCH 16/40] Added random tests for the cycle notation parsing --- tools/mcrl2/Cargo.lock | 2 ++ tools/mcrl2/crates/mcrl2/Cargo.toml | 1 + tools/mcrl2/pbes/Cargo.toml | 1 + tools/mcrl2/pbes/src/permutation.rs | 18 ++++++++++++++++++ 4 files changed, 22 insertions(+) diff --git a/tools/mcrl2/Cargo.lock b/tools/mcrl2/Cargo.lock index f0b53b6b..edee86c0 100644 --- a/tools/mcrl2/Cargo.lock +++ b/tools/mcrl2/Cargo.lock @@ -508,6 +508,7 @@ checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" name = "mcrl2" version = "1.0.0" dependencies = [ + "itertools", "log", "mcrl2-macros", "mcrl2-sys", @@ -557,6 +558,7 @@ dependencies = [ "merc_io", "merc_tools", "merc_utilities", + "rand", "thiserror", ] diff --git a/tools/mcrl2/crates/mcrl2/Cargo.toml b/tools/mcrl2/crates/mcrl2/Cargo.toml index 4346681f..3b38a497 100644 --- a/tools/mcrl2/crates/mcrl2/Cargo.toml +++ b/tools/mcrl2/crates/mcrl2/Cargo.toml @@ -12,6 +12,7 @@ mcrl2-sys.workspace = true merc_tools.workspace = true merc_utilities.workspace = true +itertools.workspace = true log.workspace = true parking_lot.workspace = true rand.workspace = true diff --git a/tools/mcrl2/pbes/Cargo.toml b/tools/mcrl2/pbes/Cargo.toml index 8b71079a..836d427d 100644 --- a/tools/mcrl2/pbes/Cargo.toml +++ b/tools/mcrl2/pbes/Cargo.toml @@ -15,6 +15,7 @@ clap.workspace = true env_logger.workspace = true itertools.workspace = true log.workspace = true +rand.workspace = true thiserror.workspace = true [features] diff --git a/tools/mcrl2/pbes/src/permutation.rs b/tools/mcrl2/pbes/src/permutation.rs index 25af8301..4e9f7dab 100644 --- a/tools/mcrl2/pbes/src/permutation.rs +++ b/tools/mcrl2/pbes/src/permutation.rs @@ -257,6 +257,9 @@ pub fn permutation_group_size(n: usize) -> usize { #[cfg(test)] mod tests { + use merc_utilities::random_test; + use rand::Rng; + use super::*; #[test] @@ -292,4 +295,19 @@ mod tests { assert_eq!(permutations.len(), permutation_group_size(indices.len())); } + + #[test] + fn test_random_cycle_notation() { + random_test(100, |rng| { + let mapping: Vec<(usize, usize)> = (0..rng.random_range(1..10)) + .map(|i| (i, rng.random_range(0..10))) + .collect(); + let permutation = Permutation::from_mapping(mapping.clone()); + + let cycle_notation = permutation.to_string(); + let parsed_permutation = Permutation::from_cycle_notation(&cycle_notation).unwrap(); + + assert_eq!(permutation, parsed_permutation, "Failed on permutation {:?}", permutation); + }) + } } From 50b8456fc4a20751f30f782d82c44b6cd48b40d7 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 7 Jan 2026 21:48:48 +0100 Subject: [PATCH 17/40] Added ATermInt for the mcrl2 aterm_int --- .../crates/mcrl2/src/atermpp/aterm_int.rs | 49 +++++++++++++++++++ tools/mcrl2/crates/mcrl2/src/atermpp/mod.rs | 6 ++- 2 files changed, 53 insertions(+), 2 deletions(-) create mode 100644 tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs new file mode 100644 index 00000000..7d611123 --- /dev/null +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs @@ -0,0 +1,49 @@ +use std::fmt; + +use mcrl2_macros::mcrl2_derive_terms; + +use crate::ATermRef; + +pub fn is_aterm_int(term: &ATermRef<'_>) -> bool { + false +} + +#[mcrl2_derive_terms] +mod inner { + use mcrl2_macros::mcrl2_term; + + use crate::ATerm; + use crate::ATermRef; + use crate::Markable; + use crate::Todo; + use crate::is_aterm_int; + + /// Represents an atermpp::aterm_string from the mCRL2 toolset. + #[mcrl2_term(is_aterm_int)] + pub struct ATermInt { + term: ATerm, + } + + impl ATermInt { + /// Returns the string value. + pub fn value(&self) -> u64 { + // The Rust::Str should ensure that this is a valid string. + 0 + } + } +} + +pub use inner::*; + +impl fmt::Display for ATermInt { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.value()) + } +} + +impl fmt::Display for ATermIntRef<'_> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.value()) + } +} + diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/mod.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/mod.rs index 5195cc10..f016a012 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/mod.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/mod.rs @@ -1,6 +1,7 @@ -mod aterm; +mod aterm_int; mod aterm_list; mod aterm_string; +mod aterm; mod busy_forbidden; mod global_aterm_pool; mod markable; @@ -8,9 +9,10 @@ mod random_term; mod symbol; mod thread_aterm_pool; -pub use aterm::*; +pub use aterm_int::*; pub use aterm_list::*; pub use aterm_string::*; +pub use aterm::*; pub use busy_forbidden::*; pub use markable::*; pub use random_term::*; From 7d1f281fad7658ced66af29cb02297d711f4ebfa Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Thu, 8 Jan 2026 15:58:37 +0100 Subject: [PATCH 18/40] Extended the visitors. --- tools/mcrl2/crates/mcrl2/src/visitor.rs | 89 +++++++++++++------------ 1 file changed, 47 insertions(+), 42 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2/src/visitor.rs b/tools/mcrl2/crates/mcrl2/src/visitor.rs index bd71254d..92ce5067 100644 --- a/tools/mcrl2/crates/mcrl2/src/visitor.rs +++ b/tools/mcrl2/crates/mcrl2/src/visitor.rs @@ -33,37 +33,43 @@ use crate::is_variable; use crate::is_where_clause; pub trait DataExpressionVisitor { - fn visit_variable(&mut self, var: &DataVariableRef<'_>) -> Option { + fn visit_variable(&mut self, _var: &DataVariableRef<'_>) -> Option { None } - fn visit_application(&mut self, appl: &DataApplicationRef<'_>) -> Option) -> Option { + let _head = self.visit(&appl.data_function_symbol().into()); - DataExpression::from(appl.protect()) + appl.data_arguments().for_each(|arg| { + self.visit(&arg.into()); + }); + + None } - fn visit_abstraction(&mut self, abstraction: &DataAbstractionRef<'_>) -> DataExpression { - DataExpression::from(abstraction.protect()) + fn visit_abstraction(&mut self, abstraction: &DataAbstractionRef<'_>) -> Option { + let _body = self.visit(&abstraction.body()); + None } - fn visit_function_symbol(&mut self, function_symbol: &DataFunctionSymbolRef<'_>) -> DataExpression { - DataExpression::from(function_symbol.protect()) + fn visit_function_symbol(&mut self, _function_symbol: &DataFunctionSymbolRef<'_>) -> Option { + None } - fn visit_where_clause(&mut self, where_: &DataWhereClauseRef<'_>) -> DataExpression { - DataExpression::from(where_.protect()) + fn visit_where_clause(&mut self, where_: &DataWhereClauseRef<'_>) -> Option { + let _body = self.visit(&where_.body()); + None } - fn visit_machine_number(&mut self, number: &DataMachineNumberRef<'_>) -> DataExpression { - DataExpression::from(number.protect()) + fn visit_machine_number(&mut self, _number: &DataMachineNumberRef<'_>) -> Option { + None } - fn visit_untyped_identifier(&mut self, identifier: &DataUntypedIdentifierRef<'_>) -> DataExpression { - DataExpression::from(identifier.protect()) + fn visit_untyped_identifier(&mut self, _identifier: &DataUntypedIdentifierRef<'_>) -> Option { + None } - fn visit(&mut self, expr: &DataExpressionRef<'_>) -> DataExpression { + fn visit(&mut self, expr: &DataExpressionRef<'_>) -> Option { if is_variable(&expr.copy()) { self.visit_variable(&DataVariableRef::from(expr.copy())) } else if is_application(&expr.copy()) { @@ -87,48 +93,48 @@ pub trait DataExpressionVisitor { pub trait PbesExpressionVisitor { fn visit_propositional_variable_instantiation( &mut self, - inst: &PbesPropositionalVariableInstantiationRef<'_>, - ) -> PbesExpression { - PbesExpression::from(inst.protect()) + _inst: &PbesPropositionalVariableInstantiationRef<'_>, + ) -> Option { + None } - fn visit_not(&mut self, not: &PbesNotRef<'_>) -> PbesExpression { + fn visit_not(&mut self, not: &PbesNotRef<'_>) -> Option { self.visit(¬.body()); - PbesExpression::from(not.protect()) + None } - fn visit_and(&mut self, and: &PbesAndRef<'_>) -> PbesExpression { + fn visit_and(&mut self, and: &PbesAndRef<'_>) -> Option { self.visit(&and.lhs()); self.visit(&and.rhs()); - PbesExpression::from(and.protect()) + None } - fn visit_or(&mut self, or: &PbesOrRef<'_>) -> PbesExpression { + fn visit_or(&mut self, or: &PbesOrRef<'_>) -> Option { self.visit(&or.lhs()); self.visit(&or.rhs()); - PbesExpression::from(or.protect()) + None } - fn visit_imp(&mut self, imp: &PbesImpRef<'_>) -> PbesExpression { + fn visit_imp(&mut self, imp: &PbesImpRef<'_>) -> Option { self.visit(&imp.lhs()); self.visit(&imp.rhs()); - PbesExpression::from(imp.protect()) + None } - fn visit_forall(&mut self, forall: &PbesForallRef<'_>) -> PbesExpression { + fn visit_forall(&mut self, forall: &PbesForallRef<'_>) -> Option { self.visit(&forall.body()); - PbesExpression::from(forall.protect()) + None } - fn visit_exists(&mut self, exists: &PbesExistsRef<'_>) -> PbesExpression { + fn visit_exists(&mut self, exists: &PbesExistsRef<'_>) -> Option { self.visit(&exists.body()); - PbesExpression::from(exists.protect()) + None } - fn visit(&mut self, expr: &PbesExpressionRef<'_>) -> PbesExpression { + fn visit(&mut self, expr: &PbesExpressionRef<'_>) -> Option { if is_pbes_propositional_variable_instantiation(&expr.copy()) { self.visit_propositional_variable_instantiation(&PbesPropositionalVariableInstantiationRef::from( - expr.copy(), + expr.copy() )) } else if is_pbes_not(&expr.copy()) { self.visit_not(&PbesNotRef::from(expr.copy())) @@ -162,13 +168,13 @@ where where F: Fn(&DataVariableRef<'_>) -> DataExpression, { - fn visit_variable(&mut self, var: &DataVariableRef<'_>) -> DataExpression { - (*self.apply)(var) + fn visit_variable(&mut self, var: &DataVariableRef<'_>) -> Option { + Some((*self.apply)(var)) } } let mut builder = ReplaceVariableBuilder { apply: f }; - builder.visit(expr) + builder.visit(expr).expect("Replacement should return a value") } /// Returns all the PVIs occurring in the given PBES expression. @@ -183,17 +189,16 @@ pub fn pbes_expression_pvi(expr: &PbesExpressionRef<'_>) -> Vec, - ) -> PbesExpression { + ) -> Option { // Found a propositional variable instantiation, return true. - self.result.push(PbesPropositionalVariableInstantiation::from(inst.protect())); - PbesExpression::from(inst.protect()) + self.result + .push(PbesPropositionalVariableInstantiation::from(inst.protect())); + None } } - let mut checker = PviChecker { - result: &mut result, - }; + let mut checker = PviChecker { result: &mut result }; checker.visit(expr); result -} \ No newline at end of file +} From 6f72972ec2b178c3b2da8c276cda524a98fbb964 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Thu, 8 Jan 2026 15:59:07 +0100 Subject: [PATCH 19/40] Fixed issue in data expression --- .../mcrl2/crates/mcrl2/src/data_expression.rs | 23 +++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2/src/data_expression.rs b/tools/mcrl2/crates/mcrl2/src/data_expression.rs index 29ace48d..83b93959 100644 --- a/tools/mcrl2/crates/mcrl2/src/data_expression.rs +++ b/tools/mcrl2/crates/mcrl2/src/data_expression.rs @@ -77,6 +77,7 @@ mod inner { use crate::ATerm; use crate::ATermArgs; + use crate::ATermIntRef; use crate::ATermRef; use crate::ATermString; use crate::ATermStringRef; @@ -133,11 +134,11 @@ mod inner { /// Returns the arguments of a data expression /// - function symbol f -> [] /// - application f(t_0, ..., t_n) -> [t_0, ..., t_n] - pub fn data_sort(&self) -> SortExpressionRef<'_> { + pub fn data_sort(&self) -> SortExpression { if is_function_symbol(&self.term) { - self.data + DataFunctionSymbolRef::from(self.term.copy()).sort().protect() } else if is_variable(&self.term) { - DataVariableRef::from(self.term.copy()).sort() + DataVariableRef::from(self.term.copy()).sort().protect() } else { panic!("data_sort not implemented for {}", self); } @@ -246,6 +247,13 @@ mod inner { term: ATerm, } + impl DataAbstraction { + /// Returns the body of the abstraction. + pub fn body(&self) -> DataExpressionRef<'_> { + self.term.arg(1).into() + } + } + /// Represents a data::function_symbol from the mCRL2 toolset. #[mcrl2_term(is_function_symbol)] pub struct DataFunctionSymbol { @@ -304,7 +312,7 @@ mod inner { impl DataMachineNumber { /// Obtain the underlying value of a machine number. pub fn value(&self) -> u64 { - 0 + ATermIntRef::from(self.term.copy()).value() } } @@ -320,6 +328,13 @@ mod inner { pub term: ATerm, } + impl DataWhereClause { + /// Returns the body of the where clause. + pub fn body(&self) -> DataExpressionRef<'_> { + self.term.arg(0).into() + } + } + /// Represents a data::untyped_identifier from the mCRL2 toolset. #[mcrl2_term(is_untyped_identifier)] pub struct DataUntypedIdentifier { From a071a31b6d9ca7b9e10ee13d7c0ae967d7090b7b Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Thu, 8 Jan 2026 19:32:46 +0100 Subject: [PATCH 20/40] Fixed the example tests --- tools/mcrl2/pbes/src/symmetry.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index fa2ca4db..746cc71e 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -743,7 +743,7 @@ mod tests { ); let mut symmetries: Vec = algorithm - .candidates(false) + .candidates(false, false) .filter(|pi| algorithm.check_symmetry(pi)) .collect(); From 108e97aca8ffc24eeab99b28f86832e4c2683775 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 9 Jan 2026 12:45:38 +0100 Subject: [PATCH 21/40] Ignore the identity symmetry --- tools/mcrl2/pbes/src/main.rs | 2 +- tools/mcrl2/pbes/src/permutation.rs | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index 829701ec..ff38f3ec 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -127,7 +127,7 @@ fn main() -> Result { if algorithm.check_symmetry(&candidate) { info!("Found symmetry: {}", candidate); - if !args.all_symmetries { + if !args.all_symmetries && !candidate.is_identity() { // Only search for the first symmetry return Ok(ExitCode::SUCCESS); } diff --git a/tools/mcrl2/pbes/src/permutation.rs b/tools/mcrl2/pbes/src/permutation.rs index 4e9f7dab..01b2afb0 100644 --- a/tools/mcrl2/pbes/src/permutation.rs +++ b/tools/mcrl2/pbes/src/permutation.rs @@ -159,7 +159,6 @@ impl Permutation { } /// Check whether this permutation is the identity permutation. - #[cfg(test)] pub fn is_identity(&self) -> bool { self.mapping.iter().all(|(d, v)| d == v) } From 633eaf9fc9aff1bce8b92dc4f98123f52b8a8e89 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 9 Jan 2026 12:46:12 +0100 Subject: [PATCH 22/40] Ignore test until it is fixed --- tools/mcrl2/pbes/src/permutation.rs | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/tools/mcrl2/pbes/src/permutation.rs b/tools/mcrl2/pbes/src/permutation.rs index 01b2afb0..142caf20 100644 --- a/tools/mcrl2/pbes/src/permutation.rs +++ b/tools/mcrl2/pbes/src/permutation.rs @@ -295,18 +295,18 @@ mod tests { assert_eq!(permutations.len(), permutation_group_size(indices.len())); } - #[test] - fn test_random_cycle_notation() { - random_test(100, |rng| { - let mapping: Vec<(usize, usize)> = (0..rng.random_range(1..10)) - .map(|i| (i, rng.random_range(0..10))) - .collect(); - let permutation = Permutation::from_mapping(mapping.clone()); - - let cycle_notation = permutation.to_string(); - let parsed_permutation = Permutation::from_cycle_notation(&cycle_notation).unwrap(); - - assert_eq!(permutation, parsed_permutation, "Failed on permutation {:?}", permutation); - }) - } + // #[test] + // fn test_random_cycle_notation() { + // random_test(100, |rng| { + // let mapping: Vec<(usize, usize)> = (0..rng.random_range(1..10)) + // .map(|i| (i, rng.random_range(0..10))) + // .collect(); + // let permutation = Permutation::from_mapping(mapping.clone()); + + // let cycle_notation = permutation.to_string(); + // let parsed_permutation = Permutation::from_cycle_notation(&cycle_notation).unwrap(); + + // assert_eq!(permutation, parsed_permutation, "Failed on permutation {:?}", permutation); + // }) + // } } From 8028cae9dd465d8be7bd8d6a3a303467cfc7ccad Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 9 Jan 2026 12:57:54 +0100 Subject: [PATCH 23/40] Print a message when it was aborted --- tools/mcrl2/pbes/src/main.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index ff38f3ec..3ecfcb93 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -129,7 +129,8 @@ fn main() -> Result { if !args.all_symmetries && !candidate.is_identity() { // Only search for the first symmetry - return Ok(ExitCode::SUCCESS); + info!("Stopping search after first non-trivial symmetry."); + break; } } } From b5598b7107f60e6d08e6a75314e0827231874ba3 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 12 Jan 2026 12:12:05 +0100 Subject: [PATCH 24/40] Deal with the undefined vertex in cfgs. --- tools/mcrl2/pbes/src/symmetry.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 746cc71e..d2590cb8 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -657,11 +657,15 @@ where result } +/// A constant representing an undefined index. +const UNDEFINED_INDEX: usize = usize::MAX; + /// Returns the index of the variable that the control flow graph considers fn variable_index(cfg: &ControlFlowGraph) -> usize { // Check that all the vertices have the same variable assigned for consistency cfg.vertices().iter().for_each(|v| { - if v.index() + if v.index() != UNDEFINED_INDEX // Ignore undefined indices + && v.index() != cfg .vertices() .first() @@ -672,8 +676,8 @@ fn variable_index(cfg: &ControlFlowGraph) -> usize { } }); - if let Some(v) = cfg.vertices().iter().next() { - // Simply return the index of the variable + if let Some(v) = cfg.vertices().iter().find(|v| v.index() != UNDEFINED_INDEX) { + // Simply return the index of the first vertex that is defined. return v.index(); } From 9f911624178917b85d2f0422c4575456bb0b2563 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 9 Jan 2026 21:49:43 +0100 Subject: [PATCH 25/40] Fixed the random cycle notation test, and added one for mappings as well --- tools/mcrl2/pbes/src/permutation.rs | 109 +++++++++++++++++++++------- 1 file changed, 83 insertions(+), 26 deletions(-) diff --git a/tools/mcrl2/pbes/src/permutation.rs b/tools/mcrl2/pbes/src/permutation.rs index 142caf20..14abf518 100644 --- a/tools/mcrl2/pbes/src/permutation.rs +++ b/tools/mcrl2/pbes/src/permutation.rs @@ -17,21 +17,18 @@ impl Permutation { /// sorts the mapping by domain for a unique representation. The input must be /// a valid permutation (so a bijection). pub fn from_mapping(mut mapping: Vec<(usize, usize)>) -> Self { - // Validate lengths and uniqueness in debug builds. - if cfg!(debug_assertions) { - let mut seen_domain = HashSet::new(); - for (d, _) in &mapping { - debug_assert!( - seen_domain.insert(*d), - "Invalid permutation mapping: multiple mappings for {}", - d - ); - } - } + debug_assert!( + is_valid_permutation(&mapping), + "Input mapping is not a valid permutation: {:?}", + mapping + ); // Sort by domain for deterministic representation. mapping.sort_unstable_by_key(|(d, _)| *d); - // debug_assert!(mapping.iter().all(|(from, to)| from != to), "Mapping should not contain identity mappings."); + debug_assert!( + mapping.iter().all(|(from, to)| from != to), + "Mapping should not contain identity mappings." + ); debug_assert!( mapping.iter().duplicates().count() == 0, "Mapping should not contain duplicate domain entries." @@ -83,6 +80,10 @@ impl Permutation { pairs.push((from, to)); } + if !is_valid_permutation(&pairs) { + return Err(MercError::from("Input mapping is not a valid permutation.")); + } + Ok(Permutation::from_mapping(pairs)) } @@ -124,6 +125,10 @@ impl Permutation { } } + if !is_valid_permutation(&mapping) { + return Err(MercError::from("Input mapping is not a valid permutation.")); + } + Ok(Permutation::from_mapping(mapping)) } @@ -164,6 +169,22 @@ impl Permutation { } } +/// Checks whether the mapping represents a valid permutation +#[cfg(debug_assertions)] +pub fn is_valid_permutation(mapping: &Vec<(usize, usize)>) -> bool { + let mut domain = HashSet::with_capacity(mapping.len()); + let mut image = HashSet::with_capacity(mapping.len()); + + for (d, v) in mapping { + if !domain.insert(*d) || !image.insert(*v) { + // Duplicate found in domain or image + return false; + } + } + + domain == image +} + /// Display the permutation in cycle notation. /// /// Cycle notation is a standard way to present permutations, where each cycle @@ -173,9 +194,9 @@ impl Permutation { impl fmt::Display for Permutation { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { // Determine the maximum value in the permutation mapping. - let max_value = self.mapping.iter().map(|(d, _)| *d + 1).max().unwrap_or(0); + let max_value = self.mapping.iter().map(|(d, e)| *d.max(e)).max().unwrap_or(0); - let mut visited = vec![false; max_value]; + let mut visited = vec![false; max_value + 1]; let mut identity = true; // The mapping is sorted by domain, so we can iterate over it directly. @@ -258,6 +279,7 @@ pub fn permutation_group_size(n: usize) -> usize { mod tests { use merc_utilities::random_test; use rand::Rng; + use rand::seq::{IteratorRandom, SliceRandom}; use super::*; @@ -295,18 +317,53 @@ mod tests { assert_eq!(permutations.len(), permutation_group_size(indices.len())); } - // #[test] - // fn test_random_cycle_notation() { - // random_test(100, |rng| { - // let mapping: Vec<(usize, usize)> = (0..rng.random_range(1..10)) - // .map(|i| (i, rng.random_range(0..10))) - // .collect(); - // let permutation = Permutation::from_mapping(mapping.clone()); + #[test] + fn test_random_cycle_notation() { + random_test(100, |rng| { + // Pick a random subset size >= 2 to allow a derangement. + let m = rng.random_range(2..10); + + // Choose a random subset of distinct domain elements. + let domain: Vec = (0..10).choose_multiple(rng, m); + + // Create a random derangement of the chosen domain. + let mut image = domain.clone(); + image.shuffle(rng); + + let mapping: Vec<(usize, usize)> = domain.into_iter().zip(image).filter(|(x, y)| x != y).collect(); + println!("Mapping: {:?}", mapping); - // let cycle_notation = permutation.to_string(); - // let parsed_permutation = Permutation::from_cycle_notation(&cycle_notation).unwrap(); + let permutation = Permutation::from_mapping(mapping.clone()); - // assert_eq!(permutation, parsed_permutation, "Failed on permutation {:?}", permutation); - // }) - // } + let cycle_notation = permutation.to_string(); + let parsed_permutation = Permutation::from_cycle_notation(&cycle_notation).unwrap(); + + assert_eq!(permutation, parsed_permutation, "Failed on permutation {:?}", permutation); + }) + } + + #[test] + fn test_random_mapping_notation() { + random_test(100, |rng| { + // Pick a random subset size >= 2 to allow a derangement. + let m = rng.random_range(2..10); + + // Choose a random subset of distinct domain elements. + let domain: Vec = (0..10).choose_multiple(rng, m); + + // Create a random derangement of the chosen domain. + let mut image = domain.clone(); + image.shuffle(rng); + + let mapping: Vec<(usize, usize)> = domain.into_iter().zip(image).filter(|(x, y)| x != y).collect(); + println!("Mapping: {:?}", mapping); + + let permutation = Permutation::from_mapping(mapping.clone()); + + let mapping_notation = format!("{:?}", permutation); + let parsed_permutation = Permutation::from_mapping_notation(&mapping_notation).unwrap(); + + assert_eq!(permutation, parsed_permutation, "Failed on permutation {:?}", permutation); + }) + } } From 3484e43c773ba61196cfb8f883454d94a3c4e275 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 12 Jan 2026 10:11:02 +0100 Subject: [PATCH 26/40] Started with ATermListRef --- .../crates/mcrl2/src/atermpp/aterm_int.rs | 3 +- .../crates/mcrl2/src/atermpp/aterm_list.rs | 54 ++++++++++++++++--- 2 files changed, 48 insertions(+), 9 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs index 7d611123..69e524b3 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs @@ -1,11 +1,12 @@ use std::fmt; use mcrl2_macros::mcrl2_derive_terms; +use mcrl2_sys::atermpp::ffi::mcrl2_aterm_is_int; use crate::ATermRef; pub fn is_aterm_int(term: &ATermRef<'_>) -> bool { - false + mcrl2_aterm_is_int(term.get()) } #[mcrl2_derive_terms] diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs index 808209f9..83339b58 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs @@ -1,5 +1,8 @@ +use std::fmt; use std::marker::PhantomData; +use itertools::Itertools; + use crate::ATerm; use crate::ATermRef; @@ -39,7 +42,7 @@ impl ATermList { /// Obtain the tail, i.e. the remainder, of the list. Will panic if the list /// is empty. pub fn tail(&self) -> ATermList { - self.term.arg(1).into() + self.term.arg(1).protect().into() } /// Returns the tail if it exists, or None if the list is empty. @@ -100,12 +103,6 @@ impl From for ATermList { } } -impl<'a, T> From> for ATermList { - fn from(value: ATermRef<'a>) -> Self { - Self::new(value.protect()) - } -} - impl> IntoIterator for ATermList { type IntoIter = ATermListIter; type Item = T; @@ -124,6 +121,12 @@ impl> IntoIterator for &ATermList { } } +impl + fmt::Debug> fmt::Debug for ATermList { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "[{:?}]", self.iter().format(", ")) + } +} + pub struct ATermListIter { current: ATermList, } @@ -159,6 +162,23 @@ pub struct ATermListRef<'a, T> { _marker: PhantomData, } +impl ATermListRef<'_, T> { + /// Returns true iff the list is empty. + pub fn is_empty(&self) -> bool { + self.term.is_empty_list() + } +} + +impl<'a, T: From> ATermListRef<'a, T> { + pub fn head(&self) -> T { + self.term.arg(0).protect().into() + } + + pub fn tail(&'a self) -> ATermListRef<'a, T> { + self.term.arg(1).into() + } +} + impl<'a, T> From> for ATermListRef<'a, T> { fn from(value: ATermRef<'a>) -> Self { debug_assert!(value.is_list(), "Term is not a list: {:?}", value); @@ -167,4 +187,22 @@ impl<'a, T> From> for ATermListRef<'a, T> { _marker: PhantomData, } } -} \ No newline at end of file +} + +pub struct ATermListIterRef<'a, T> { + current: ATermListRef<'a, T>, +} + +// impl<'a, T: From> Iterator for ATermListIterRef<'a, T> { +// type Item = T; + +// fn next(&mut self) -> Option { +// if self.current.is_empty() { +// None +// } else { +// let head = self.current.head(); +// self.current = self.current.tail(); +// Some(head) +// } +// } +// } From 3130b7b955d7bc3640bea68aec3ea5031fd6743d Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 12 Jan 2026 14:44:47 +0100 Subject: [PATCH 27/40] Added a replace_variables for data expressions. --- tools/mcrl2/crates/mcrl2-sys/build.rs | 2 + tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp | 28 ++++++ tools/mcrl2/crates/mcrl2-sys/cpp/data.h | 7 ++ tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h | 1 + tools/mcrl2/pbes/src/symmetry.rs | 116 ++++++++++++++-------- 5 files changed, 115 insertions(+), 39 deletions(-) create mode 100644 tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp diff --git a/tools/mcrl2/crates/mcrl2-sys/build.rs b/tools/mcrl2/crates/mcrl2-sys/build.rs index 29d6e982..a5a8865c 100644 --- a/tools/mcrl2/crates/mcrl2-sys/build.rs +++ b/tools/mcrl2/crates/mcrl2-sys/build.rs @@ -174,6 +174,7 @@ fn main() { &utilities_source_files, )) .file("cpp/pbes.cpp") + .file("cpp/data.cpp") .file(mcrl2_workarounds_path.clone() + "mcrl2_syntax.c"); // This is to avoid generating the dparser grammer. #[cfg(feature = "mcrl2_jittyc")] @@ -204,6 +205,7 @@ fn main() { rerun_if_changed!("cpp/atermpp.h"); rerun_if_changed!("cpp/exception.h"); rerun_if_changed!("cpp/data.h"); + rerun_if_changed!("cpp/data.cpp"); rerun_if_changed!("cpp/pbes.h"); rerun_if_changed!("cpp/pbes.cpp"); rerun_if_changed!("cpp/log.h"); diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp b/tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp new file mode 100644 index 00000000..855be3ab --- /dev/null +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp @@ -0,0 +1,28 @@ +#include "atermpp.h" +#include "mcrl2-sys/cpp/data.h" +#include "mcrl2-sys/src/data.rs.h" + +namespace mcrl2::data +{ + +std::unique_ptr mcrl2_data_expression_replace_variables(const atermpp::detail::_aterm& term, + const rust::Vec& sigma) +{ + atermpp::unprotected_aterm_core tmp_expr(&term); + MCRL2_ASSERT(is_data_expression(atermpp::down_cast(tmp_expr))); + + data::mutable_map_substitution<> tmp; + for (const auto& assign : sigma) + { + atermpp::unprotected_aterm_core tmp_lhs(assign.lhs); + atermpp::unprotected_aterm_core tmp_rhs(assign.rhs); + + tmp[atermpp::down_cast(tmp_lhs)] + = atermpp::down_cast(tmp_rhs); + } + + return std::make_unique( + data::replace_variables(atermpp::down_cast(tmp_expr), tmp)); +} + +} \ No newline at end of file diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/data.h b/tools/mcrl2/crates/mcrl2-sys/cpp/data.h index 2c6e6b43..8341d95d 100644 --- a/tools/mcrl2/crates/mcrl2-sys/cpp/data.h +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/data.h @@ -23,6 +23,10 @@ namespace mcrl2::data { + +// Forward declaration +struct assignment_pair; + inline std::unique_ptr mcrl2_data_specification_from_string(rust::Str input) { @@ -45,6 +49,9 @@ std::unique_ptr mcrl2_create_rewriter_jittyc(con #endif +std::unique_ptr mcrl2_data_expression_replace_variables(const atermpp::detail::_aterm& term, + const rust::Vec& sigma); + bool mcrl2_data_expression_is_variable(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h index 6cb624c9..1a41f9df 100644 --- a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h @@ -27,6 +27,7 @@ namespace mcrl2::pbes_system /// Alias for templated type. using srf_equation = detail::pre_srf_equation; +// Forward declaration struct vertex_outgoing_edge; struct assignment_pair; diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index d2590cb8..70ddacdc 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -2,6 +2,7 @@ /// Authors: Menno Bartels and Maurice Laveaux /// To keep consistent with the theory we allow non-snake case names. use std::cell::Cell; +use std::collections::HashSet; use std::iter; use itertools::Itertools; @@ -19,6 +20,8 @@ use mcrl2::PbesExpression; use mcrl2::PbesStategraph; use mcrl2::SrfPbes; use mcrl2::StategraphEquation; +use mcrl2::data_expression_variables; +use mcrl2::pbes_expression_pvi; use mcrl2::replace_propositional_variables; use mcrl2::replace_variables; use merc_io::LargeFormatter; @@ -259,9 +262,9 @@ impl SymmetryAlgorithm { info!("Parameter indices in clique: {:?}", control_flow_parameter_indices); - // Groups the data parameters by their sort. - let (mut number_of_permutations, all_data_groups) = if partition_data_sorts { - let same_sort_parameters = partition( + let data_parameter_partition = if partition_data_sorts { + // Groups the data parameters by their sort. + partition( self.parameters.iter().enumerate().filter_map(|(index, param)| { if self.all_control_flow_parameters.contains(&index) { // Skip control flow parameters. @@ -271,53 +274,77 @@ impl SymmetryAlgorithm { } }), |lhs, rhs| lhs.sort() == rhs.sort(), - ); + ) - let mut number_of_permutations = 1usize; - let mut all_data_groups: Box> = Box::new(iter::empty()); // Default value is overwritten in first iteration. - for group in same_sort_parameters { - // Determine the indices of these parameters. - let parameter_indices: Vec = group - .iter() - .map(|param| self.parameters.iter().position(|p| p.name() == param.name()).unwrap()) - .collect(); - - info!( - "Same sort data parameters: {:?}, indices: {:?}", - group, parameter_indices - ); - - // Compute the product of the current data group with the already concatenated ones. - let number_of_parametes = parameter_indices.len(); - if number_of_permutations == 1 { - all_data_groups = - Box::new(permutation_group(parameter_indices)) as Box>; + } else { + // All data parameters in a single group. + vec![self.parameters.iter().enumerate().filter_map(|(index, param)| { + if self.all_control_flow_parameters.contains(&index) { + // Skip control flow parameters. + None } else { - all_data_groups = Box::new( - all_data_groups - .cartesian_product(permutation_group(parameter_indices)) - .map(|(a, b)| a.concat(&b)), - ) as Box>; + Some(param) } + }).collect()] + }; + + let data_parameter_partition = if partition_data_updates { + let mut parameter_updates = vec![HashSet::new(); self.parameters.len()]; - number_of_permutations *= permutation_group_size(number_of_parametes); + // Figure out all the PVIs in which the parameter is updated. + for equation in self.srf.equations() { + for summand in equation.summands() { + for pvi in pbes_expression_pvi(&summand.variable().copy()) { + for (index, param) in self.parameters.iter().enumerate() { + if pvi.parameters().iter().any(|arg| arg == param) { + parameter_updates[index].insert(pvi.clone()); + } + } + } + } } - (number_of_permutations, all_data_groups) + for _group in &data_parameter_partition { + + } + + data_parameter_partition } else { - // All data parameters in a single group. - let parameter_indices: Vec = (0..self.parameters.len()) - .filter(|i| !self.all_control_flow_parameters.contains(i)) + // Do nothing + data_parameter_partition + }; + + // For progress messages keep track of the number of permutations we need to check. + let mut number_of_permutations = 1usize; + + let mut all_data_groups: Box> = Box::new(iter::empty()); // Default value is overwritten in first iteration. + for group in data_parameter_partition { + // Determine the indices of these parameters. + let parameter_indices: Vec = group + .iter() + .map(|param| self.parameters.iter().position(|p| p.name() == param.name()).unwrap()) .collect(); - info!("All data parameter indices: {:?}", parameter_indices); + info!( + "Same sort data parameters: {:?}, indices: {:?}", + group, parameter_indices + ); - let number_of_permutations = permutation_group_size(parameter_indices.len()); - let all_data_groups = - Box::new(permutation_group(parameter_indices.clone())) as Box>; + // Compute the product of the current data group with the already concatenated ones. + let number_of_parametes = parameter_indices.len(); + if number_of_permutations == 1 { + all_data_groups = + Box::new(permutation_group(parameter_indices)) as Box>; + } else { + all_data_groups = Box::new( + all_data_groups + .cartesian_product(permutation_group(parameter_indices)) + .map(|(a, b)| a.concat(&b)), + ) as Box>; + } - (number_of_permutations, all_data_groups) - }; + number_of_permutations *= permutation_group_size(number_of_parametes); + } number_of_permutations *= permutation_group_size(control_flow_parameter_indices.len()); @@ -660,6 +687,17 @@ where /// A constant representing an undefined index. const UNDEFINED_INDEX: usize = usize::MAX; +/// Replaces all variables in the expression by omega. +fn replace_variables_by_omega(expression: &DataExpression) -> DataExpression { + let variables = data_expression_variables(&expression.copy()); + + let omega = DataExpression::from(ATerm::with_args(&Symbol::new("OpId", 2), &[ATerm::constant::from("")])) + + let sigma = + + replace_variables(expr, sigma) +} + /// Returns the index of the variable that the control flow graph considers fn variable_index(cfg: &ControlFlowGraph) -> usize { // Check that all the vertices have the same variable assigned for consistency From 97583a9357a3f9991ed4df9dc10f6cef650dc859 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 12 Jan 2026 14:45:20 +0100 Subject: [PATCH 28/40] Added various helper functions. --- tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs | 8 ++++- .../crates/mcrl2/src/atermpp/aterm_list.rs | 14 ++++++++ .../crates/mcrl2/src/atermpp/random_term.rs | 4 +-- .../mcrl2/crates/mcrl2/src/data_expression.rs | 21 +++++++++++- tools/mcrl2/crates/mcrl2/src/pbes.rs | 4 +-- tools/mcrl2/crates/mcrl2/src/visitor.rs | 34 ++++++++++++++++--- 6 files changed, 75 insertions(+), 10 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs index 19bcc7bf..cd6fa221 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs @@ -218,10 +218,16 @@ pub struct ATerm { impl ATerm { /// Creates a new ATerm with the given symbol and arguments. - pub fn new<'a, 'b>(symbol: &impl Borrow>, arguments: &[impl Borrow>]) -> ATerm { + pub fn with_args<'a, 'b>(symbol: &impl Borrow>, arguments: &[impl Borrow>]) -> ATerm { THREAD_TERM_POOL.with_borrow(|tp| tp.create(symbol, arguments)) } + /// Creates a constant ATerm with the given symbol. + pub fn constant<'a>(symbol: &impl Borrow>) -> ATerm { + let tmp: &[ATermRef<'a>] = &[]; + THREAD_TERM_POOL.with_borrow(|tp| tp.create(symbol, tmp)) + } + /// Constructs an ATerm from a string by parsing it. pub fn from_string(s: &str) -> Result { THREAD_TERM_POOL.with_borrow(|tp| tp.from_string(s)) diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs index 83339b58..d5e4c6ce 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs @@ -49,6 +49,15 @@ impl ATermList { pub fn try_tail(&self) -> Option> { if self.is_empty() { None } else { Some(self.tail()) } } + + /// Casts the list to another type. This does not check whether the cast is + /// valid. + pub fn cast(&self) -> ATermList { + ATermList { + term: self.term.clone(), + _marker: PhantomData, + } + } } impl> ATermList { @@ -167,6 +176,11 @@ impl ATermListRef<'_, T> { pub fn is_empty(&self) -> bool { self.term.is_empty_list() } + + /// Protects the list by creating an owned version of it. + pub fn protect(&self) -> ATermList { + ATermList::new(self.term.protect()) + } } impl<'a, T: From> ATermListRef<'a, T> { diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/random_term.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/random_term.rs index a43bfc64..53c4e141 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/random_term.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/random_term.rs @@ -19,7 +19,7 @@ pub fn random_term( let mut subterms = HashSet::::from_iter( constants .iter() - .map(|name| ATerm::new(&Symbol::new(name, 0), &[] as &[ATerm])), + .map(|name| ATerm::with_args(&Symbol::new(name, 0), &[] as &[ATerm])), ); let mut result = ATerm::default(); @@ -31,7 +31,7 @@ pub fn random_term( arguments.push(subterms.iter().choose(rng).unwrap().clone()); } - result = ATerm::new(&Symbol::new(symbol, *arity), &arguments); + result = ATerm::with_args(&Symbol::new(symbol, *arity), &arguments); // Make this term available as another subterm that can be used. subterms.insert(result.clone()); diff --git a/tools/mcrl2/crates/mcrl2/src/data_expression.rs b/tools/mcrl2/crates/mcrl2/src/data_expression.rs index 83b93959..3ba5a709 100644 --- a/tools/mcrl2/crates/mcrl2/src/data_expression.rs +++ b/tools/mcrl2/crates/mcrl2/src/data_expression.rs @@ -1,4 +1,5 @@ use mcrl2_macros::mcrl2_derive_terms; +use mcrl2_sys::data::ffi::assignment_pair; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_abstraction; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_application; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_data_expression; @@ -7,9 +8,11 @@ use mcrl2_sys::data::ffi::mcrl2_data_expression_is_machine_number; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_untyped_identifier; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_variable; use mcrl2_sys::data::ffi::mcrl2_data_expression_is_where_clause; +use mcrl2_sys::data::ffi::mcrl2_data_expression_replace_variables; use mcrl2_sys::data::ffi::mcrl2_data_expression_to_string; use mcrl2_sys::data::ffi::mcrl2_is_data_sort_expression; +use crate::ATerm; use crate::ATermRef; /// Checks if this term is a data variable. @@ -79,7 +82,6 @@ mod inner { use crate::ATermArgs; use crate::ATermIntRef; use crate::ATermRef; - use crate::ATermString; use crate::ATermStringRef; use crate::Markable; use crate::Todo; @@ -345,6 +347,23 @@ mod inner { pub use inner::*; +pub fn substitute_variables(data_expression: &DataExpressionRef, sigma: Vec<(DataExpression, DataExpression)>) -> DataExpression { + // Do not into_iter here, as we need to keep sigma alive for the call. + let sigma: Vec = sigma + .iter() + .map(|(lhs, rhs)| assignment_pair { + lhs: lhs.address(), + rhs: rhs.address(), + }) + .collect(); + + DataExpression::new(ATerm::from_unique_ptr(mcrl2_data_expression_replace_variables( + data_expression.get(), + &sigma, + ))) +} + + // Allowed conversions impl From for DataExpression { fn from(var: DataVariable) -> Self { diff --git a/tools/mcrl2/crates/mcrl2/src/pbes.rs b/tools/mcrl2/crates/mcrl2/src/pbes.rs index 3dad7fc2..220fd2f1 100644 --- a/tools/mcrl2/crates/mcrl2/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2/src/pbes.rs @@ -453,7 +453,7 @@ impl fmt::Debug for PropositionalVariable { } /// Replace variables in the given PBES expression according to the given substitution sigma. -pub fn replace_variables(expr: &PbesExpression, sigma: Vec<(DataExpression, DataExpression)>) -> PbesExpression { +pub fn substitute_data_expressions(expr: &PbesExpression, sigma: Vec<(DataExpression, DataExpression)>) -> PbesExpression { // Do not into_iter here, as we need to keep sigma alive for the call. let sigma: Vec = sigma .iter() @@ -470,7 +470,7 @@ pub fn replace_variables(expr: &PbesExpression, sigma: Vec<(DataExpression, Data } /// Replaces propositional variables in the given PBES expression according to the given substitution sigma. -pub fn replace_propositional_variables(expr: &PbesExpression, pi: &Vec) -> PbesExpression { +pub fn reorder_propositional_variables(expr: &PbesExpression, pi: &Vec) -> PbesExpression { PbesExpression::new(ATerm::from_unique_ptr( mcrl2_pbes_expression_replace_propositional_variables(expr.term.get(), pi), )) diff --git a/tools/mcrl2/crates/mcrl2/src/visitor.rs b/tools/mcrl2/crates/mcrl2/src/visitor.rs index 92ce5067..9318de3b 100644 --- a/tools/mcrl2/crates/mcrl2/src/visitor.rs +++ b/tools/mcrl2/crates/mcrl2/src/visitor.rs @@ -5,6 +5,7 @@ use crate::DataExpressionRef; use crate::DataFunctionSymbolRef; use crate::DataMachineNumberRef; use crate::DataUntypedIdentifierRef; +use crate::DataVariable; use crate::DataVariableRef; use crate::DataWhereClauseRef; use crate::PbesAndRef; @@ -156,6 +157,8 @@ pub trait PbesExpressionVisitor { /// Replaces data variables in the given data expression according to the /// provided substitution function. +/// +/// TODO: This is not yet functional, the replacements actually do not work. pub fn data_expression_replace_variables(expr: &DataExpressionRef<'_>, f: &F) -> DataExpression where F: Fn(&DataVariableRef<'_>) -> DataExpression, @@ -181,11 +184,12 @@ where pub fn pbes_expression_pvi(expr: &PbesExpressionRef<'_>) -> Vec { let mut result = Vec::new(); - struct PviChecker<'a> { + /// Local struct that is used to collect PVI occurrences. + struct PviOccurrences<'a> { result: &'a mut Vec, } - impl PbesExpressionVisitor for PviChecker<'_> { + impl PbesExpressionVisitor for PviOccurrences<'_> { fn visit_propositional_variable_instantiation( &mut self, inst: &PbesPropositionalVariableInstantiationRef<'_>, @@ -197,8 +201,30 @@ pub fn pbes_expression_pvi(expr: &PbesExpressionRef<'_>) -> Vec) -> Vec { + let mut result = Vec::new(); + + /// Local struct that is used to collect PVI occurrences. + struct VariableOccurrences<'a> { + result: &'a mut Vec, + } + + impl DataExpressionVisitor for VariableOccurrences<'_> { + fn visit_variable(&mut self, var: &DataVariableRef<'_>) -> Option { + // Found a propositional variable instantiation, return true. + self.result + .push(DataVariable::from(var.protect())); + None + } + } - checker.visit(expr); + let mut occurrences = VariableOccurrences { result: &mut result }; + occurrences.visit(expr); result } From ac289f2a43991b15739785c51a9e6e7236198e28 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 12 Jan 2026 15:19:29 +0100 Subject: [PATCH 29/40] Added missing inline keywords --- tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp | 5 ++++- tools/mcrl2/crates/mcrl2-sys/cpp/data.h | 10 ++++++++++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp b/tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp index 855be3ab..2d6ad8d0 100644 --- a/tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp @@ -1,4 +1,7 @@ #include "atermpp.h" +#include "mcrl2/data/substitutions/mutable_map_substitution.h" +#include "mcrl2/data/replace.h" + #include "mcrl2-sys/cpp/data.h" #include "mcrl2-sys/src/data.rs.h" @@ -22,7 +25,7 @@ std::unique_ptr mcrl2_data_expression_replace_variables(const at } return std::make_unique( - data::replace_variables(atermpp::down_cast(tmp_expr), tmp)); + replace_variables(atermpp::down_cast(tmp_expr), tmp)); } } \ No newline at end of file diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/data.h b/tools/mcrl2/crates/mcrl2-sys/cpp/data.h index 8341d95d..0e871812 100644 --- a/tools/mcrl2/crates/mcrl2-sys/cpp/data.h +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/data.h @@ -52,60 +52,70 @@ std::unique_ptr mcrl2_create_rewriter_jittyc(con std::unique_ptr mcrl2_data_expression_replace_variables(const atermpp::detail::_aterm& term, const rust::Vec& sigma); +inline bool mcrl2_data_expression_is_variable(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); return data::is_variable(atermpp::down_cast(tmp)); } +inline bool mcrl2_data_expression_is_application(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); return data::is_application(atermpp::down_cast(tmp)); } +inline bool mcrl2_data_expression_is_abstraction(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); return data::is_abstraction(atermpp::down_cast(tmp)); } +inline bool mcrl2_data_expression_is_function_symbol(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); return data::is_function_symbol(atermpp::down_cast(tmp)); } +inline bool mcrl2_data_expression_is_where_clause(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); return data::is_where_clause(atermpp::down_cast(tmp)); } +inline bool mcrl2_data_expression_is_machine_number(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); return data::is_machine_number(atermpp::down_cast(tmp)); } +inline bool mcrl2_data_expression_is_untyped_identifier(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); return data::is_untyped_identifier(atermpp::down_cast(tmp)); } +inline bool mcrl2_data_expression_is_data_expression(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); return data::is_data_expression(atermpp::down_cast(tmp)); } +inline bool mcrl2_is_data_sort_expression(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); return data::is_sort_expression(atermpp::down_cast(tmp)); } +inline rust::String mcrl2_data_expression_to_string(const atermpp::detail::_aterm& input) { atermpp::unprotected_aterm_core tmp(&input); From ddd67f4ffb7b4f82837a2bc1737cb54ff7c5ad2e Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 12 Jan 2026 15:51:59 +0100 Subject: [PATCH 30/40] Added a not yet correct version of partitioning parameters on their update expressions. --- tools/mcrl2/crates/mcrl2-sys/src/data.rs | 16 ++++ .../crates/mcrl2/src/atermpp/aterm_list.rs | 2 +- tools/mcrl2/pbes/src/main.rs | 10 +- tools/mcrl2/pbes/src/permutation.rs | 1 - tools/mcrl2/pbes/src/symmetry.rs | 96 +++++++++++++------ 5 files changed, 91 insertions(+), 34 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2-sys/src/data.rs b/tools/mcrl2/crates/mcrl2-sys/src/data.rs index 803fd324..088f85eb 100644 --- a/tools/mcrl2/crates/mcrl2-sys/src/data.rs +++ b/tools/mcrl2/crates/mcrl2-sys/src/data.rs @@ -1,5 +1,12 @@ #[cxx::bridge(namespace = "mcrl2::data")] pub mod ffi { + + /// A helper struct for std::pair> + struct assignment_pair { + pub lhs: *const _aterm, + pub rhs: *const _aterm, + } + unsafe extern "C++" { include!("mcrl2-sys/cpp/data.h"); include!("mcrl2-sys/cpp/exception.h"); @@ -26,6 +33,15 @@ pub mod ffi { #[namespace = "atermpp::detail"] type _aterm = crate::atermpp::ffi::_aterm; + #[namespace = "atermpp"] + type aterm = crate::atermpp::ffi::aterm; + + /// Replace variables in the given data expression according to the given substitution sigma. + fn mcrl2_data_expression_replace_variables( + input: &_aterm, + sigma: &Vec, + ) -> UniquePtr; + // Recognizers for the various variants of data expressions. fn mcrl2_data_expression_is_variable(input: &_aterm) -> bool; fn mcrl2_data_expression_is_application(input: &_aterm) -> bool; diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs index d5e4c6ce..f225e064 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs @@ -204,7 +204,7 @@ impl<'a, T> From> for ATermListRef<'a, T> { } pub struct ATermListIterRef<'a, T> { - current: ATermListRef<'a, T>, + _current: ATermListRef<'a, T>, } // impl<'a, T: From> Iterator for ATermListIterRef<'a, T> { diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index 3ecfcb93..103dc6fb 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -73,6 +73,10 @@ struct SymmetryArgs { /// Partition data parameters based on their updates. #[arg(long, default_value_t = false)] partition_data_updates: bool, + + /// Print the symmetry in the mapping notation instead of the cycle notation. + #[arg(long, default_value_t = false)] + mapping_notation: bool, } fn main() -> Result { @@ -125,7 +129,11 @@ fn main() -> Result { info!("Found candidate: {}", candidate); if algorithm.check_symmetry(&candidate) { - info!("Found symmetry: {}", candidate); + if args.mapping_notation { + info!("Found symmetry: {:?}", candidate); + } else { + info!("Found symmetry: {}", candidate); + } if !args.all_symmetries && !candidate.is_identity() { // Only search for the first symmetry diff --git a/tools/mcrl2/pbes/src/permutation.rs b/tools/mcrl2/pbes/src/permutation.rs index 14abf518..bc05b928 100644 --- a/tools/mcrl2/pbes/src/permutation.rs +++ b/tools/mcrl2/pbes/src/permutation.rs @@ -170,7 +170,6 @@ impl Permutation { } /// Checks whether the mapping represents a valid permutation -#[cfg(debug_assertions)] pub fn is_valid_permutation(mapping: &Vec<(usize, usize)>) -> bool { let mut domain = HashSet::with_capacity(mapping.len()); let mut image = HashSet::with_capacity(mapping.len()); diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 70ddacdc..7b922c1f 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -10,6 +10,7 @@ use log::debug; use log::info; use log::trace; +use mcrl2::ATerm; use mcrl2::ATermString; use mcrl2::ControlFlowGraph; use mcrl2::ControlFlowGraphVertex; @@ -20,10 +21,12 @@ use mcrl2::PbesExpression; use mcrl2::PbesStategraph; use mcrl2::SrfPbes; use mcrl2::StategraphEquation; +use mcrl2::Symbol; use mcrl2::data_expression_variables; use mcrl2::pbes_expression_pvi; -use mcrl2::replace_propositional_variables; -use mcrl2::replace_variables; +use mcrl2::reorder_propositional_variables; +use mcrl2::substitute_data_expressions; +use mcrl2::substitute_variables; use merc_io::LargeFormatter; use merc_io::TimeProgress; use merc_utilities::MercError; @@ -104,9 +107,13 @@ impl SymmetryAlgorithm { } /// Returns compliant permutations. - /// + /// /// See [clique_candidates] for the parameters. - pub fn candidates(&self, partition_data_sorts: bool, partition_data_updates: bool) -> impl Iterator + '_ { + pub fn candidates( + &self, + partition_data_sorts: bool, + partition_data_updates: bool, + ) -> impl Iterator + '_ { let cliques = self.cliques(); for clique in &cliques { @@ -124,7 +131,8 @@ impl SymmetryAlgorithm { let mut number_of_candidates = 1usize; for clique in &cliques { - let (number_of_permutations, candidates) = self.clique_candidates(clique.clone(), partition_data_sorts, partition_data_updates); + let (number_of_permutations, candidates) = + self.clique_candidates(clique.clone(), partition_data_sorts, partition_data_updates); info!( "Maximum number of permutations for clique {:?}: {}", clique, @@ -274,18 +282,23 @@ impl SymmetryAlgorithm { } }), |lhs, rhs| lhs.sort() == rhs.sort(), - ) - + ) } else { // All data parameters in a single group. - vec![self.parameters.iter().enumerate().filter_map(|(index, param)| { - if self.all_control_flow_parameters.contains(&index) { - // Skip control flow parameters. - None - } else { - Some(param) - } - }).collect()] + vec![ + self.parameters + .iter() + .enumerate() + .filter_map(|(index, param)| { + if self.all_control_flow_parameters.contains(&index) { + // Skip control flow parameters. + None + } else { + Some(param) + } + }) + .collect(), + ] }; let data_parameter_partition = if partition_data_updates { @@ -295,20 +308,33 @@ impl SymmetryAlgorithm { for equation in self.srf.equations() { for summand in equation.summands() { for pvi in pbes_expression_pvi(&summand.variable().copy()) { - for (index, param) in self.parameters.iter().enumerate() { - if pvi.parameters().iter().any(|arg| arg == param) { - parameter_updates[index].insert(pvi.clone()); - } + for (index, param) in pvi.arguments().protect().cast::().iter().enumerate() { + parameter_updates[index].insert(replace_variables_by_omega(¶m)); } } } } - for _group in &data_parameter_partition { + for (index, param) in self.parameters.iter().enumerate() { + debug!( + "Parameter {} is updated with expressions: {}", + param.name(), + parameter_updates[index] + .iter() + .map(|expr| expr.to_string()) + .join(", ") + ); + } - } + let mut update_partition = Vec::new(); + for group in data_parameter_partition { + update_partition.extend(partition(group.iter().cloned(), |lhs, rhs| { + parameter_updates[self.parameters.iter().position(|p| p.name() == lhs.name()).unwrap()] + == parameter_updates[self.parameters.iter().position(|p| p.name() == rhs.name()).unwrap()] + })); + } - data_parameter_partition + update_partition } else { // Do nothing data_parameter_partition @@ -326,7 +352,7 @@ impl SymmetryAlgorithm { .collect(); info!( - "Same sort data parameters: {:?}, indices: {:?}", + "Parameters group: {:?}, indices: {:?}", group, parameter_indices ); @@ -684,20 +710,28 @@ where result } -/// A constant representing an undefined index. -const UNDEFINED_INDEX: usize = usize::MAX; - /// Replaces all variables in the expression by omega. fn replace_variables_by_omega(expression: &DataExpression) -> DataExpression { let variables = data_expression_variables(&expression.copy()); - let omega = DataExpression::from(ATerm::with_args(&Symbol::new("OpId", 2), &[ATerm::constant::from("")])) + // Generate an omega variable. + let omega = DataExpression::from(ATerm::with_args( + &Symbol::new("OpId", 2), + &[ATerm::constant(&Symbol::new("omega", 0)), + ATerm::with_args(&Symbol::new("SortId", 1), &[ATerm::constant(&Symbol::new("@untyped", 0))])], + )); - let sigma = + let sigma = variables + .iter() + .map(|var| (var.clone().into(), omega.clone())) + .collect::>(); - replace_variables(expr, sigma) + substitute_variables(&expression.copy(), sigma) } +/// A constant representing an undefined vertex. +const UNDEFINED_INDEX: usize = usize::MAX; + /// Returns the index of the variable that the control flow graph considers fn variable_index(cfg: &ControlFlowGraph) -> usize { // Check that all the vertices have the same variable assigned for consistency @@ -738,10 +772,10 @@ fn apply_permutation(expression: &PbesExpression, parameters: &Vec }) .collect(); - let result = replace_variables(expression, sigma); + let result = substitute_data_expressions(expression, sigma); let pi = (0..parameters.len()).map(|i| pi.value(i)).collect::>(); - replace_propositional_variables(&result, &pi) + reorder_propositional_variables(&result, &pi) } #[cfg(test)] From e5b64fd03e89106e3f0dc53a0541b6fcdcb42a1c Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 14 Jan 2026 14:54:29 +0100 Subject: [PATCH 31/40] Revert "Deal with the undefined vertex in cfgs." This reverts commit b5598b7107f60e6d08e6a75314e0827231874ba3. --- tools/mcrl2/pbes/src/symmetry.rs | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 7b922c1f..8ad681a8 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -729,15 +729,11 @@ fn replace_variables_by_omega(expression: &DataExpression) -> DataExpression { substitute_variables(&expression.copy(), sigma) } -/// A constant representing an undefined vertex. -const UNDEFINED_INDEX: usize = usize::MAX; - /// Returns the index of the variable that the control flow graph considers fn variable_index(cfg: &ControlFlowGraph) -> usize { // Check that all the vertices have the same variable assigned for consistency cfg.vertices().iter().for_each(|v| { - if v.index() != UNDEFINED_INDEX // Ignore undefined indices - && v.index() + if v.index() != cfg .vertices() .first() @@ -748,8 +744,8 @@ fn variable_index(cfg: &ControlFlowGraph) -> usize { } }); - if let Some(v) = cfg.vertices().iter().find(|v| v.index() != UNDEFINED_INDEX) { - // Simply return the index of the first vertex that is defined. + if let Some(v) = cfg.vertices().iter().next() { + // Simply return the index of the variable return v.index(); } From 555feb0055ca17e0bb4a2160c4a5887e8fbb6c78 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 14 Jan 2026 17:14:29 +0100 Subject: [PATCH 32/40] Normalize the PBES after the SRF transformation --- tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h | 13 ++++++++----- tools/mcrl2/crates/mcrl2-sys/src/pbes.rs | 3 +++ tools/mcrl2/crates/mcrl2/src/pbes.rs | 6 ++++++ tools/mcrl2/pbes/src/main.rs | 6 +++++- tools/mcrl2/pbes/src/symmetry.rs | 15 +++++++-------- 5 files changed, 29 insertions(+), 14 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h index 1a41f9df..87d5d245 100644 --- a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h @@ -64,6 +64,12 @@ std::unique_ptr mcrl2_pbes_data_specification(const pb return std::make_unique(pbesspec.data()); } +inline +void mcrl2_pbes_normalize(pbes& pbesspec) +{ + algorithms::normalize(pbesspec); +} + inline rust::String mcrl2_pbes_to_string(const pbes& pbesspec) { @@ -87,15 +93,12 @@ class stategraph_algorithm : private detail::stategraph_local_algorithm public: stategraph_algorithm(const pbes& input) - : super(input, pbesstategraph_options{.print_influence_graph = true}) + : super(input, pbesstategraph_options{.cache_marking_updates = true}) {} void run() override { - // We explicitly ignore the virtual call to run in the base class - detail::stategraph_algorithm::stategraph_algorithm::run(); // NOLINT(bugprone-parent-virtual-call) - - compute_local_control_flow_graphs(); + super::run(); for (decltype(m_local_control_flow_graphs)::iterator i = m_local_control_flow_graphs.begin(); i != m_local_control_flow_graphs.end(); diff --git a/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs b/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs index 06ce448a..184a348b 100644 --- a/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs @@ -29,6 +29,9 @@ pub mod ffi { /// Loads a PBES from a string. fn mcrl2_load_pbes_from_text(input: &str) -> Result>; + /// Normaklizes a PBES. + fn mcrl2_pbes_normalize(input: Pin<&mut pbes>); + #[namespace = "mcrl2::data"] type data_specification = crate::data::ffi::data_specification; diff --git a/tools/mcrl2/crates/mcrl2/src/pbes.rs b/tools/mcrl2/crates/mcrl2/src/pbes.rs index 220fd2f1..2c770aac 100644 --- a/tools/mcrl2/crates/mcrl2/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2/src/pbes.rs @@ -85,6 +85,12 @@ impl Pbes { DataSpecification::new(mcrl2_pbes_data_specification(&self.pbes)) } + /// Normalizes the PBES. + pub fn normalize(&mut self) { + mcrl2_sys::pbes::ffi::mcrl2_pbes_normalize(self.pbes.pin_mut()); + } + + /// Creates a new PBES from the given FFI PBES pointer. pub(crate) fn new(pbes: UniquePtr) -> Self { Pbes { pbes } } diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index 103dc6fb..08c7d00a 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -77,6 +77,10 @@ struct SymmetryArgs { /// Print the symmetry in the mapping notation instead of the cycle notation. #[arg(long, default_value_t = false)] mapping_notation: bool, + + /// Print the SRF representation of the PBES. + #[arg(long, default_value_t = false)] + print_srf: bool, } fn main() -> Result { @@ -105,7 +109,7 @@ fn main() -> Result { PbesFormat::Text => Pbes::from_text_file(&args.filename)?, }; - let algorithm = SymmetryAlgorithm::new(&pbes, false)?; + let algorithm = SymmetryAlgorithm::new(&pbes, args.print_srf)?; if let Some(permutation) = &args.permutation { let pi = if permutation.trim_start().starts_with("[") { Permutation::from_mapping_notation(permutation)? diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 8ad681a8..33aa544b 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -55,12 +55,6 @@ pub struct SymmetryAlgorithm { progress: TimeProgress, } -// #[derive(Error, Debug)] -// enum CompatibleReason { -// #[error("Different number of vertices: {0} vs {1}")] -// InvalidVertexSets(usize, usize) -// } - impl SymmetryAlgorithm { /// Does the required preprocessing to analyse symmetries in the given PBES. pub fn new(pbes: &Pbes, print_srf: bool) -> Result { @@ -72,7 +66,7 @@ impl SymmetryAlgorithm { info!("==== SRF PBES ===="); info!("{}", srf.to_pbes()); } - + let parameters = if let Some(equation) = srf.equations().first() { equation.variable().parameters().to_vec() } else { @@ -82,7 +76,12 @@ impl SymmetryAlgorithm { info!("Unified parameters: {}", parameters.iter().format(", ")); - let state_graph = PbesStategraph::run(&srf.to_pbes())?; + let state_graph = { + let mut pbes = srf.to_pbes(); + pbes.normalize(); + PbesStategraph::run(&pbes)? + }; + let all_control_flow_parameters = state_graph .control_flow_graphs() .iter() From 42e3493a9d9af900e0d51f4a20b1000e85826074 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 14 Jan 2026 17:14:50 +0100 Subject: [PATCH 33/40] Avoid adding the identity mappings, and add is_well_typed to PBES. --- tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h | 6 ++++++ tools/mcrl2/crates/mcrl2-sys/src/pbes.rs | 5 ++++- tools/mcrl2/crates/mcrl2/src/pbes.rs | 5 +++++ tools/mcrl2/pbes/src/permutation.rs | 11 +++++++++-- tools/mcrl2/pbes/src/symmetry.rs | 1 + 5 files changed, 25 insertions(+), 3 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h index 87d5d245..82c217b1 100644 --- a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h @@ -70,6 +70,12 @@ void mcrl2_pbes_normalize(pbes& pbesspec) algorithms::normalize(pbesspec); } +inline +bool mcrl2_pbes_is_well_typed(const pbes& pbesspec) +{ + return pbesspec.is_well_typed(); +} + inline rust::String mcrl2_pbes_to_string(const pbes& pbesspec) { diff --git a/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs b/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs index 184a348b..75e60340 100644 --- a/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs @@ -29,9 +29,12 @@ pub mod ffi { /// Loads a PBES from a string. fn mcrl2_load_pbes_from_text(input: &str) -> Result>; - /// Normaklizes a PBES. + /// Normalizes a PBES. fn mcrl2_pbes_normalize(input: Pin<&mut pbes>); + /// Checks whether the PBES is well-typed. + fn mcrl2_pbes_is_well_typed(input: &pbes) -> bool; + #[namespace = "mcrl2::data"] type data_specification = crate::data::ffi::data_specification; diff --git a/tools/mcrl2/crates/mcrl2/src/pbes.rs b/tools/mcrl2/crates/mcrl2/src/pbes.rs index 2c770aac..a7026365 100644 --- a/tools/mcrl2/crates/mcrl2/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2/src/pbes.rs @@ -90,6 +90,11 @@ impl Pbes { mcrl2_sys::pbes::ffi::mcrl2_pbes_normalize(self.pbes.pin_mut()); } + /// Checks whether the PBES is well-typed. + pub fn is_well_typed(&self) -> bool { + mcrl2_sys::pbes::ffi::mcrl2_pbes_is_well_typed(&self.pbes) + } + /// Creates a new PBES from the given FFI PBES pointer. pub(crate) fn new(pbes: UniquePtr) -> Self { Pbes { pbes } diff --git a/tools/mcrl2/pbes/src/permutation.rs b/tools/mcrl2/pbes/src/permutation.rs index bc05b928..0bf494bd 100644 --- a/tools/mcrl2/pbes/src/permutation.rs +++ b/tools/mcrl2/pbes/src/permutation.rs @@ -25,6 +25,10 @@ impl Permutation { // Sort by domain for deterministic representation. mapping.sort_unstable_by_key(|(d, _)| *d); + debug_assert!( + mapping.iter().is_sorted(), + "Mapping should be sorted by domain." + ); debug_assert!( mapping.iter().all(|(from, to)| from != to), "Mapping should not contain identity mappings." @@ -262,9 +266,12 @@ impl fmt::Debug for Permutation { /// - (0 4 3) pub fn permutation_group(indices: Vec) -> impl Iterator + Clone { let n = indices.len(); - let indices2 = indices.clone(); + + // Clone the indices for use in the closure. + let indices_rhs = indices.clone(); indices.into_iter().permutations(n).map(move |perm| { - let mapping: Vec<(usize, usize)> = indices2.iter().cloned().zip(perm).collect(); + // Remove identity mappings. + let mapping: Vec<(usize, usize)> = indices_rhs.iter().cloned().zip(perm).filter(|(x, y)| x != y).collect(); Permutation::from_mapping(mapping) }) } diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 33aa544b..e10e5ece 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -79,6 +79,7 @@ impl SymmetryAlgorithm { let state_graph = { let mut pbes = srf.to_pbes(); pbes.normalize(); + debug_assert!(pbes.is_well_typed(), "PBES should be well-typed after normalization."); PbesStategraph::run(&pbes)? }; From 9b417aacaf1d9d5a28ee2053b2fc4bfd35cb2478 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 14 Jan 2026 17:22:08 +0100 Subject: [PATCH 34/40] Only compute the CFGs. --- tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h index 82c217b1..969d400c 100644 --- a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h @@ -104,7 +104,10 @@ class stategraph_algorithm : private detail::stategraph_local_algorithm void run() override { - super::run(); + // We explicitly ignore the virtual call to run in the base class + detail::stategraph_algorithm::stategraph_algorithm::run(); // NOLINT(bugprone-parent-virtual-call) + + compute_local_control_flow_graphs(); for (decltype(m_local_control_flow_graphs)::iterator i = m_local_control_flow_graphs.begin(); i != m_local_control_flow_graphs.end(); From 975120b2865b41e6daadd0230c3003491bacb9c3 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 14 Jan 2026 17:37:18 +0100 Subject: [PATCH 35/40] Ensure that the omega function symbols are valid data expressions. --- tools/mcrl2/crates/mcrl2-sys/cpp/atermpp.h | 7 +++++++ tools/mcrl2/crates/mcrl2-sys/src/atermpp.rs | 3 +++ tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs | 10 ++++++++++ .../crates/mcrl2/src/atermpp/thread_aterm_pool.rs | 11 +++++++++++ tools/mcrl2/pbes/src/symmetry.rs | 12 +++++++++--- 5 files changed, 40 insertions(+), 3 deletions(-) diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/atermpp.h b/tools/mcrl2/crates/mcrl2-sys/cpp/atermpp.h index ea84d30b..9e0ede0c 100644 --- a/tools/mcrl2/crates/mcrl2-sys/cpp/atermpp.h +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/atermpp.h @@ -149,6 +149,13 @@ inline const detail::_aterm* mcrl2_aterm_create(const detail::_function_symbol& return 0; } +inline const detail::_aterm* mcrl2_aterm_create_int(std::uint64_t value) +{ + atermpp::unprotected_aterm_core result(nullptr); + make_aterm_int(reinterpret_cast(result), static_cast(value)); + return detail::address(result); +} + inline std::unique_ptr mcrl2_aterm_from_string(rust::Str text) { return std::make_unique(read_term_from_string(static_cast(text))); diff --git a/tools/mcrl2/crates/mcrl2-sys/src/atermpp.rs b/tools/mcrl2/crates/mcrl2-sys/src/atermpp.rs index 68886d64..692b6047 100644 --- a/tools/mcrl2/crates/mcrl2-sys/src/atermpp.rs +++ b/tools/mcrl2/crates/mcrl2-sys/src/atermpp.rs @@ -71,6 +71,9 @@ pub mod ffi { /// garbage collection marks the terms, which is done atomically. unsafe fn mcrl2_aterm_create(function: &_function_symbol, arguments: &[*const _aterm]) -> *const _aterm; + /// Creates an aterm_int from the given value. + fn mcrl2_aterm_create_int(value: u64) -> *const _aterm; + /// Parses the given string and returns an aterm fn mcrl2_aterm_from_string(text: &str) -> Result>; diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs index 69e524b3..8577d2ad 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs @@ -11,11 +11,13 @@ pub fn is_aterm_int(term: &ATermRef<'_>) -> bool { #[mcrl2_derive_terms] mod inner { + use mcrl2_macros::mcrl2_ignore; use mcrl2_macros::mcrl2_term; use crate::ATerm; use crate::ATermRef; use crate::Markable; + use crate::THREAD_TERM_POOL; use crate::Todo; use crate::is_aterm_int; @@ -26,6 +28,14 @@ mod inner { } impl ATermInt { + /// Creates a new ATermInt from the given string value. + #[mcrl2_ignore] + pub fn with_value(value: u64) -> Self { + Self { + term: THREAD_TERM_POOL.with_borrow(|tp| tp.create_int(value)) + } + } + /// Returns the string value. pub fn value(&self) -> u64 { // The Rust::Str should ensure that this is a valid string. diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/thread_aterm_pool.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/thread_aterm_pool.rs index 3437bd69..6e07b041 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/thread_aterm_pool.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/thread_aterm_pool.rs @@ -9,6 +9,7 @@ use log::trace; use mcrl2_sys::atermpp::ffi; use mcrl2_sys::atermpp::ffi::mcrl2_aterm_create; +use mcrl2_sys::atermpp::ffi::mcrl2_aterm_create_int; use mcrl2_sys::atermpp::ffi::mcrl2_aterm_from_string; use mcrl2_sys::atermpp::ffi::mcrl2_aterm_pool_collect_garbage; use mcrl2_sys::atermpp::ffi::mcrl2_aterm_pool_print_metrics; @@ -163,6 +164,16 @@ impl ThreadTermPool { } } + /// Creates an aterm_int from the given value. + pub fn create_int(&self, value: u64) -> ATerm { + unsafe { + // ThreadPool is not Sync, so only one has access. + let protection_set = self.protection_set.write_exclusive(); + let term: *const ffi::_aterm = mcrl2_aterm_create_int(value); + self.protect_with(protection_set, term) + } + } + /// Creates a function symbol with the given name and arity. pub fn create_symbol(&self, name: &str, arity: usize) -> Symbol { Symbol::take(mcrl2_function_symbol_create(String::from(name), arity)) diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index e10e5ece..694adfc3 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -11,6 +11,7 @@ use log::info; use log::trace; use mcrl2::ATerm; +use mcrl2::ATermInt; use mcrl2::ATermString; use mcrl2::ControlFlowGraph; use mcrl2::ControlFlowGraphVertex; @@ -716,9 +717,14 @@ fn replace_variables_by_omega(expression: &DataExpression) -> DataExpression { // Generate an omega variable. let omega = DataExpression::from(ATerm::with_args( - &Symbol::new("OpId", 2), - &[ATerm::constant(&Symbol::new("omega", 0)), - ATerm::with_args(&Symbol::new("SortId", 1), &[ATerm::constant(&Symbol::new("@untyped", 0))])], + &Symbol::new("OpId", 3), + &[ + // Identifier + ATerm::constant(&Symbol::new("omega", 0)), + // Sort + ATerm::with_args(&Symbol::new("SortId", 1), &[ATerm::constant(&Symbol::new("@NoValue", 0))]), + // Index + ATermInt::with_value(0).into()], )); let sigma = variables From f44898537faa1e25b55761ff4f418c41d815e0f0 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 19 Jan 2026 16:04:00 +0100 Subject: [PATCH 36/40] Deal with the question mark vertices by ignoring them when finding the CFG index. --- tools/mcrl2/pbes/src/main.rs | 3 ++- tools/mcrl2/pbes/src/symmetry.rs | 11 +++++++---- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index 08c7d00a..47d1fcfd 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -2,6 +2,7 @@ use std::process::ExitCode; use clap::Parser; use clap::Subcommand; +use log::debug; use log::info; use mcrl2::Pbes; @@ -130,7 +131,7 @@ fn main() -> Result { } } else { for candidate in algorithm.candidates(args.partition_data_sorts, args.partition_data_updates) { - info!("Found candidate: {}", candidate); + debug!("Found candidate: {}", candidate); if algorithm.check_symmetry(&candidate) { if args.mapping_notation { diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 694adfc3..3c94dbf6 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -735,11 +735,14 @@ fn replace_variables_by_omega(expression: &DataExpression) -> DataExpression { substitute_variables(&expression.copy(), sigma) } +/// A constant representing an undefined vertex. +const UNDEFINED_VERTEX: usize = usize::MAX; + /// Returns the index of the variable that the control flow graph considers fn variable_index(cfg: &ControlFlowGraph) -> usize { // Check that all the vertices have the same variable assigned for consistency cfg.vertices().iter().for_each(|v| { - if v.index() + if v.index() != UNDEFINED_VERTEX && v.index() != cfg .vertices() .first() @@ -749,9 +752,9 @@ fn variable_index(cfg: &ControlFlowGraph) -> usize { panic!("Inconsistent variable indices in control flow graph."); } }); - - if let Some(v) = cfg.vertices().iter().next() { - // Simply return the index of the variable + + if let Some(v) = cfg.vertices().iter().find(|v| v.index() != UNDEFINED_VERTEX) { + // Return the first non-undefined index return v.index(); } From c12e6ca55756f58fe867f445d726cfa4cdfc4c4a Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 19 Jan 2026 16:33:41 +0100 Subject: [PATCH 37/40] Avoid overflow, and deal with the empty partition --- tools/mcrl2/pbes/src/symmetry.rs | 45 ++++++++++++++++++++------------ 1 file changed, 28 insertions(+), 17 deletions(-) diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 3c94dbf6..fff8509f 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -151,7 +151,8 @@ impl SymmetryAlgorithm { ) as Box>; } - number_of_candidates *= number_of_permutations; + // If the number overflows we probably don't really care. + number_of_candidates = number_of_candidates.saturating_mul(number_of_permutations); } info!( @@ -285,21 +286,26 @@ impl SymmetryAlgorithm { |lhs, rhs| lhs.sort() == rhs.sort(), ) } else { - // All data parameters in a single group. - vec![ - self.parameters - .iter() - .enumerate() - .filter_map(|(index, param)| { - if self.all_control_flow_parameters.contains(&index) { - // Skip control flow parameters. - None - } else { - Some(param) - } - }) - .collect(), - ] + let groups: Vec<&DataVariable> = self.parameters + .iter() + .enumerate() + .filter_map(|(index, param)| { + if self.all_control_flow_parameters.contains(&index) { + // Skip control flow parameters. + None + } else { + Some(param) + } + }) + .collect(); + + if groups.is_empty() { + // No data parameters. + Vec::new() + } else { + // All data parameters in a single group. + vec![groups] + } }; let data_parameter_partition = if partition_data_updates { @@ -353,7 +359,7 @@ impl SymmetryAlgorithm { .collect(); info!( - "Parameters group: {:?}, indices: {:?}", + "Data parameters group: {:?}, indices: {:?}", group, parameter_indices ); @@ -696,6 +702,8 @@ where let mut result: Vec> = Vec::new(); for element in elements { + // See if the element can be added to an existing group, by taking the first element of + // each group as representative. if let Some(group) = result.iter_mut().find(|g: &&mut Vec<_>| { if let Some(first) = g.first() { predicate(first, &element) @@ -703,11 +711,14 @@ where false } }) { + // Add to existing group group.push(element.clone()); } else { + // Create new group result.push(vec![element.clone()]); } } + result } From cf40f70617ff37ec3ef631a4c8a1bbd801aa49ca Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 19 Jan 2026 16:48:06 +0100 Subject: [PATCH 38/40] Do not print the identity permutation --- tools/mcrl2/pbes/src/main.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/tools/mcrl2/pbes/src/main.rs b/tools/mcrl2/pbes/src/main.rs index 47d1fcfd..95643ccb 100644 --- a/tools/mcrl2/pbes/src/main.rs +++ b/tools/mcrl2/pbes/src/main.rs @@ -70,7 +70,7 @@ struct SymmetryArgs { /// Partition data parameters into their sorts before considering their permutation groups. #[arg(long, default_value_t = false)] partition_data_sorts: bool, - + /// Partition data parameters based on their updates. #[arg(long, default_value_t = false)] partition_data_updates: bool, @@ -133,6 +133,11 @@ fn main() -> Result { for candidate in algorithm.candidates(args.partition_data_sorts, args.partition_data_updates) { debug!("Found candidate: {}", candidate); + if candidate.is_identity() { + // Skip the identity permutation + continue; + } + if algorithm.check_symmetry(&candidate) { if args.mapping_notation { info!("Found symmetry: {:?}", candidate); @@ -140,7 +145,7 @@ fn main() -> Result { info!("Found symmetry: {}", candidate); } - if !args.all_symmetries && !candidate.is_identity() { + if !args.all_symmetries { // Only search for the first symmetry info!("Stopping search after first non-trivial symmetry."); break; From cc3758827683bb80a9cdff4ccac90aa11df0b8dc Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 19 Jan 2026 16:48:46 +0100 Subject: [PATCH 39/40] Deal with no data parameters by starting with the identity mapping --- tools/mcrl2/pbes/src/permutation.rs | 20 +++++++++----- tools/mcrl2/pbes/src/symmetry.rs | 41 +++++++++++++++-------------- 2 files changed, 34 insertions(+), 27 deletions(-) diff --git a/tools/mcrl2/pbes/src/permutation.rs b/tools/mcrl2/pbes/src/permutation.rs index 0bf494bd..c5750dc8 100644 --- a/tools/mcrl2/pbes/src/permutation.rs +++ b/tools/mcrl2/pbes/src/permutation.rs @@ -25,10 +25,7 @@ impl Permutation { // Sort by domain for deterministic representation. mapping.sort_unstable_by_key(|(d, _)| *d); - debug_assert!( - mapping.iter().is_sorted(), - "Mapping should be sorted by domain." - ); + debug_assert!(mapping.iter().is_sorted(), "Mapping should be sorted by domain."); debug_assert!( mapping.iter().all(|(from, to)| from != to), "Mapping should not contain identity mappings." @@ -285,7 +282,8 @@ pub fn permutation_group_size(n: usize) -> usize { mod tests { use merc_utilities::random_test; use rand::Rng; - use rand::seq::{IteratorRandom, SliceRandom}; + use rand::seq::IteratorRandom; + use rand::seq::SliceRandom; use super::*; @@ -344,7 +342,11 @@ mod tests { let cycle_notation = permutation.to_string(); let parsed_permutation = Permutation::from_cycle_notation(&cycle_notation).unwrap(); - assert_eq!(permutation, parsed_permutation, "Failed on permutation {:?}", permutation); + assert_eq!( + permutation, parsed_permutation, + "Failed on permutation {:?}", + permutation + ); }) } @@ -369,7 +371,11 @@ mod tests { let mapping_notation = format!("{:?}", permutation); let parsed_permutation = Permutation::from_mapping_notation(&mapping_notation).unwrap(); - assert_eq!(permutation, parsed_permutation, "Failed on permutation {:?}", permutation); + assert_eq!( + permutation, parsed_permutation, + "Failed on permutation {:?}", + permutation + ); }) } } diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index fff8509f..8d4d6d15 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -67,7 +67,7 @@ impl SymmetryAlgorithm { info!("==== SRF PBES ===="); info!("{}", srf.to_pbes()); } - + let parameters = if let Some(equation) = srf.equations().first() { equation.variable().parameters().to_vec() } else { @@ -286,7 +286,8 @@ impl SymmetryAlgorithm { |lhs, rhs| lhs.sort() == rhs.sort(), ) } else { - let groups: Vec<&DataVariable> = self.parameters + let groups: Vec<&DataVariable> = self + .parameters .iter() .enumerate() .filter_map(|(index, param)| { @@ -326,10 +327,7 @@ impl SymmetryAlgorithm { debug!( "Parameter {} is updated with expressions: {}", param.name(), - parameter_updates[index] - .iter() - .map(|expr| expr.to_string()) - .join(", ") + parameter_updates[index].iter().map(|expr| expr.to_string()).join(", ") ); } @@ -350,7 +348,8 @@ impl SymmetryAlgorithm { // For progress messages keep track of the number of permutations we need to check. let mut number_of_permutations = 1usize; - let mut all_data_groups: Box> = Box::new(iter::empty()); // Default value is overwritten in first iteration. + let mut all_data_groups: Box> = + Box::new(iter::once(Permutation::from_mapping(Vec::new()))); // Default value is overwritten in first iteration. for group in data_parameter_partition { // Determine the indices of these parameters. let parameter_indices: Vec = group @@ -358,10 +357,7 @@ impl SymmetryAlgorithm { .map(|param| self.parameters.iter().position(|p| p.name() == param.name()).unwrap()) .collect(); - info!( - "Data parameters group: {:?}, indices: {:?}", - group, parameter_indices - ); + info!("Data parameters group: {:?}, indices: {:?}", group, parameter_indices); // Compute the product of the current data group with the already concatenated ones. let number_of_parametes = parameter_indices.len(); @@ -733,9 +729,13 @@ fn replace_variables_by_omega(expression: &DataExpression) -> DataExpression { // Identifier ATerm::constant(&Symbol::new("omega", 0)), // Sort - ATerm::with_args(&Symbol::new("SortId", 1), &[ATerm::constant(&Symbol::new("@NoValue", 0))]), + ATerm::with_args( + &Symbol::new("SortId", 1), + &[ATerm::constant(&Symbol::new("@NoValue", 0))], + ), // Index - ATermInt::with_value(0).into()], + ATermInt::with_value(0).into(), + ], )); let sigma = variables @@ -753,17 +753,18 @@ const UNDEFINED_VERTEX: usize = usize::MAX; fn variable_index(cfg: &ControlFlowGraph) -> usize { // Check that all the vertices have the same variable assigned for consistency cfg.vertices().iter().for_each(|v| { - if v.index() != UNDEFINED_VERTEX && v.index() - != cfg - .vertices() - .first() - .expect("There is at least one vertex in a CFG") - .index() + if v.index() != UNDEFINED_VERTEX + && v.index() + != cfg + .vertices() + .first() + .expect("There is at least one vertex in a CFG") + .index() { panic!("Inconsistent variable indices in control flow graph."); } }); - + if let Some(v) = cfg.vertices().iter().find(|v| v.index() != UNDEFINED_VERTEX) { // Return the first non-undefined index return v.index(); From 91056a94e5e46b764faadecaa59ddf12f4edb2f0 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 26 Jan 2026 11:51:50 +0100 Subject: [PATCH 40/40] Deal with the case where the first vertex is undefined. --- tools/mcrl2/pbes/src/symmetry.rs | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 8d4d6d15..aba1b19d 100644 --- a/tools/mcrl2/pbes/src/symmetry.rs +++ b/tools/mcrl2/pbes/src/symmetry.rs @@ -751,26 +751,22 @@ const UNDEFINED_VERTEX: usize = usize::MAX; /// Returns the index of the variable that the control flow graph considers fn variable_index(cfg: &ControlFlowGraph) -> usize { + // Find the first defined index + let defined_index = cfg.vertices().iter().find(|v| v.index() != UNDEFINED_VERTEX) + .expect("Control flow graph should have defined variable index.") + .index(); + // Check that all the vertices have the same variable assigned for consistency cfg.vertices().iter().for_each(|v| { if v.index() != UNDEFINED_VERTEX && v.index() - != cfg - .vertices() - .first() - .expect("There is at least one vertex in a CFG") - .index() + != defined_index { - panic!("Inconsistent variable indices in control flow graph."); + panic!("Inconsistent variable index {} in control flow graph.", v.index()); } }); - - if let Some(v) = cfg.vertices().iter().find(|v| v.index() != UNDEFINED_VERTEX) { - // Return the first non-undefined index - return v.index(); - } - - panic!("No variable found in control flow graph."); + + return defined_index; } /// Applies the given permutation to the given expression.