Added a graph based symmetry variant - #128
Open
mlaveaux wants to merge 28 commits into
Open
Conversation
There was a problem hiding this comment.
Pull request overview
This PR adds a new graph-based symmetry detection variant for the PBES toolchain by constructing a Symmetry Detection Graph (SDG) and invoking GAP to compute automorphisms, alongside supporting API and workspace updates.
Changes:
- Introduces a
graph-symmetrysubcommand for PBES that builds/exports the SDG (DOT/graph6) and computes symmetry generators via GAP. - Extends the
mcrl2Rust wrapper with direct PBES equation access, in-place parameter unification, and new traversal utilities used by SDG construction. - Performs workspace-wide maintenance updates (explicit
[[bin]]targets, lint configuration propagation, and additional public re-exports).
Reviewed changes
Copilot reviewed 21 out of 22 changed files in this pull request and generated 6 comments.
Show a summary per file
| File | Description |
|---|---|
| tools/vpg/Cargo.toml | Adds an explicit merc-vpg binary target and disables rustdoc to avoid output name collisions. |
| tools/mcrl2/pbes/src/main.rs | Adds the graph-symmetry CLI subcommand and command handler wiring. |
| tools/mcrl2/pbes/src/graph_symmetry.rs | New SDG construction + GAP integration implementation, including DOT/graph6 export and tests. |
| tools/mcrl2/pbes/README.md | Documents graph-symmetry usage and external dependencies (GAP + Digraphs, Graphviz). |
| tools/mcrl2/pbes/Cargo.toml | Adds dependencies needed for SDG building/export and process invocation (e.g., petgraph/duct/which). |
| tools/mcrl2/crates/mcrl2/src/visitor.rs | Adds flatten_associative and new context-threading visitors for data/PBES expressions. |
| tools/mcrl2/crates/mcrl2/src/pbes.rs | Adds Pbes::unify_parameters and access to PBES equations without SRF conversion. |
| tools/mcrl2/crates/mcrl2/src/pbes_expression.rs | Exposes bound-variable lists on forall/exists PBES nodes. |
| tools/mcrl2/Cargo.toml | Adds workspace deps (petgraph/which), updates mcrl2-sys rev, and tweaks dev patch comments. |
| tools/mcrl2/Cargo.lock | Lockfile updates for new/updated dependencies (petgraph/which/foldhash/windows-sys, etc.). |
| tools/lts/Cargo.toml | Adds an explicit merc-lts binary target and disables rustdoc to avoid output name collisions. |
| crates/vpg/Cargo.toml | Enables workspace lint inheritance for the crate. |
| crates/unsafety/Cargo.toml | Adjusts lint configuration and allows rustdoc private_intra_doc_links. |
| crates/tools/src/lib.rs | Exposes Console from the tools crate API surface. |
| crates/symbolic/src/lib.rs | Adds additional public re-exports for symbolic types/utilities. |
| crates/symbolic/Cargo.toml | Enables workspace lint inheritance for the crate. |
| crates/sharedmutex/src/lib.rs | Re-exports additional guard types publicly and adjusts crate root exports. |
| crates/sabre/src/lib.rs | Re-exports RewritingStatistics. |
| crates/lts/src/io.rs | Fixes an intra-doc link path in documentation. |
| crates/lts/Cargo.toml | Enables workspace lint inheritance for the crate. |
| crates/aterm/Cargo.toml | Enables workspace lint inheritance for the crate. |
| Cargo.toml | Adds workspace rustdoc lint configuration (private_intra_doc_links = "allow"). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+1191
to
+1198
| let images: Vec<usize> = line | ||
| .split_whitespace() | ||
| .map(|s| { | ||
| s.parse::<usize>() | ||
| .map(|v| v - 1) // 1-indexed → 0-indexed | ||
| .map_err(|_| MercError::from(format!("invalid image '{}' on generator line {}", s, line_no))) | ||
| }) | ||
| .collect::<Result<_, _>>()?; |
Comment on lines
+659
to
+660
| } else if is_where_clause(&r) { | ||
| todo!("where clauses are not yet supported by the symmetry detection graph construction") |
…Also added tests.
…to be in normal form.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This pull request is to ensure that tests are being executed.