Lines
82.29 %
Functions
44.44 %
Branches
33.33 %
use std::hash::Hash;
use merc_utilities::TagIndex;
/// A unique type for declarations.
pub struct DefTag;
/// The index type for a label.
pub type DefId = TagIndex<usize, DefTag>;
/// A complete mCRL2 process specification.
#[derive(Debug, Default, Eq, PartialEq, Hash)]
pub struct UntypedProcessSpecification {
pub data_specification: UntypedDataSpecification,
pub global_variables: Vec<IdDecl>,
pub action_declarations: Vec<ActDecl>,
pub process_declarations: Vec<ProcDecl>,
pub init: Option<ProcessExpr>,
}
/// An mCRL2 data specification.
#[derive(Clone, Debug, Default, Eq, PartialEq, Hash)]
pub struct UntypedDataSpecification {
pub sort_declarations: Vec<SortDecl>,
pub constructor_declarations: Vec<IdDecl>,
pub map_declarations: Vec<IdDecl>,
pub equation_declarations: Vec<EqnSpec>,
impl UntypedDataSpecification {
/// Returns true if the data specification is empty.
pub fn is_empty(&self) -> bool {
self.sort_declarations.is_empty()
&& self.constructor_declarations.is_empty()
&& self.map_declarations.is_empty()
&& self.equation_declarations.is_empty()
/// Merges another data specification into the current one.
pub fn merge(&mut self, other_spec: &UntypedDataSpecification) {
self.sort_declarations.extend_from_slice(&other_spec.sort_declarations);
self.constructor_declarations
.extend_from_slice(&other_spec.constructor_declarations);
self.map_declarations.extend_from_slice(&other_spec.map_declarations);
self.equation_declarations
.extend_from_slice(&other_spec.equation_declarations);
/// An mCRL2 parameterised boolean equation system (PBES).
pub struct UntypedPbes {
pub equations: Vec<PbesEquation>,
pub init: PropVarInst,
pub struct UntypedPres {
pub equations: Vec<PresEquation>,
#[derive(Debug, Eq, PartialEq, Hash)]
pub struct PropVarDecl {
pub identifier: String,
pub parameters: Vec<IdDecl>,
pub span: Span,
impl PropVarDecl {
/// Creates a new propositional variable declaration with the given identifier and parameters.
pub fn new(identifier: String, parameters: Vec<IdDecl>) -> Self {
PropVarDecl {
identifier,
parameters,
span: Span::default(),
pub struct PropVarInst {
pub arguments: Vec<DataExpr>,
impl PropVarInst {
/// Creates a new instance of a propositional variable with the given identifier and arguments.
pub fn new(identifier: String, arguments: Vec<DataExpr>) -> Self {
PropVarInst { identifier, arguments }
/// A declaration of an identifier with its sort.
#[derive(Clone, Debug, Eq, PartialEq, PartialOrd, Ord, Hash)]
pub struct IdDecl {
/// Identifier being declared
/// Sort expression for this identifier
pub sort: SortExpression,
/// Source location information
/// Unique ID assigned to this declaration during name resolution.
pub id: Option<DefId>,
impl IdDecl {
/// Creates a new identifier declaration with the given identifier, sort, and span.
pub fn new(identifier: String, sort: SortExpression, span: Span) -> Self {
IdDecl {
sort,
span,
id: None,
/// Expression representing a sort (type).
#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd, Hash)]
pub enum SortExpression {
/// Product of two sorts (A # B)
Product {
lhs: Box<SortExpression>,
rhs: Box<SortExpression>,
},
/// Function sort (A -> B)
Function {
domain: Box<SortExpression>,
range: Box<SortExpression>,
Struct {
inner: Vec<ConstructorDecl>,
/// Reference to a named sort
Reference(String),
/// Built-in simple sort
Simple(Sort),
/// Parameterized complex sort
Complex(ComplexSort, Box<SortExpression>),
/// Resolved reference to a sort after name resolution
Resolved(String, DefId),
/// Function sort (A_0 # ... # A_n -> B) after flattening (performed during name resolution)
FlattenedFunction {
domain: Vec<SortExpression>,
/// Constructor declaration
pub struct ConstructorDecl {
pub name: String,
pub args: Vec<(Option<String>, SortExpression)>,
pub projection: Option<String>,
/// Built-in simple sorts.
#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd, Hash)]
pub enum Sort {
Bool,
Pos,
Int,
Nat,
Real,
/// Complex (parameterized) sorts.
pub enum ComplexSort {
List,
Set,
FSet,
FBag,
Bag,
/// Sort declaration
#[derive(Clone, Debug, Eq, PartialEq, Hash)]
pub struct SortDecl {
/// Sort identifier
/// Sort expression (if structured)
pub expr: Option<SortExpression>,
/// Where the sort is defined
impl SortDecl {
/// Creates a new sort declaration with the given identifier, expression, and span.
pub fn new(identifier: String, expr: Option<SortExpression>, span: Span) -> Self {
SortDecl {
expr,
pub struct EqnSpec {
pub variables: Vec<IdDecl>,
pub equations: Vec<EqnDecl>,
/// Equation declaration
pub struct EqnDecl {
pub condition: Option<DataExpr>,
pub lhs: DataExpr,
pub rhs: DataExpr,
/// Action declaration
pub struct ActDecl {
pub args: Vec<SortExpression>,
/// Process declaration
pub struct ProcDecl {
pub params: Vec<IdDecl>,
pub body: ProcessExpr,
pub enum DataExprUnaryOp {
Negation,
Minus,
Size,
pub enum DataExprBinaryOp {
Conj,
Disj,
Implies,
Equal,
NotEqual,
LessThan,
LessEqual,
GreaterThan,
GreaterEqual,
Cons,
Snoc,
In,
Concat,
Add,
Subtract,
Div,
IntDiv,
Mod,
Multiply,
At,
/// Data expression
pub enum DataExpr {
Id(String),
Number(String), // Is string because the number can be any size.
Bool(bool),
Application {
function: Box<DataExpr>,
arguments: Vec<DataExpr>,
EmptyList,
List(Vec<DataExpr>),
EmptySet,
Set(Vec<DataExpr>),
EmptyBag,
Bag(Vec<BagElement>),
SetBagComp {
variable: IdDecl,
predicate: Box<DataExpr>,
Lambda {
variables: Vec<IdDecl>,
body: Box<DataExpr>,
Quantifier {
op: Quantifier,
Unary {
op: DataExprUnaryOp,
expr: Box<DataExpr>,
Binary {
op: DataExprBinaryOp,
lhs: Box<DataExpr>,
rhs: Box<DataExpr>,
FunctionUpdate {
update: Box<DataExprUpdate>,
Whr {
assignments: Vec<Assignment>,
pub struct BagElement {
pub expr: DataExpr,
pub multiplicity: DataExpr,
pub struct DataExprUpdate {
pub update: DataExpr,
pub struct Assignment {
pub enum ProcExprBinaryOp {
Sequence,
Choice,
Parallel,
LeftMerge,
CommMerge,
Until,
/// Process expression
pub enum ProcessExpr {
Id(String, Vec<Assignment>),
Action(String, Vec<DataExpr>),
Delta,
Tau,
Sum {
operand: Box<ProcessExpr>,
Dist {
expr: DataExpr,
op: ProcExprBinaryOp,
lhs: Box<ProcessExpr>,
rhs: Box<ProcessExpr>,
Hide {
actions: Vec<String>,
Rename {
renames: Vec<Rename>,
Allow {
actions: Vec<MultiActionLabel>,
Block {
Comm {
comm: Vec<CommExpr>,
Condition {
condition: DataExpr,
then: Box<ProcessExpr>,
else_: Option<Box<ProcessExpr>>,
At {
expr: Box<ProcessExpr>,
operand: DataExpr,
pub struct UntypedStateFrmSpec {
pub formula: StateFrm,
#[derive(Debug, Clone, Copy, Eq, PartialEq, Hash)]
pub enum StateFrmUnaryOp {
pub enum StateFrmOp {
Addition,
Disjunction,
Conjunction,
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub enum FixedPointOperator {
Least,
Greatest,
pub struct StateVarDecl {
pub arguments: Vec<StateVarAssignment>,
impl StateVarDecl {
/// Creates a new state variable declaration.
pub fn new(identifier: String, arguments: Vec<StateVarAssignment>) -> Self {
StateVarDecl {
arguments,
pub struct StateVarAssignment {
pub enum ModalityOperator {
Diamond,
Box,
pub enum StateFrm {
True,
False,
/// `delay` or `delay@t`; the optional time is `None` for a bare `delay`.
Delay(Option<DataExpr>),
/// `yaled` or `yaled@t`; the optional time is `None` for a bare `yaled`.
Yaled(Option<DataExpr>),
Id(String, Vec<DataExpr>),
DataValExprLeftMult(DataExpr, Box<StateFrm>),
DataValExprRightMult(Box<StateFrm>, DataExpr),
DataValExpr(DataExpr),
Modality {
operator: ModalityOperator,
formula: RegFrm,
expr: Box<StateFrm>,
op: StateFrmUnaryOp,
op: StateFrmOp,
lhs: Box<StateFrm>,
rhs: Box<StateFrm>,
quantifier: Quantifier,
body: Box<StateFrm>,
Bound {
bound: Bound,
FixedPoint {
operator: FixedPointOperator,
variable: StateVarDecl,
/// Represents a multi action label `a | b | c ...`.
#[derive(Clone, Debug, Eq, PartialEq, Hash, PartialOrd, Ord)]
pub struct MultiActionLabel {
pub actions: Vec<String>,
impl MultiActionLabel {
/// Creates a new multi-action label from a list of action identifiers.
pub fn new(actions: Vec<String>) -> Self {
MultiActionLabel { actions }
/// Returns true if the multi-action label is empty (i.e., contains no actions).
pub fn is_tau_label(&self) -> bool {
self.actions.is_empty()
pub struct Action {
pub id: String,
pub args: Vec<DataExpr>,
impl Action {
/// Creates a new action from an identifier and a list of arguments.
pub fn new(id: String, args: Vec<DataExpr>) -> Self {
Action { id, args }
#[derive(Clone, Debug, Eq)]
pub struct MultiAction {
pub actions: Vec<Action>,
impl MultiAction {
/// Creates a new multi-action from a list of actions.
pub fn new(actions: Vec<Action>) -> Self {
MultiAction { actions }
/// Creates the empty multi-action, which represents the tau action.
pub fn tau() -> Self {
MultiAction { actions: Vec::new() }
impl PartialEq for MultiAction {
fn eq(&self, other: &Self) -> bool {
// Check whether both multi-actions contain the same actions
if self.actions.len() != other.actions.len() {
return false;
// Map every action onto the other, equal length means they must be the same.
for action in self.actions.iter() {
if !other.actions.contains(action) {
true
impl Hash for MultiAction {
fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
let mut actions = self.actions.clone();
// Sort the action ids to ensure that the hash is independent of the order.
actions.sort();
for action in actions {
action.hash(state);
pub enum Quantifier {
Exists,
Forall,
pub enum ActFrmBinaryOp {
Union,
Intersect,
pub enum ActFrm {
MultAct(MultiAction),
DataExprVal(DataExpr),
Negation(Box<ActFrm>),
body: Box<ActFrm>,
op: ActFrmBinaryOp,
lhs: Box<ActFrm>,
rhs: Box<ActFrm>,
pub enum PbesExpr {
PropVarInst(PropVarInst),
body: Box<PbesExpr>,
Negation(Box<PbesExpr>),
op: PbesExprBinaryOp,
lhs: Box<PbesExpr>,
rhs: Box<PbesExpr>,
pub enum Eq {
EqInf,
EqnInf,
pub enum Condition {
Condsm,
Condeq,
// TODO: What should this be called?
pub enum Bound {
Inf,
Sup,
Sum,
pub enum PresExprBinaryOp {
pub enum PresExpr {
RightConstantMultiply {
expr: Box<PresExpr>,
constant: DataExpr,
LeftConstantMultiply {
op: Bound,
Equal {
eq: Eq,
body: Box<PresExpr>,
condition: Condition,
lhs: Box<PresExpr>,
then: Box<PresExpr>,
else_: Box<PresExpr>,
Negation(Box<PresExpr>),
op: PresExprBinaryOp,
rhs: Box<PresExpr>,
pub struct PbesEquation {
pub operator: FixedPointOperator,
pub variable: PropVarDecl,
pub formula: PbesExpr,
impl PbesEquation {
/// Creates a new PBES equation with the given operator, variable and formula.
pub fn new(operator: FixedPointOperator, variable: PropVarDecl, formula: PbesExpr) -> Self {
PbesEquation {
operator,
variable,
formula,
pub enum PbesExprBinaryOp {
pub struct PresEquation {
pub formula: PresExpr,
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub enum RegFrm {
Action(ActFrm),
Iteration(Box<RegFrm>),
Plus(Box<RegFrm>),
Sequence { lhs: Box<RegFrm>, rhs: Box<RegFrm> },
Choice { lhs: Box<RegFrm>, rhs: Box<RegFrm> },
pub struct Rename {
pub from: String,
pub to: String,
pub struct CommExpr {
pub from: MultiActionLabel,
impl CommExpr {
/// Creates a new communication expression from a multi-action label and a target action identifier.
pub fn new(from: MultiActionLabel, to: String) -> Self {
CommExpr { from, to }
pub struct UntypedActionRenameSpec {
pub rename_declarations: Vec<ActionRenameDecl>,
pub struct ActionRenameDecl {
pub variables_specification: Vec<IdDecl>,
pub rename_rule: ActionRenameRule,
pub struct ActionRenameRule {
pub action: Action,
pub rhs: ActionRHS,
pub enum ActionRHS {
Action(Action),
/// Source location information, spanning from start to end in the source text.
#[derive(Clone, Default, Debug, Eq, Ord, PartialEq, PartialOrd, Hash)]
pub struct Span {
pub start: usize,
pub end: usize,
impl From<pest::Span<'_>> for Span {
fn from(span: pest::Span) -> Self {
Span {
start: span.start(),
end: span.end(),