Continued the static analysis for pbessymmetry #48

mlaveaux · 2025-12-21T16:06:20Z

Reopened the pull request to run tests, now as part of a fork since the main repository has been moved.

Tasks:

Added PBES expressions and DATA expressions.
Added visitors.
Parse and print permutations in cycle notation.
Added various tests.
Add the partitioning based on updates
Remove undefined vertices from the CFGs

Copilot

Pull request overview

This PR continues static analysis work for the pbessymmetry tool by implementing cycle notation parsing for permutations and adding validation logic. The main accomplishment is the completion of parsing permutations in cycle notation (one of the two tasks in the PR description).

Added cycle notation parsing for permutations (e.g., "(0 2 1)(3 4)")
Introduced permutation validation to ensure control flow parameters are correctly mapped
Fixed a critical bug in C++ FFI code where mcrl2_srf_summand_condition was incorrectly returning the summand variable instead of the condition

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 6 comments.

Show a summary per file

File	Description
`tools/mcrl2/pbes/src/symmetry.rs`	Added documentation comments to struct fields, improved logging output format, and introduced `is_valid_permutation` method to validate permutation constraints
`tools/mcrl2/pbes/src/permutation.rs`	Renamed `from_input` to `from_mapping_notation`, added `from_cycle_notation` parser, added `domain` method, and included test for cycle notation parsing
`tools/mcrl2/pbes/src/main.rs`	Updated CLI arguments, added automatic detection of permutation format (mapping vs cycle notation), and integrated permutation validation
`tools/mcrl2/crates/mcrl2/src/pbes.rs`	Added Display trait for PbesExpression and updated Debug formatting for SrfSummand to use Display instead of Debug
`tools/mcrl2/crates/mcrl2-sys/src/pbes.rs`	Changed FFI signature from `&aterm` to `&_aterm` for consistency with C++ implementation
`tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h`	Fixed critical bug where `mcrl2_srf_summand_condition` returned `summand.variable()` instead of `summand.condition()`, and updated `mcrl2_pbes_expression_to_string` to properly handle `_aterm` references
`.gitmodules`	Updated boost-include-only submodule URL to point to MERCorg fork

tools/mcrl2/pbes/src/symmetry.rs

tools/mcrl2/pbes/src/main.rs

tools/mcrl2/pbes/src/symmetry.rs

Copilot

Pull request overview

Copilot reviewed 7 out of 7 changed files in this pull request and generated 6 comments.

tools/mcrl2/pbes/src/symmetry.rs

tools/mcrl2/pbes/src/main.rs

tools/mcrl2/pbes/src/symmetry.rs

tools/mcrl2/pbes/src/permutation.rs

tools/mcrl2/pbes/src/main.rs

…ing somewhat.

Copilot

Pull request overview

Copilot reviewed 7 out of 7 changed files in this pull request and generated 7 comments.

tools/mcrl2/pbes/src/symmetry.rs

Copilot · 2026-01-05T13:31:57Z

tools/mcrl2/pbes/src/symmetry.rs

+    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(())
+    }


The new is_valid_permutation method lacks test coverage. Consider adding tests to verify the validation logic for both valid and invalid cases, including boundary conditions and control flow parameter constraints.

Copilot · 2026-01-05T13:31:58Z

tools/mcrl2/pbes/src/main.rs

+        default_value_t = false
    )]
-    partition_data_sorts: bool,
+    partition_data_sorts: bool,    


Trailing whitespace detected. Remove the trailing space at the end of this line.

Suggested change

partition_data_sorts: bool,

partition_data_sorts: bool,

Copilot · 2026-01-05T13:31:58Z

tools/mcrl2/pbes/src/symmetry.rs

