Enum Rule 

pub enum Rule {
    EOI,
    COMMENT,
    WHITESPACE,
    Id,
    IdAt,
    IdInfix,
    IdList,
    IdInfixList,
    Number,
    MCRL2Spec,
    DataSpec,
    ActSpec,
    ActDecl,
    SortSpec,
    SortDecl,
    SortExpr,
    SortExprPrimary,
    SortExprBool,
    SortExprPos,
    SortExprNat,
    SortExprInt,
    SortExprReal,
    SortExprList,
    SortExprSet,
    SortExprBag,
    SortExprFSet,
    SortExprFBag,
    SortExprParens,
    SortExprStruct,
    SortExprInfix,
    SortExprFunction,
    SortExprProduct,
    ConstrDecl,
    ConstrDeclList,
    SortProduct,
    DataExpr,
    DataExprUnit,
    DataExprPrefix,
    DataExprForall,
    DataExprExists,
    DataExprLambda,
    DataExprNegation,
    DataExprMinus,
    DataExprSize,
    DataExprPrimary,
    DataExprTrue,
    DataExprFalse,
    DataExprEmptyList,
    DataExprEmptySet,
    DataExprEmptyBag,
    DataExprListEnum,
    DataExprBagEnum,
    DataExprSetBagComp,
    DataExprSetEnum,
    DataExprBrackets,
    DataExprPostfix,
    DataExprUpdate,
    DataExprApplication,
    DataExprWhr,
    DataExprInfix,
    DataExprImpl,
    DataExprDisj,
    DataExprConj,
    DataExprEq,
    DataExprNeq,
    DataExprLeq,
    DataExprSnoc,
    DataExprLess,
    DataExprGeq,
    DataExprGreater,
    DataExprIn,
    DataExprCons,
    DataExprConcat,
    DataExprAdd,
    DataExprSubtract,
    DataExprDiv,
    DataExprIntDiv,
    DataExprMod,
    DataExprMult,
    DataExprAt,
    DataExprList,
    Assignment,
    AssignmentList,
    VarDecl,
    VarsDecl,
    VarsDeclList,
    BagEnumElt,
    BagEnumEltList,
    Action,
    ActIdSet,
    MultActId,
    MultActIdList,
    MultActIdSet,
    ProjDecl,
    ProjDeclList,
    CommExpr,
    CommExprList,
    CommExprSet,
    RenExpr,
    RenExprList,
    RenExprSet,
    ProcExpr,
    ProcExprPrimary,
    ProcExprDelta,
    ProcExprTau,
    ProcExprBlock,
    ProcExprAllow,
    ProcExprHide,
    ProcExprRename,
    ProcExprComm,
    ProcExprBrackets,
    ProcExprId,
    ProcExprPrefix,
    ProcExprSum,
    ProcExprDist,
    ProcExprIfThen,
    ProcExprIf,
    ProcExprInfix,
    ProcExprChoice,
    ProcExprLeftMerge,
    ProcExprParallel,
    ProcExprSeq,
    ProcExprUntil,
    ProcExprSync,
    ProcExprPostfix,
    ProcExprAt,
    ProcExprNoIf,
    ProcExprNoIfInfix,
    ProcDecl,
    ProcSpec,
    Init,
    IdsDecl,
    ConsSpec,
    MapSpec,
    GlobVarSpec,
    VarSpec,
    EqnSpec,
    EqnDecl,
    StateFrmSpec,
    FormSpec,
    StateFrmSpecElt,
    StateFrm,
    StateFrmPrimary,
    StateFrmBrackets,
    StateFrmTrue,
    StateFrmFalse,
    StateFrmDelay,
    StateFrmYaled,
    StateFrmId,
    StateFrmDataValExpr,
    StateFrmPrefix,
    StateFrmMu,
    StateFrmNu,
    StateFrmInf,
    StateFrmSup,
    StateFrmSum,
    StateFrmForall,
    StateFrmExists,
    StateFrmBox,
    StateFrmDiamond,
    StateFrmUnaryMinus,
    StateFrmNegation,
    StateFrmLeftConstantMultiply,
    StateFrmInfix,
    StateFrmAddition,
    StateFrmImplication,
    StateFrmDisjunction,
    StateFrmConjunction,
    StateFrmPostfix,
    StateFrmRightConstantMultiply,
    RegFrm,
    RegFrmPrimary,
    RegFrmBackets,
    RegFrmInfix,
    RegFrmAlternative,
    RegFrmComposition,
    RegFrmPostfix,
    RegFrmIteration,
    RegFrmPlus,
    ActFrm,
    ActFrmPrimary,
    ActFrmBrackets,
    ActFrmTrue,
    ActFrmFalse,
    ActFrmPrefix,
    ActFrmNegation,
    ActFrmForall,
    ActFrmExists,
    ActFrmInfix,
    ActFrmImplies,
    ActFrmUnion,
    ActFrmIntersect,
    ActFrmPostfix,
    ActFrmAt,
    MultAct,
    MultiActTau,
    ActionList,
    DataValExpr,
    StateVarDecl,
    StateVarAssignment,
    StateVarAssignmentList,
    ActionRenameSpec,
    ActionRenameRuleSpec,
    ActionRenameRule,
    ActionRenameRuleRHS,
    FixedPointOperator,
    FixedPointMu,
    FixedPointNu,
    PbesSpec,
    PbesEqnSpec,
    PbesEqnDecl,
    PropVarDecl,
    PropVarInst,
    PbesInit,
    PbesExpr,
    PbesExprPrimary,
    PbesExprParens,
    PbesExprTrue,
    PbesExprFalse,
    PbesExprPrefix,
    PbesExprForall,
    PbesExprExists,
    PbesExprNegation,
    PbesExprInfix,
    PbesExprImplies,
    PbesExprConj,
    PbesExprDisj,
    PresSpec,
    PresEqnSpec,
    PresEqnDecl,
    PresExpr,
    PresExprPrimary,
    PresExprParens,
    PresExprEqinf,
    PresExprEqninf,
    PresExprCondsm,
    PresExprCondeq,
    PresExprPrefix,
    PresExprInf,
    PresExprSup,
    PresExprSum,
    PresExprLeftConstantMultiply,
    PresExprInfix,
    PresExprAdd,
    PresExprPostfix,
    PresExprRightConstMultiply,
}

