Convert symbolic LTS using LDDs to a BDD based representation #66

mlaveaux · 2026-01-20T13:30:34Z

Also started with the signature based strong symbolic bisimulation. This is not yet working correctly, and the quotient is also missing.

Moved pest_consume to a fork of the original repository, this adds traceability to where 3rd-party dependencies come from, and removed external code from this repo.
Move the 3rd party mCRL2 code to its own mcrl2-sys repository. However, it seems that cargo might not work ideal with submodules inside so perhaps this should not be done. Or we can add mcrl2-sys as a submodule itself.
Renamed some features for consistency.

Copilot

Pull request overview

This pull request converts symbolic LTS representation from LDDs to BDDs and begins implementing signature-based strong symbolic bisimulation. The PR also reorganizes third-party dependencies by moving pest_consume and mcrl2-sys to external GitHub repositories.

Changes:

Adds BDD-based symbolic LTS representation and conversion from LDD format
Implements initial signature refinement algorithm (incomplete)
Moves third-party code (pest_consume, mcrl2-sys) to separate repositories
Adds new CLI commands to merc-sym tool for symbolic LTS operations
Renames mCRL2 features for consistency

Reviewed changes

Copilot reviewed 58 out of 62 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
tools/sym/src/main.rs	Adds new CLI interface with commands for info, explore, reorder, convert, and reduce operations on symbolic LTS
crates/symbolic/src/symbolic_lts_bdd.rs	New module implementing BDD-based symbolic LTS representation with conversion from LDD format
crates/symbolic/src/sigref.rs	New module for signature refinement algorithm (incomplete implementation)
crates/symbolic/src/ldd_to_bdd.rs	Refactors LDD to BDD conversion to use explicit variable mapping instead of auto-generated variables
Cargo.toml	Updates dependencies to use external repositories for pest_consume and mcrl2-sys
.gitmodules	Removes submodules for mCRL2, boost, and cpptrace (moved to mcrl2-sys repo)
3rd-party/*	Removes vendored pest_consume and mCRL2-related code
tools/mcrl2/*	Removes mcrl2-sys crate (moved to separate repository)

crates/symbolic/src/sigref.rs

crates/symbolic/src/symbolic_lts_bdd.rs

tools/sym/src/main.rs

Copilot · 2026-01-20T13:38:15Z

tools/sym/src/main.rs

+    /// Sets the input symbolic LTS format.
+    #[arg(long)]
+    format: Option<LtsFormat>,


The format argument expects SymFormat but the help text says "Sets the input symbolic LTS format", yet the type should be LtsFormat based on the struct name ReduceArgs and the context. This type mismatch will cause compilation errors or incorrect behavior.

…mand to merc-sym.

Also take cases where there are fixpoint but it is not the first one, such as "<true> nu X ..."

…different levels of the partition and the signature. This was unclear from the pseudocode.

…wice as slow with linking as thin LTO. This is 5 minutes in total on a full rebuild for the GUI tools, and is now 2,5 minutes.

* It seems that rusty file dialog has been rewritten to drop about 200 dependencies, so that is nice.

…bdd.

… the miri feature.

Copilot

Pull request overview

Copilot reviewed 77 out of 83 changed files in this pull request and generated 8 comments.

Copilot · 2026-01-24T20:54:25Z

crates/symbolic/src/ldd_to_bdd.rs

            let resulting_ldd = bdd_to_ldd(&mut storage, &manager_ref, &bdd, &bits_dd, 0, 0).unwrap();

            println!("resulting LDD: {}", LddDisplay::new(&storage, &resulting_ldd));
-            assert_eq!(ldd, resulting_ldd, "Converted LDD does not match original");
+            // assert_eq!(ldd, resulting_ldd, "Converted LDD does not match original");
        });


The core correctness assertion in test_random_ldd_to_bdd is commented out, which means this test no longer verifies the LDD↔BDD roundtrip. This likely hides a real regression in ldd_to_bdd/bdd_to_ldd. Please fix the conversion logic so the roundtrip holds again and re-enable the assertion.

crates/symbolic/src/reachability_bdd.rs

crates/syntax/src/visitor.rs

tools/mcrl2/crates/mcrl2/Cargo.toml

crates/unsafety/Cargo.toml

tools/sym/src/main.rs

Copilot · 2026-01-24T20:54:27Z

crates/symbolic/src/ldd_to_bdd.rs

 /// Converts an LDD representing a set of vectors into a BDD representing the
-/// same set by bitblasting the vector elements.
-pub fn ldd_to_bdd_simple(
-    storage: &mut Storage,
-    manager_ref: &BDDManagerRef,
-    ldd: &LddRef<'_>,
-) -> Result<BDDFunction, MercError> {
-    let highest = compute_highest(storage, ldd);
-    let bits = compute_bits(&highest);
-    let bits_dd = merc_ldd::singleton(storage, &bits);
-
-    ldd_to_bdd(storage, manager_ref, ldd, &bits_dd, 0)
-}
-
-/// Converts an LDD representing a set of vectors into a BDD representing the
-/// same set by bitblasting the vector elements.
+/// same set by bitblasting the vector elements using the given variables as bits.
 ///
 /// # Details
 ///


The ldd_to_bdd doc comment is now out of sync with the function signature: it still describes a first_variable parameter and implies consecutive BDD layers, but the API now takes an explicit vars: &[VarNo] mapping. Please update the comment to match the new contract (and remove first_variable references).

mlaveaux self-assigned this Jan 20, 2026

mlaveaux added the enhancement New feature or request label Jan 20, 2026

Copilot AI review requested due to automatic review settings January 20, 2026 13:30

Copilot started reviewing on behalf of mlaveaux January 20, 2026 13:31 View session

Copilot AI reviewed Jan 20, 2026

View reviewed changes

mlaveaux added 25 commits January 24, 2026 19:08

Mention the kahypar feature

e2c1ad0

Mention merc-sym in the changelog

a940622

Removed create_variables helper function

d730807

Made it possible to pass the variables used for the bits in ldd_to_bdd

1b53f53

Fixed typo

de7b0e5

Smaller changes

e477088

Moved the pest_consume vendored code to a separate repository

1fc443e

Started a conversion from an LDD to BDD symbolic LTS.

112f989

Started with the signature refinement, and added it as the reduce com…

0590430

…mand to merc-sym.

Moved from mcrl2-sys to the separate git repository

2cc271b

Add the cpptrace feature

97040a2

Fixed adding the outermost operator by avoiding duplicates.

48a670b

Also take cases where there are fixpoint but it is not the first one, such as "<true> nu X ..."

Fixed typo

4da2b2d

Fixed the bit assignment for the short transition relations

0dfb935

Switched to proper data expressions for read symbolic LTSs

a5e9cac

Added oxidd-dump for visualisation, also using oxidd-vis

6e00dbd

Fixed printing of terms.

c5988da

Added a visitor for regular formulas.

e42dc12

Implemented the refine operation for signature refinement.

d2d5b07

Fixed an issue with the refine operation, applying the result to two …

f491bb3

…different levels of the partition and the signature. This was unclear from the pseudocode.

Made the way help is added consistent

0ac8185

Switched to doc comments for all CLI argument help text

9d2cab0

We might want to introduce a package profile, but fat LTO is almost t…

b7f321c

…wice as slow with linking as thin LTO. This is 5 minutes in total on a full rebuild for the GUI tools, and is now 2,5 minutes.

Updated dependencies.

58f4518

* It seems that rusty file dialog has been rewritten to drop about 200 dependencies, so that is nice.

Renamed to LtsMultiAction to differentiate from the AST MultiAction

fdf39b7

mlaveaux added 6 commits January 24, 2026 19:11

Made consistent

32486e4

Added a BDD based reachability algorithm that can be used with --use-…

916454d

…bdd.

Deal with the empty relation case

8b0adea

Fixed compilation issues.

58b2871

Fixed some warnings, removed unused tests.

731a11d

Simplified various cargo features, added metrics for oxidd and remove…

bd1aa0d

… the miri feature.

mlaveaux force-pushed the feature/symbolic_lts_bdd branch from 3f5ff5a to bd1aa0d Compare January 24, 2026 20:44

mlaveaux requested a review from Copilot January 24, 2026 20:44

Copilot started reviewing on behalf of mlaveaux January 24, 2026 20:44 View session

Copilot AI reviewed Jan 24, 2026

View reviewed changes

mlaveaux added 5 commits January 24, 2026 22:13

Print the order in a way that lpsreach can consume.

3f8e33b

wgpu requires rustc 1.92.0

1b74bf4

Fixed several suggestions

97f6a42

Tried to fix this file.

07c644c

Added random symbolic LTSs, and a test for reachability.

0b5f1d7

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Convert symbolic LTS using LDDs to a BDD based representation #66

Convert symbolic LTS using LDDs to a BDD based representation #66

Uh oh!

mlaveaux commented Jan 20, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI Jan 20, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Jan 24, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI Jan 24, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Convert symbolic LTS using LDDs to a BDD based representation #66

Are you sure you want to change the base?

Convert symbolic LTS using LDDs to a BDD based representation #66

Uh oh!

Conversation

mlaveaux commented Jan 20, 2026

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!

Copilot AI Jan 20, 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 24, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI Jan 24, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant