Repository navigation
Conversation
…cess specifications
…ion, since this is not stored
…the rewriters. * Currently does not support the compiling rewriter.
There was a problem hiding this comment.
🟡 Changes recommended
A missing workspace member, unresolved modules and imports, and an undefined forwarded feature block builds, while number-encoding detection also misclassifies machine-word specifications.
8 open issues
What changed in this PR
This PR begins moving LPS support from the mCRL2 tools workspace into the main workspace, using native ATerms to support exploration and control-flow analysis.
Changes:
- Adds native LPS data structures, binary I/O, formatting, and control-flow exploration code.
- Adds runtime rewriter selection and exposes supporting action, sort, and numeric APIs.
- Updates workspace dependencies and semantic-version check exclusions.
| File | Description |
|---|---|
crates/transition_systems/lts/src/multi_action.rs |
Types action-label arguments as sorts and adds an accessor. |
crates/transition_systems/lts/src/lib.rs |
Exports action term types for LPS I/O. |
crates/rewriter/sabre/src/rewriter.rs |
Adds runtime rewrite-engine selection. |
crates/rewriter/data/src/lib.rs |
Exports additional sort predicates. |
crates/rewriter/data/src/data_terms.rs |
Adds structured-sort detection and exposes sort predicates. |
crates/rewriter/data/src/data_expression.rs |
Makes machine-number values publicly accessible. |
crates/language/lps/src/lps_terms.rs |
Defines distribution and initializer terms for binary I/O. |
crates/language/lps/src/linear_process.rs |
Defines native LPS structures and display implementations. |
crates/language/lps/src/lib.rs |
Establishes the LPS crate’s public model and I/O API. |
crates/language/lps/src/io_lps.rs |
Implements binary LPS reading and writing. |
crates/language/lps/src/control_flow.rs |
Adds control-flow parameter and edge analysis. |
crates/language/lps/src/cfg_lps.rs |
Adds a CFG-based exploration wrapper and pruning metrics. |
crates/language/lps/README.md |
Documents the native LPS model and binary I/O usage. |
crates/language/lps/Cargo.toml |
Defines the new crate’s dependencies and features. |
crates/language/lowering/src/system_symbols.rs |
Adds the negative-integer constructor name and declaration test. |
crates/language/lowering/src/number_encoding.rs |
Adds numeric-encoding detection and tests. |
crates/language/lowering/src/lowering.rs |
Reuses the shared machine-word width and reorganizes helpers. |
crates/language/lowering/src/lib.rs |
Exports numeric-encoding detection. |
crates/language/lowering/Cargo.toml |
Adds supporting dependencies and a test dependency. |
crates/core/number/src/machine_word.rs |
Exposes the machine-word width and updates its uses. |
crates/core/number/src/lib.rs |
Re-exports the machine-word width constant. |
Cargo.toml |
Registers the native LPS library and tool workspace entries. |
Cargo.lock |
Records native LPS packages and dependency updates. |
.github/workflows/semver.yml |
Excludes the new LPS packages from semantic-version checks. |
Review effort: Balanced
|
|
||
| "crates/xtask", | ||
|
|
||
| "tools/lps", |
Comment on lines
+31
to
+32
| if matches!(term.arg(0).get_head_symbol().name(), C1 | C_DUB | C_NAT) { | ||
| return NumberEncoding::Binary; |
| metrics = ["merc_explore/metrics", "merc_symbolic/metrics"] | ||
|
|
||
| # Derives the `clap::ValueEnum` trait. | ||
| clap = ["merc_sabre/clap"] |
| #![forbid(unsafe_code)] | ||
|
|
||
| mod io_lps; | ||
| mod linear_process; |
| use merc_data::Mcrl2DataSpecification; | ||
| use merc_data::SortExpression; | ||
| use merc_data::is_bool_literal; | ||
| use merc_lowering::Pretty; |
Comment on lines
+10
to
+14
| use crate::explore_explicit::ExplicitContext; | ||
| use crate::explore_explicit::ExplicitLinearProcessSpecification; | ||
| use crate::explore_explicit::ExplicitSummand; | ||
| use crate::explore_explicit::LpsMultiActionLabel; | ||
| use crate::transformations::TransformedLps; |
Comment on lines
+128
to
+130
| if !self.action_labels.is_empty() { | ||
| writeln!(f, "act {};", self.action_labels.iter().format(", "))?; | ||
| } |
| } | ||
|
|
||
| /// A rewriter of the selected [RewriterKind]. | ||
| pub enum DataRewriter { |
This branch has not been deployed
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.
Overview
Ported several modules from the
tools/mcrl2workspace into the main workspace to allow it to operate on the LPSs defined there, for example control flow graphs. It would be nice to generalize them, but there are now two different aterm representations, the native one and the mCRL2 one that cannot be easily merged.