Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
45 commits
Select commit Hold shift + click to select a range
e151d25
Mention the kahypar feature
mlaveaux Jan 17, 2026
e309394
Mention merc-sym in the changelog
mlaveaux Jan 17, 2026
673f678
Removed create_variables helper function
mlaveaux Jan 17, 2026
1d25ad8
Made it possible to pass the variables used for the bits in ldd_to_bdd
mlaveaux Jan 17, 2026
93b5903
Fixed typo
mlaveaux Jan 18, 2026
f0f11b1
Smaller changes
mlaveaux Jan 18, 2026
c1b4fbb
Moved the pest_consume vendored code to a separate repository
mlaveaux Jan 18, 2026
dedd86e
Started a conversion from an LDD to BDD symbolic LTS.
mlaveaux Jan 18, 2026
3168002
Started with the signature refinement, and added it as the reduce com…
mlaveaux Jan 18, 2026
c55919d
Moved from mcrl2-sys to the separate git repository
mlaveaux Jan 18, 2026
8701d09
Add the cpptrace feature
mlaveaux Jan 18, 2026
5caa6c9
Fixed adding the outermost operator by avoiding duplicates.
mlaveaux Jan 20, 2026
92adbae
Fixed typo
mlaveaux Jan 21, 2026
f5ce1fd
Fixed the bit assignment for the short transition relations
mlaveaux Jan 21, 2026
a96b72b
Switched to proper data expressions for read symbolic LTSs
mlaveaux Jan 21, 2026
b6f957e
Added oxidd-dump for visualisation, also using oxidd-vis
mlaveaux Jan 21, 2026
c71b61e
Fixed printing of terms.
mlaveaux Jan 21, 2026
74f78e0
Added a visitor for regular formulas.
mlaveaux Jan 21, 2026
a18859c
Implemented the refine operation for signature refinement.
mlaveaux Jan 21, 2026
783c5c4
Fixed an issue with the refine operation, applying the result to two …
mlaveaux Jan 22, 2026
9e43534
Made the way help is added consistent
mlaveaux Jan 22, 2026
a152736
Switched to doc comments for all CLI argument help text
mlaveaux Jan 23, 2026
2142c50
We might want to introduce a package profile, but fat LTO is almost t…
mlaveaux Jan 23, 2026
d64c800
Updated dependencies.
mlaveaux Jan 23, 2026
791bef8
Renamed to LtsMultiAction to differentiate from the AST MultiAction
mlaveaux Jan 23, 2026
8cbf882
Made consistent
mlaveaux Jan 23, 2026
0555813
Added a BDD based reachability algorithm that can be used with --use-…
mlaveaux Jan 24, 2026
5ae5858
Deal with the empty relation case
mlaveaux Jan 24, 2026
66ffcf8
Fixed compilation issues.
mlaveaux Jan 24, 2026
a829f78
Fixed some warnings, removed unused tests.
mlaveaux Jan 24, 2026
006f2f9
Simplified various cargo features, added metrics for oxidd and remove…
mlaveaux Jan 24, 2026
f36f385
Print the order in a way that lpsreach can consume.
mlaveaux Jan 24, 2026
91ec24d
wgpu requires rustc 1.92.0
mlaveaux Jan 24, 2026
667656f
Fixed several suggestions
mlaveaux Jan 25, 2026
9893d2b
Tried to fix this file.
mlaveaux Jan 25, 2026
478a423
Added random symbolic LTSs, and a test for reachability.
mlaveaux Jan 25, 2026
30f50dd
Optimised the CubeIter to not iterate over irrelevant cubes
mlaveaux Jan 27, 2026
699d04c
Removed pest_consume
mlaveaux Jan 27, 2026
9cfd682
Made printing of the partition more efficient by avoiding allocating …
mlaveaux Jan 27, 2026
73f7402
Made progress on sigref
mlaveaux Jan 27, 2026
abddf2c
Propagate errors in CubeIter, and made CubeIterAll more efficient.
mlaveaux Jan 28, 2026
099e141
Share the target directories to avoid recompiling, and such that carg…
mlaveaux Jan 28, 2026
e3084d9
Optimised CubeIterAll, added various trace logging and "fixed" the si…
mlaveaux Jan 28, 2026
e1eb04f
Smaller changes, updated README
mlaveaux Jan 29, 2026
313677a
Small comments
mlaveaux Jan 29, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions .github/copilot-instructions.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
This is a Rust based repository that demonstrates efficient, correct and safe implementations of algorithms and data structures.
This is a Rust-based repository that demonstrates efficient, correct, and safe implementations of algorithms and data structures.

