Language reference/Lexical syntax

From MCRL2

Syntax definition

Lexical syntax Data syntax Process syntax mu-calculus syntax PBES syntax

Contents

This page describes the lexical syntax of mCRL2 expressions and specifications.

Contents 1 Lexical elements 1.1 Identifiers 1.2 Numbers 1.3 Whitespace 1.4 Comments

Lexical elements

The notions of identifiers, numbers, whitespace and comments are defined.

Identifiers

An identifier is a string matching the pattern "[A-Za-z_][A-Za-z_0-9]*", excluding the following reserved words:

sort cons map var eqn act glob proc pbes init
struct Bool Pos Nat Int Real List Set Bag
true false if div mod in lambda forall exists whr end
delta tau sum block allow hide rename comm
val mu nu delay yaled nil

Identifiers are used for representing sort names b, function names f, data variable names x, action names a, process reference names P, and propositional variable names X.

Numbers

A number is a string matching the pattern "0" or "[1-9][0-9]*".

Whitespace

Spaces, tabs and newlines are treated as whitespace.

Comments

A "%"-sign indicates the beginning of a comment that extends to the end of the line.

---

Syntax definition

Data syntax