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 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-macros/src/mcrl2_derive_terms.rs b/tools/mcrl2/crates/mcrl2-macros/src/mcrl2_derive_terms.rs index c8240b85..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!( @@ -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() } @@ -114,12 +121,25 @@ 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> } 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() } @@ -171,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-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/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/cpp/data.cpp b/tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp new file mode 100644 index 00000000..2d6ad8d0 --- /dev/null +++ b/tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp @@ -0,0 +1,31 @@ +#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" + +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( + 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..0e871812 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,60 +49,73 @@ 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); + +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); diff --git a/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h b/tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h index 50f2821c..969d400c 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; @@ -63,6 +64,18 @@ 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 +bool mcrl2_pbes_is_well_typed(const pbes& pbesspec) +{ + return pbesspec.is_well_typed(); +} + inline rust::String mcrl2_pbes_to_string(const pbes& pbesspec) { @@ -72,10 +85,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(); } @@ -85,7 +99,7 @@ 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 @@ -309,13 +323,71 @@ 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); 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/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-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-sys/src/pbes.rs b/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs index b0051c72..75e60340 100644 --- a/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2-sys/src/pbes.rs @@ -29,6 +29,12 @@ pub mod ffi { /// Loads a PBES from a string. fn mcrl2_load_pbes_from_text(input: &str) -> Result>; + /// 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; @@ -69,6 +75,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 +141,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; @@ -154,6 +159,15 @@ pub mod ffi { pi: &Vec, ) -> UniquePtr; - fn mcrl2_pbes_expression_to_string(expression: &aterm) -> String; + 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/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/crates/mcrl2/src/atermpp/aterm.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm.rs index bd3fd452..cd6fa221 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; @@ -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_int.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs new file mode 100644 index 00000000..8577d2ad --- /dev/null +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs @@ -0,0 +1,60 @@ +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 { + mcrl2_aterm_is_int(term.get()) +} + +#[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; + + /// Represents an atermpp::aterm_string from the mCRL2 toolset. + #[mcrl2_term(is_aterm_int)] + pub struct ATermInt { + term: ATerm, + } + + 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. + 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/aterm_list.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_list.rs index ee8d2e91..f225e064 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,13 +42,22 @@ 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. 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 { @@ -100,12 +112,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 +130,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, } @@ -151,3 +163,60 @@ 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 ATermListRef<'_, T> { + /// Returns true iff the list is empty. + 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> { + 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); + ATermListRef { + term: value, + _marker: PhantomData, + } + } +} + +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) +// } +// } +// } diff --git a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs index 6c40bce9..889b7629 100644 --- a/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs +++ b/tools/mcrl2/crates/mcrl2/src/atermpp/aterm_string.rs @@ -1,34 +1,49 @@ 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; + + 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, } - /// 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() + 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() + } } } -impl fmt::Debug for ATermString { +pub use inner::*; + +impl fmt::Display for ATermString { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "{}", self.str()) } } -impl fmt::Display for ATermString { +impl fmt::Display for ATermStringRef<'_> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "{}", self.str()) } } + 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::*; 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/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/crates/mcrl2/src/data_expression.rs b/tools/mcrl2/crates/mcrl2/src/data_expression.rs index 54c46862..3ba5a709 100644 --- a/tools/mcrl2/crates/mcrl2/src/data_expression.rs +++ b/tools/mcrl2/crates/mcrl2/src/data_expression.rs @@ -1,3 +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; @@ -6,10 +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_macros::mcrl2_derive_terms; +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. @@ -69,25 +72,19 @@ 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; + use crate::ATermIntRef; use crate::ATermRef; - use crate::ATermString; + use crate::ATermStringRef; 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 +105,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 @@ -147,9 +138,9 @@ mod inner { /// - application f(t_0, ..., t_n) -> [t_0, ..., t_n] pub fn data_sort(&self) -> SortExpression { if is_function_symbol(&self.term) { - DataFunctionSymbolRef::from(self.term.copy()).sort().protect() + 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); } @@ -170,7 +161,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,21 +175,14 @@ 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()) + 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() } } @@ -215,13 +199,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() @@ -273,11 +250,9 @@ mod inner { } 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 } + /// Returns the body of the abstraction. + pub fn body(&self) -> DataExpressionRef<'_> { + self.term.arg(1).into() } } @@ -288,13 +263,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 +292,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 +307,231 @@ 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 + ATermIntRef::from(self.term.copy()).value() } } - 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, + } + + 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 { + pub term: ATerm, + } + } 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 { - 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/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 3c686508..a7026365 100644 --- a/tools/mcrl2/crates/mcrl2/src/pbes.rs +++ b/tools/mcrl2/crates/mcrl2/src/pbes.rs @@ -47,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 @@ -84,6 +85,17 @@ 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()); + } + + /// 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 } } @@ -411,7 +423,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() ) @@ -451,27 +463,8 @@ 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::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 { +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() @@ -488,7 +481,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/pbes_expression.rs b/tools/mcrl2/crates/mcrl2/src/pbes_expression.rs new file mode 100644 index 00000000..dc449b9a --- /dev/null +++ b/tools/mcrl2/crates/mcrl2/src/pbes_expression.rs @@ -0,0 +1,352 @@ +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; + +/// 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()) +} + +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::ATermListRef; + use crate::ATermRef; + use crate::ATermStringRef; + use crate::DataExpressionRef; + 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, + } + + 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::*; + +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()) + } +} diff --git a/tools/mcrl2/crates/mcrl2/src/visitor.rs b/tools/mcrl2/crates/mcrl2/src/visitor.rs index f44216e4..9318de3b 100644 --- a/tools/mcrl2/crates/mcrl2/src/visitor.rs +++ b/tools/mcrl2/crates/mcrl2/src/visitor.rs @@ -1,70 +1,230 @@ -use crate::DataAbstraction; -use crate::DataApplication; +use crate::DataAbstractionRef; +use crate::DataApplicationRef; use crate::DataExpression; -use crate::DataFunctionSymbol; +use crate::DataExpressionRef; +use crate::DataFunctionSymbolRef; +use crate::DataMachineNumberRef; +use crate::DataUntypedIdentifierRef; use crate::DataVariable; +use crate::DataVariableRef; +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; 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<'_>) -> Option { + None } - fn visit_application(&mut self, _app: &DataApplication) -> DataExpression { - unimplemented!() + fn visit_application(&mut self, appl: &DataApplicationRef<'_>) -> Option { + let _head = self.visit(&appl.data_function_symbol().into()); + + appl.data_arguments().for_each(|arg| { + self.visit(&arg.into()); + }); + + None + } + + fn visit_abstraction(&mut self, abstraction: &DataAbstractionRef<'_>) -> Option { + let _body = self.visit(&abstraction.body()); + None + } + + fn visit_function_symbol(&mut self, _function_symbol: &DataFunctionSymbolRef<'_>) -> Option { + None } - fn visit_abstraction(&mut self, _abs: &DataAbstraction) -> DataExpression { - unimplemented!() + fn visit_where_clause(&mut self, where_: &DataWhereClauseRef<'_>) -> Option { + let _body = self.visit(&where_.body()); + None } - fn visit_function_symbol(&mut self, _fs: &DataFunctionSymbol) -> DataExpression { - unimplemented!() + fn visit_machine_number(&mut self, _number: &DataMachineNumberRef<'_>) -> Option { + None } - fn visit(&mut self, expr: &DataExpression) -> DataExpression { + fn visit_untyped_identifier(&mut self, _identifier: &DataUntypedIdentifierRef<'_>) -> Option { + None + } + + fn visit(&mut self, expr: &DataExpressionRef<'_>) -> Option { 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<'_>, + ) -> Option { + None + } + + fn visit_not(&mut self, not: &PbesNotRef<'_>) -> Option { + self.visit(¬.body()); + None + } + + fn visit_and(&mut self, and: &PbesAndRef<'_>) -> Option { + self.visit(&and.lhs()); + self.visit(&and.rhs()); + None + } + + fn visit_or(&mut self, or: &PbesOrRef<'_>) -> Option { + self.visit(&or.lhs()); + self.visit(&or.rhs()); + None + } + + fn visit_imp(&mut self, imp: &PbesImpRef<'_>) -> Option { + self.visit(&imp.lhs()); + self.visit(&imp.rhs()); + None + } + + fn visit_forall(&mut self, forall: &PbesForallRef<'_>) -> Option { + self.visit(&forall.body()); + None + } + + fn visit_exists(&mut self, exists: &PbesExistsRef<'_>) -> Option { + self.visit(&exists.body()); + None + } + + fn visit(&mut self, expr: &PbesExpressionRef<'_>) -> Option { + 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, +/// +/// 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, +{ + 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<'_>) -> 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. +pub fn pbes_expression_pvi(expr: &PbesExpressionRef<'_>) -> Vec { + let mut result = Vec::new(); + + /// Local struct that is used to collect PVI occurrences. + struct PviOccurrences<'a> { + result: &'a mut Vec, + } + + impl PbesExpressionVisitor for PviOccurrences<'_> { + fn visit_propositional_variable_instantiation( + &mut self, + inst: &PbesPropositionalVariableInstantiationRef<'_>, + ) -> Option { + // Found a propositional variable instantiation, return true. + self.result + .push(PbesPropositionalVariableInstantiation::from(inst.protect())); + None + } + } + + let mut occurrences = PviOccurrences { result: &mut result }; + occurrences.visit(expr); + result +} + +/// Returns all the variables occurring in the given data expression. +pub fn data_expression_variables(expr: &DataExpressionRef<'_>) -> 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 + } + } + + let mut occurrences = VariableOccurrences { result: &mut result }; + occurrences.visit(expr); + result } 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/main.rs b/tools/mcrl2/pbes/src/main.rs index 353ecace..95643ccb 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; @@ -58,15 +59,29 @@ 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, - #[arg( - long, - default_value_t = false, - help = "Partition data parameters into their sorts before considering their permutation groups" - )] + /// 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, + + /// 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, + + /// Print the SRF representation of the PBES. + #[arg(long, default_value_t = false)] + print_srf: bool, } fn main() -> Result { @@ -95,20 +110,46 @@ 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 = Permutation::from_input(permutation)?; + 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: {x}"); + return Ok(ExitCode::FAILURE); + } + + info!("Checking permutation: {}", pi); if algorithm.check_symmetry(&pi) { println!("true"); } else { println!("false"); } } else { - for candidate in algorithm.candidates(args.partition_data_sorts) { - info!("Found candidate: {}", candidate); + 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) { - info!("Found symmetry: {}", candidate); + if args.mapping_notation { + info!("Found symmetry: {:?}", candidate); + } else { + info!("Found symmetry: {}", candidate); + } + + if !args.all_symmetries { + // Only search for the first symmetry + info!("Stopping search after first non-trivial symmetry."); + break; + } } } } diff --git a/tools/mcrl2/pbes/src/permutation.rs b/tools/mcrl2/pbes/src/permutation.rs index bb04ff83..c5750dc8 100644 --- a/tools/mcrl2/pbes/src/permutation.rs +++ b/tools/mcrl2/pbes/src/permutation.rs @@ -17,28 +17,29 @@ 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().duplicates().count() == 0, "Mapping should not contain duplicate domain entries."); + 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." + ); + 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 = @@ -80,9 +81,58 @@ 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)) } + /// 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)); + } + } + + if !is_valid_permutation(&mapping) { + return Err(MercError::from("Input mapping is not a valid permutation.")); + } + + Ok(Permutation::from_mapping(mapping)) + } + /// Construct a new permutation by concatenating two (disjoint) permutations. pub fn concat(self, other: &Permutation) -> Permutation { debug_assert!( @@ -109,12 +159,32 @@ 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) } } +/// Checks whether the mapping represents a valid permutation +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 @@ -124,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. @@ -193,9 +263,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) }) } @@ -207,23 +280,36 @@ pub fn permutation_group_size(n: usize) -> usize { #[cfg(test)] mod tests { + use merc_utilities::random_test; + use rand::Rng; + use rand::seq::IteratorRandom; + use rand::seq::SliceRandom; + use super::*; #[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]; @@ -234,4 +320,62 @@ mod tests { assert_eq!(permutations.len(), permutation_group_size(indices.len())); } + + #[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 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_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 + ); + }) + } } diff --git a/tools/mcrl2/pbes/src/symmetry.rs b/tools/mcrl2/pbes/src/symmetry.rs index 551c46b9..aba1b19d 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; @@ -9,6 +10,8 @@ use log::debug; use log::info; use log::trace; +use mcrl2::ATerm; +use mcrl2::ATermInt; use mcrl2::ATermString; use mcrl2::ControlFlowGraph; use mcrl2::ControlFlowGraphVertex; @@ -19,10 +22,14 @@ use mcrl2::PbesExpression; use mcrl2::PbesStategraph; use mcrl2::SrfPbes; use mcrl2::StategraphEquation; -use mcrl2::replace_propositional_variables; -use mcrl2::replace_variables; -use merc_io::TimeProgress; +use mcrl2::Symbol; +use mcrl2::data_expression_variables; +use mcrl2::pbes_expression_pvi; +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; use crate::clone_iterator::CloneIterator; @@ -32,25 +39,23 @@ 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. + /// The indices of all control flow parameters in the PBES. + 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, 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 { @@ -70,12 +75,15 @@ impl SymmetryAlgorithm { Vec::new() }; - info!( - "Unified parameters: {:?}", - parameters.iter().map(|p| (p.name(), p.sort())).format(", ") - ); + info!("Unified parameters: {}", parameters.iter().format(", ")); + + 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)? + }; - let state_graph = PbesStategraph::run(&srf.to_pbes())?; let all_control_flow_parameters = state_graph .control_flow_graphs() .iter() @@ -100,7 +108,13 @@ 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 { @@ -118,7 +132,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); + let (number_of_permutations, candidates) = + self.clique_candidates(clique.clone(), partition_data_sorts, partition_data_updates); info!( "Maximum number of permutations for clique {:?}: {}", clique, @@ -136,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!( @@ -147,6 +163,34 @@ 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() { @@ -215,6 +259,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 @@ -227,78 +272,108 @@ 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 = { - let mut result: Vec> = Vec::new(); - - for (index, param) in self.parameters.iter().enumerate() { + 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. - continue; + None + } else { + Some(param) } + }), + |lhs, rhs| lhs.sort() == rhs.sort(), + ) + } else { + 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 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 + let data_parameter_partition = if partition_data_updates { + let mut parameter_updates = vec![HashSet::new(); self.parameters.len()]; + + // 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 pvi.arguments().protect().cast::().iter().enumerate() { + parameter_updates[index].insert(replace_variables_by_omega(¶m)); } - }) { - group.push(param.clone()); - } else { - result.push(vec![param.clone()]); } } - result - }; - - 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 + 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(", ") ); + } - // 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 *= permutation_group_size(number_of_parametes); + 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()] + })); } - (number_of_permutations, all_data_groups) + update_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::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 + .iter() + .map(|param| self.parameters.iter().position(|p| p.name() == param.name()).unwrap()) .collect(); - info!("All data parameter indices: {:?}", parameter_indices); + info!("Data parameters group: {:?}, 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()); @@ -613,27 +688,85 @@ 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 { + // 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) + } else { + false + } + }) { + // Add to existing group + group.push(element.clone()); + } else { + // Create new group + result.push(vec![element.clone()]); + } + } + + result +} + +/// Replaces all variables in the expression by omega. +fn replace_variables_by_omega(expression: &DataExpression) -> DataExpression { + let variables = data_expression_variables(&expression.copy()); + + // Generate an omega variable. + let omega = DataExpression::from(ATerm::with_args( + &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 + .iter() + .map(|var| (var.clone().into(), omega.clone())) + .collect::>(); + + 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 { + // 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() - != cfg - .vertices() - .first() - .expect("There is at least one vertex in a CFG") - .index() + if v.index() != UNDEFINED_VERTEX + && v.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().next() { - // Simply return the index of the variable - return v.index(); - } - - panic!("No variable found in control flow graph."); + + return defined_index; } /// Applies the given permutation to the given expression. @@ -652,10 +785,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)] @@ -689,18 +822,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) + .candidates(false, 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()); @@ -713,9 +853,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" ); }