## Development Workflows

Expand Down Expand Up @@ -40,12 +40,12 @@ cargo +nightly fmt
### Parsing & Grammar

- **`pest`/`pest_derive`**: PEG parser generator
- **`pest_consume`**: Vendored in `3rd-party/pest_consume/` - parser combinator framework built on pest
- **`pest_consume`**: A set of macros to consume pest parse trees into ASTs effectively.
- Grammar files use `.pest` extension (see `crates/syntax/mcrl2_grammar.pest`, `crates/aterm/term_grammar.pest`)

### Data Structures

- **`hashbrown`**: Fast HashMap implementation (basis for std HashMap)
- **`hashbrown`**: Fast HashMap implementation (basis for std::collections::HashMap)
- **`dashmap`**: Concurrent HashMap
- **`smallvec`**: Stack-allocated vectors for small sizes
- **`bitvec`**: Bit manipulation and bit vectors
Expand All @@ -58,13 +58,13 @@ cargo +nightly fmt

### CLI & I/O

- **`clap`** (with derive): Command-line argument parsing
- **`clap`** (derive feature): Command-line argument parsing
- **`bitstream-io`**: Binary I/O for LTS file formats
- **`env_logger`/`log`**: Logging infrastructure

### Development & Testing

- **`criterion`**: Micro-benchmarking framework (see `crates/*/benchmarks/`)
- **`criterion`**: Microbenchmarking framework (see `crates/*/benchmarks/`)
- **`test-case`/`test-log`**: Parameterized tests and test logging
- **`arbtest`/`arbitrary`**: Property-based testing and fuzzing
- **`trybuild`**: Compile-fail tests for proc macros (see `crates/macros/tests/`)
Expand All @@ -74,5 +74,5 @@ cargo +nightly fmt
- **`duct`**: Shell command execution (used in xtask)
- **`proc-macro2`/`quote`/`syn`**: Proc macro development (see `crates/macros/`)
- **`regex`**: Regular expressions (benchmarking, parsing)
- **`serde`/`serde_json`**: Serialization (benchmark results, configs)
- **`serde`/`serde_json`**: Serialization (benchmark results, configurations)

2 changes: 1 addition & 1 deletion .github/dependabot.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ updates:
allow:
- update-types: version-update:semver-major
groups:
- name: "crate-dependencies"
crate-dependencies:
patterns:
- "*"
- package-ecosystem: "github-actions"
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/msrv.yml
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ jobs:
working-directory: tools/mcrl2

- name: Test GUI MSRV
run: cargo msrv verify --rust-version 1.90.0
run: cargo msrv verify --rust-version 1.92.0
env:
RUSTC_WRAPPER: sccache
working-directory: tools/gui
2 changes: 1 addition & 1 deletion .github/workflows/test-miri.yml
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ jobs:
submodules: true

- name: Run tests
run: cargo +nightly miri nextest run --no-fail-fast --features merc_miri
run: cargo +nightly miri nextest run --no-fail-fast
env:
RUST_BACKTRACE: full
RUST_LOG: debug
Expand Down
2 changes: 1 addition & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
compile_commands.json
.cache

# Confiruation files for rustc
# Configuration files for rustc
.cargo

# will have the code coverage report
Expand Down
15 changes: 0 additions & 15 deletions .gitmodules

This file was deleted.

1 change: 0 additions & 1 deletion 3rd-party/boost-include-only
Submodule boost-include-only deleted from 42bdc6
1 change: 0 additions & 1 deletion 3rd-party/cpptrace
Submodule cpptrace deleted from 787d8a
1 change: 0 additions & 1 deletion 3rd-party/mCRL2
Submodule mCRL2 deleted from ce29f2
11 changes: 0 additions & 11 deletions 3rd-party/mCRL2-workarounds/README.md

This file was deleted.

This file was deleted.

Loading
Loading