This contains the grammar for .mcrl2 specifications.

Considerations for PEG parsers

AFTER parsing we can use a PrattParser to define the associativity and precedence of operators for rules of the following shape:

expr = { prefix* ~ primary ~ postfix* ~ (infix ~ prefix* ~ primary ~ postfix* )* }

The | operator defines a choice operator and does not mean OR with backtracking. This means the following rules

Expr = { “Bool” ~ ASCII_ALPHANUMERIC* }

Will match the expression “Boolean” by eating up “Bool” and leaving “ean” as the remaining. However, this is undesirable since this should be an identifier Boolean. This is resolved by only allowing keywords to match whenever it is not by something that is part of an identifier.

Variants

EOI

End-of-input

COMMENT

This is a silent rule eating all the comments.

WHITESPACE

This is a silent rule eating all the white space in the input.

Id

Identifiers

IdAt

Internal identifiers that can start with at “@”.

IdInfix

Identifiers that can also be the allowed infix operators.

IdList

List of identifiers

IdInfixList

List of identifiers

Number

Numbers

MCRL2Spec

Parsing an mCRL2 specification

DataSpec

Parsing an mCRL2 specification

ActSpec

Action specification

ActDecl

Declaration of actions

SortSpec

Sort specification

SortDecl

SortExpr

A general sort expression with infix operators.

SortExprPrimary

A single sort expression

SortExprBool

SortExprPos

SortExprNat

SortExprInt

SortExprReal

SortExprList

SortExprSet

SortExprBag

SortExprFSet

SortExprFBag

SortExprParens

SortExprStruct

SortExprInfix

SortExprFunction

SortExprProduct

ConstrDecl

Constructor declaration

ConstrDeclList

Constructor declaration list

SortProduct

A single sort A -> B -> …

DataExpr

Data Expression

DataExprUnit

Data Expressions without infix operators

DataExprPrefix

DataExprForall

DataExprExists

DataExprLambda

DataExprNegation

DataExprMinus

DataExprSize

DataExprPrimary

DataExprTrue

DataExprFalse

DataExprEmptyList

DataExprEmptySet

DataExprEmptyBag

DataExprListEnum

DataExprBagEnum

DataExprSetBagComp

DataExprSetEnum

DataExprBrackets

DataExprPostfix

DataExprUpdate

DataExprApplication

DataExprWhr

DataExprInfix

DataExprImpl

DataExprDisj

DataExprConj

DataExprEq

DataExprNeq

DataExprLeq

DataExprSnoc

DataExprLess

DataExprGeq

DataExprGreater

DataExprIn

DataExprCons

DataExprConcat

DataExprAdd

DataExprSubtract

DataExprDiv

DataExprIntDiv

DataExprMod

DataExprMult

DataExprAt

DataExprList

List of data expressions

Assignment

Assignment x = expression

AssignmentList

List of assignments

VarDecl

Typed variable

VarsDecl

Typed variables

VarsDeclList

Individually typed variables

BagEnumElt

Bag element with multiplicity

BagEnumEltList

Elements in a finite bag

Action

Action, process instantiation

ActIdSet

Action set

MultActId

Multi-action label