+    let mut result: Vec<Vec<T>> = Vec::new();
+
+    for element in elements {
+


Unnecessary blank line. Remove this empty line for consistency with the codebase formatting style.

Suggested change

Copilot · 2026-01-05T13:31:58Z

tools/mcrl2/pbes/src/main.rs

    format: Option<PbesFormat>,

-    /// 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.


Documentation comment is slightly inaccurate. The permutation can be in either mapping notation (e.g., [0->2, 1->0]) or cycle notation (e.g., (0 2 1)), not just cycle notation. Consider updating to: "Pass a single permutation in mapping notation [0->2, 1->0] or cycle notation (0 2 1) to check whether it is a symmetry."

Suggested change

/// Pass a single permutation in cycles notation to check whether it is a symmetry.

/// Pass a single permutation in mapping notation [0->2, 1->0] or cycle notation (0 2 1) to check whether it is a symmetry.

Copilot · 2026-01-05T13:31:59Z

tools/mcrl2/pbes/src/permutation.rs

+    pub fn from_cycle_notation(cycle_notation: &str) -> Result<Self, MercError> {
+        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<Vec<usize>, MercError> = cycle_content
+                .split_whitespace()
+                .map(|num_str| {
+                    num_str
+                        .parse::<usize>()
+                        .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))
+    }


Consider adding test coverage for edge cases in from_cycle_notation, such as empty input, single-element cycles, invalid formatting (missing parentheses, invalid numbers), and cycles with duplicate elements.

…ies an option

…pdate expressions.

This reverts commit b5598b7.

Copilot

Pull request overview

Copilot reviewed 27 out of 29 changed files in this pull request and generated 10 comments.

Copilot · 2026-01-14T16:50:06Z

tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs

+        pub fn value(&self) -> u64 {
+            // The Rust::Str should ensure that this is a valid string.
+            0
+        }


The value() method always returns 0 instead of the actual integer value stored in the ATerm. This is a placeholder implementation that needs to be completed. The method should extract the actual value from the underlying C++ aterm_int. Additionally, the comment mentions 'Rust::Str' which is incorrect for an integer value method.

Copilot · 2026-01-14T16:50:06Z

tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs

+    use crate::Todo;
+    use crate::is_aterm_int;
+
+    /// Represents an atermpp::aterm_string from the mCRL2 toolset.


The documentation states this represents an 'aterm_string', but the struct is ATermInt which represents an integer term. The comment should be corrected to 'Represents an atermpp::aterm_int from the mCRL2 toolset.'

Copilot · 2026-01-14T16:50:06Z

tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs

+    }
+
+    impl ATermInt {
+        /// Creates a new ATermInt from the given string value.


The documentation incorrectly states 'from the given string value' when it should be 'from the given integer value' since the parameter is value: u64.

Copilot · 2026-01-14T16:50:07Z

tools/mcrl2/crates/mcrl2/src/atermpp/aterm_int.rs

+            }                     
+        }
+
+        /// Returns the string value.


The documentation incorrectly states 'Returns the string value' when it should be 'Returns the integer value' since the method returns u64.

Copilot · 2026-01-14T16:50:07Z

tools/mcrl2/crates/mcrl2/src/visitor.rs

+/// 
+/// TODO: This is not yet functional, the replacements actually do not work.


The function data_expression_replace_variables has a TODO indicating it is not functional, but it's being exported and potentially used. If this is truly non-functional, consider marking it as #[doc(hidden)] or with a #[deprecated] attribute to prevent its use, or remove it until it's implemented correctly.

Copilot · 2026-01-14T16:50:07Z

tools/mcrl2/crates/mcrl2/src/visitor.rs

