Crate merc_syntax 

Overview

This crate contains a complete Pest grammar for the mCRL2 specification language, along with functionality to consume the resulting parse tree into an abstract syntax tree (AST). As opposed to the mCRL2 toolset where the AST is represented by terms, we store the AST in a Rust-idiomatic way using enums and structs. This means that we potentially use more memory because there is no term sharing of expressions, but manipulating the AST is much easier.

Usage

The mCRL2 specifications can simply be parsed using the untyped variants of the various objects: UntypedProcessSpecification, UntypedDataSpecification, etc.

use merc_syntax::UntypedProcessSpecification;

let mcrl2_spec = UntypedProcessSpecification::parse("
    act
        a, b: Nat;

    proc
        P(n: Nat) = a(n).P(n + 1) + b(n).P(n - 1);

    init
        P(0);

").unwrap();

Changelog

2.0

Added various builders and visitors to manipulate the ASTs.

Removed the arbitrary dependency since generating these expressions completely arbitrarily is not that useful.

Safety

This crate contains no unsafe code.

Minimum Supported Rust Version

We do not maintain an official minimum supported rust version (MSRV), and it may be upgraded at any time when necessary.

License

All MERC crates are licensed under the BSL-1.0 license. See the LICENSE file in the repository root for more information.

Structs

ActDecl

Action declaration

Action

ActionRenameDecl

ActionRenameRule

Assignment

BagElement

CommExpr

ConstructorDecl

Constructor declaration

DataExprUpdate

DeclTag

A unique type for declarations.

EqnDecl

Equation declaration

EqnSpec

IdDecl

A declaration of an identifier with its sort.

Mcrl2Parser

MultiAction

MultiActionLabel

Represents a multi action label a | b | c ....

PbesEquation

PresEquation

ProcDecl

Process declaration

PropVarDecl

PropVarInst

Rename

SortDecl

Sort declaration

Span

Source location information, spanning from start to end in the source text.

StateVarAssignment

StateVarDecl

UntypedActionRenameSpec

UntypedDataSpecification

An mCRL2 data specification.

UntypedPbes

An mCRL2 parameterised boolean equation system (PBES).

UntypedPres

An mCRL2 parameterised boolean equation system (PBES).

UntypedProcessSpecification

A complete mCRL2 process specification.

UntypedStateFrmSpec

Enums

ActFrm

ActFrmBinaryOp

ActionRHS

AliasedRule

Bound

ComplexSort

Complex (parameterized) sorts.

Condition

DataExpr

Data expression

DataExprBinaryOp

DataExprUnaryOp

Eq

FixedPointOperator

ModalityOperator

PbesExpr

PbesExprBinaryOp

PresExpr

PresExprBinaryOp

ProcExprBinaryOp

ProcessExpr

Process expression

Quantifier

RegFrm

Rule

This contains the grammar for .mcrl2 specifications.

Sort

Built-in simple sorts.

SortExpression

Expression representing a sort (type).

StateFrm

StateFrmOp

StateFrmUnaryOp

Statics

ACTFRM_PRATT_PARSER

Defines the operator precedence for action formulas using a Pratt parser.

DATAEXPR_PRATT_PARSER

PROCEXPR_PRATT_PARSER

REGFRM_PRATT_PARSER

Defines the operator precedence for regular expressions using a Pratt parser.

SORT_PRATT_PARSER

Functions

apply_regular_formula

Applies the given function recursively to the regular formula.

apply_sort_expression

apply_statefrm

Applies the given function recursively to the state formula.

generate_formula

Generates a formula that characterizes the counter example trace.

parse_actfrm

Parses a sequence of Rule pairs into an ActFrm using a Pratt parser defined in ACTFRM_PRATT_PARSER for operator precedence.

parse_action_names

Parses a list of action names from the given input string, for example those used in the hide operator.

parse_allow_action_names

Parses the action names for the allow operator from the given input string.

parse_comm_expr_set

Parses a list of communication expressions from the given input string.

parse_dataexpr

parse_pbesexpr

parse_presexpr

parse_process_expr

parse_regfrm

Parses a sequence of Rule pairs into an RegFrm using a Pratt parser defined in REGFRM_PRATT_PARSER for operator precedence.

parse_sortexpr

Parses a sequence of Rule pairs into a SortExpression using a Pratt parser for operator precedence.

parse_sortexpr_primary

parse_statefrm

print_location

Prints location information for a span in the source.

visit_action_formula

Visitor for action formulas.

visit_regular_formula

Maps the given function recursively to the regular formula.

visit_sort_expr

visit_statefrm

Visits the state formula and calls the given function on each subformula.

Type Aliases

DeclId

The index type for a label.