MultActIdList

MultActIdSet

Multi-action label set

ProjDecl

Domain with optional projection

ProjDeclList

Declaration of projection functions

CommExpr

Action synchronization

CommExprList

Action synchronizations

CommExprSet

Action synchronization set

RenExpr

Action renaming

RenExprList

Multiple action renamings

RenExprSet

An action renaming set.

ProcExpr

ProcExprPrimary

Single Process expressions

ProcExprDelta

ProcExprTau

ProcExprBlock

ProcExprAllow

ProcExprHide

ProcExprRename

ProcExprComm

ProcExprBrackets

ProcExprId

ProcExprPrefix

ProcExprSum

ProcExprDist

ProcExprIfThen

ProcExprIf

ProcExprInfix

ProcExprChoice

ProcExprLeftMerge

ProcExprParallel

ProcExprSeq

ProcExprUntil

ProcExprSync

ProcExprPostfix

ProcExprAt

ProcExprNoIf

ProcExprNoIfInfix

ProcDecl

ProcSpec

Process specification

Init

Initial process

IdsDecl

Typed parameters

ConsSpec

Declaration of constructors

MapSpec

Declaration of mappings

GlobVarSpec

Declaration of global variables

VarSpec

Declaration of variables

EqnSpec

Definition of equations

EqnDecl

Conditional equation

StateFrmSpec

Single state formula or state formula specification

FormSpec

StateFrmSpecElt

StateFrm

StateFrmPrimary

StateFrmBrackets

StateFrmTrue

StateFrmFalse

StateFrmDelay

StateFrmYaled

StateFrmId

StateFrmDataValExpr

StateFrmPrefix

StateFrmMu

StateFrmNu

StateFrmInf

StateFrmSup

StateFrmSum

StateFrmForall

StateFrmExists

StateFrmBox

StateFrmDiamond

StateFrmUnaryMinus

StateFrmNegation

StateFrmLeftConstantMultiply

StateFrmInfix

StateFrmAddition

StateFrmImplication

StateFrmDisjunction

StateFrmConjunction

StateFrmPostfix

StateFrmRightConstantMultiply

RegFrm

Regular formulas. To guard for the ambiguity of a + b and a+ we use a negative premise

RegFrmPrimary

RegFrmBackets

RegFrmInfix

RegFrmAlternative

RegFrmComposition

RegFrmPostfix

RegFrmIteration

RegFrmPlus

ActFrm

ActFrmPrimary

ActFrmBrackets

ActFrmTrue

ActFrmFalse

ActFrmPrefix

ActFrmNegation

ActFrmForall

ActFrmExists

ActFrmInfix

ActFrmImplies

ActFrmUnion

ActFrmIntersect

ActFrmPostfix

ActFrmAt

MultAct

MultiActTau

ActionList

DataValExpr

Marked data exression

StateVarDecl

State variable declaration

StateVarAssignment

Typed variable with initial value

StateVarAssignmentList

Typed variable list

ActionRenameSpec

Action rename specification

ActionRenameRuleSpec

Action rename rule section

ActionRenameRule

Conditional action renaming

ActionRenameRuleRHS

FixedPointOperator

FixedPointMu

FixedPointNu

PbesSpec

Parameterised boolean equations systems

PbesEqnSpec

PbesEqnDecl

PropVarDecl

PropVarInst

PbesInit

PbesExpr

PbesExprPrimary

PbesExprParens

PbesExprTrue

PbesExprFalse

PbesExprPrefix

PbesExprForall

PbesExprExists

PbesExprNegation

PbesExprInfix

PbesExprImplies

PbesExprConj

PbesExprDisj

PresSpec

Parameterised boolean equations systems

PresEqnSpec

PresEqnDecl

PresExpr

PresExprPrimary

PresExprParens

PresExprEqinf

PresExprEqninf

PresExprCondsm

PresExprCondeq

PresExprPrefix

PresExprInf

PresExprSup

PresExprSum

PresExprLeftConstantMultiply

PresExprInfix

PresExprAdd

PresExprPostfix

PresExprRightConstMultiply

Implementations

impl Rule

pub fn all_rules() -> &'static [Rule]

Trait Implementations

impl Clone for Rule

fn clone(&self) -> Rule

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Rule

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Hash for Rule

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Ord for Rule

fn cmp(&self, other: &Rule) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl Parser<Rule> for Mcrl2Parser

fn parse<'i>(rule: Rule, input: &'i str) -> Result<Pairs<'i, Rule>, Error<Rule>>

Parses a &str starting from rule.

impl PartialEq for Rule

fn eq(&self, other: &Rule) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for Rule

fn partial_cmp(&self, other: &Rule) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Copy for Rule

impl Eq for Rule

impl StructuralPartialEq for Rule