+pub fn data_expression_variables(expr: &DataExpressionRef<'_>) -> Vec<DataVariable> {
+    let mut result = Vec::new();
+
+    /// Local struct that is used to collect PVI occurrences.


The comment says 'PVI occurrences' but should be 'variable occurrences' since this is for the VariableOccurrences struct in the data_expression_variables function.

Copilot · 2026-01-14T16:50:07Z

tools/mcrl2/crates/mcrl2/src/visitor.rs

+
+    impl DataExpressionVisitor for VariableOccurrences<'_> {
+        fn visit_variable(&mut self, var: &DataVariableRef<'_>) -> Option<DataExpression> {
+            // Found a propositional variable instantiation, return true.


The comment says 'Found a propositional variable instantiation' but should be 'Found a data variable' since this is in the visit_variable method of VariableOccurrences.

Copilot · 2026-01-14T16:50:08Z

tools/mcrl2/pbes/src/symmetry.rs

-            let all_data_groups =
-                Box::new(permutation_group(parameter_indices.clone())) as Box<dyn CloneIterator<Item = Permutation>>;
+            // Compute the product of the current data group with the already concatenated ones.
+            let number_of_parametes = parameter_indices.len();


Corrected spelling of 'parametes' to 'parameters'.

Copilot · 2026-01-14T16:50:08Z

tools/mcrl2/pbes/src/permutation.rs

 }

+/// Checks whether the mapping represents a valid permutation
+pub fn is_valid_permutation(mapping: &Vec<(usize, usize)>) -> bool {


The parameter type &Vec<T> should be &[T] to accept any slice type. Change &Vec<(usize, usize)> to &[(usize, usize)] for more idiomatic Rust.

Copilot · 2026-01-14T16:50:09Z

tools/mcrl2/crates/mcrl2/src/data_expression.rs

        /// Obtain the underlying value of a machine number.
        pub fn value(&self) -> u64 {
-            0
+            ATermIntRef::from(self.term.copy()).value()


This calls ATermIntRef::value() which is inherited from ATermInt::value() that always returns 0. This will return incorrect values until the value() method in aterm_int.rs is properly implemented.

…e CFG index.

mlaveaux self-assigned this Dec 21, 2025

Copilot AI review requested due to automatic review settings December 21, 2025 16:06

mlaveaux added the enhancement New feature or request label Dec 21, 2025

Copilot started reviewing on behalf of mlaveaux December 21, 2025 16:06 View session

Copilot AI reviewed Dec 21, 2025

View reviewed changes

mlaveaux force-pushed the feature/pbessymmetry branch from f45a124 to 2f6d669 Compare December 24, 2025 18:44

mlaveaux requested a review from Copilot December 24, 2025 18:45

Copilot started reviewing on behalf of mlaveaux December 24, 2025 18:45 View session

Copilot AI reviewed Dec 24, 2025

View reviewed changes

mlaveaux added 4 commits January 4, 2026 21:24

Changed boost-include-only to the upstream directory

0f6bd23

Parse permutations in cycle notation

fbb627e

Allow cycle notation for the now --permutation option. Improved print…

078e714

…ing somewhat.

Fixed several suggestions

07c585a

mlaveaux force-pushed the feature/pbessymmetry branch from 2f6d669 to 07c585a Compare January 4, 2026 20:27

Added a proper partitioning function, also to be used for other filters.

1f5157d

mlaveaux requested a review from Copilot January 5, 2026 13:27

Copilot started reviewing on behalf of mlaveaux January 5, 2026 13:28 View session

Copilot AI reviewed Jan 5, 2026

View reviewed changes

mlaveaux added 12 commits January 6, 2026 21:53

Added the pbes expression variants

cdd965b

Added visitor for the pbes expression

b963dcb

Removed the original PbesExpression

379c2d4

Made ATermString a proper aterm

2a24103

Added new for all terms

b59b400

Added recognizers for al lthe pbes expressions

fa59f07

Added various accessor functions

43a17a3

Added ATermListRef

01a3486

Added better Debug for terms

f4c89c7

Only search the first symmetry, annd instead made finding all symmetr…

731fb27

…ies an option

Added random tests for the cycle notation parsing

e5fc2d3

Added ATermInt for the mcrl2 aterm_int

50b8456

mlaveaux added 18 commits January 8, 2026 15:58

Extended the visitors.

7d1f281

Fixed issue in data expression

6f72972

Fixed the example tests

a071a31

Ignore the identity symmetry

108e97a

Ignore test until it is fixed

633eaf9

Print a message when it was aborted

8028cae

Deal with the undefined vertex in cfgs.

b5598b7

Fixed the random cycle notation test, and added one for mappings as well

9f91162

Started with ATermListRef

3484e43

Added a replace_variables for data expressions.

3130b7b

Added various helper functions.

97583a9

Added missing inline keywords

ac289f2

Added a not yet correct version of partitioning parameters on their u…

ddd67f4

…pdate expressions.

Revert "Deal with the undefined vertex in cfgs."

e5b64fd

This reverts commit b5598b7.

Normalize the PBES after the SRF transformation

555feb0

Avoid adding the identity mappings, and add is_well_typed to PBES.

42e3493

Only compute the CFGs.

9b417aa

Ensure that the omega function symbols are valid data expressions.

975120b

mlaveaux requested a review from Copilot January 14, 2026 16:37

Copilot started reviewing on behalf of mlaveaux January 14, 2026 16:47 View session

Copilot AI reviewed Jan 14, 2026

View reviewed changes

mlaveaux added 5 commits January 19, 2026 16:04

Deal with the question mark vertices by ignoring them when finding th…

f448985

…e CFG index.

Avoid overflow, and deal with the empty partition

c12e6ca

Do not print the identity permutation

cf40f70

Deal with no data parameters by starting with the identity mapping

cc37588

Deal with the case where the first vertex is undefined.

91056a9

		let mut result: Vec<Vec<T>> = Vec::new();

		for element in elements {

	/// Pass a single permutation in cycles notation to check whether it is a symmetry.
	/// Pass a single permutation in mapping notation [0->2, 1->0] or cycle notation (0 2 1) to check whether it is a symmetry.

		///
		/// TODO: This is not yet functional, the replacements actually do not work.

Continued the static analysis for pbessymmetry #48

Are you sure you want to change the base?

Continued the static analysis for pbessymmetry #48

Uh oh!

Conversation

mlaveaux commented Dec 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

Copilot AI Jan 5, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 5, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 5, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 5, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 5, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Copilot AI Jan 14, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 14, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 14, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 14, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 14, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 14, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 14, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 14, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 14, 2026

Choose a reason for hiding this comment

mlaveaux commented Dec 21, 2025 •

edited

Loading