Language reference/Process syntax

From MCRL2

Syntax definition

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

Contents

This page describes the concrete syntax of process specifications.

The syntax of process expressions and specifications is described, and how they are used in files.

Process expressions

Process expressions p:

p    ::=  a  |  "delta"  |  "tau"  |  p "+" p  |  p "." p
       |  P  |  p "|" p  |  p "||" p  |  p "||_" p
       |  "allow"  "(" "{" as "," ... "," as "}" "," p ")"
       |  "block"  "(" "{" a  "," ... "," a  "}" "," p ")"
       |  "hide"   "(" "{" a  "," ... "," a  "}" "," p ")"
       |  "rename" "(" "{" ar "," ... "," ar "}" "," p ")"
       |  "comm"   "(" "{" ac "," ... "," ac "}" "," p ")"
       |  a "(" d "," ... "," d ")"  |  P "(" d "," ... "," d ")"
       |  P "(" ")"  |  P "(" x "=" d "," ... "," x "=" d ")"
       |  c "->" p "<>" p  |  c "->" p
       |  "sum" mvd "," ... "," mvd "." p
       |  p "@" t  |  t ">>" p  |  p ""<<" q
       |  "(" p ")"
as   ::=  a "|" ... "|" a
ar   ::=  a "->" a
ac   ::=  a "|" as "->" a  |  a "|" as "->" "tau"  |  a "|" as
mvd  ::=  x "," ... "," x ":" s

Here as represents an action sequence, ar an action renaming, ac an action communication, and mvd a multiple variable declaration. Furthermore, a stands for an action name, P for a process reference name, and x for a data variable name, which are all identifiers. s stands for a sort expression, and d, c and t stand for data expressions, of which c is of sort "Bool" and t is of sort "Real". For technical reasons, both c and t may not have an infix operator, a where clause or a quantifier at the top-level (parentheses should be used instead).

In process expressions, "a" represents an action, "delta" represents inaction, "tau" the internal action, "+" alternative composition, "." sequential composition, "P" a process reference, "|" synchronisation, "||" parallel composition, "||_" left merge, "allow" restriction, "block" blocking, "hide" hiding, "rename" renaming, and "comm" communication. Furthermore, "a(d,...,d)" represents a parameterised action, "P(d,...,d)" represents a parameterised process reference, and "P()" and "P(x=d,...,x=d)" represent process reference assignments. The expressions "c -> p <> p" and "c -> p" represent the conditional, and "sum" represents summation over a data type. Finally, there are three operators involving time: "@" represents a process at a certain time, ">>" represents initialisation, and "<<" represents before.

The descending order of precedence of the operators is: "|", "@", ".", { "<<", ">>" }, "->", { "||", "||_" }, "sum", "+". Of these operators "+", "||", "||_", ".", "->" and "|" associate to the right. These priorities can be overruled with the use of parentheses "(" and ")".

Process specifications

Process specifications proc_spec:

proc_spec      ::=  ( proc_spec_elt )*
proc_spec_elt  ::=  data_spec
                 |  "act"  ( ad ";" )+
                 |  "glob" ( mvd ";" )+
                 |  "proc" ( pd ";" )+
                 |  "init" p ";"
ad             ::=  a  |  a ":" s "#" ... "#" s
pd             ::=  P "=" p  |  P "(" mvd "," ... "," mvd ")" "=" p

Here proc_spec_elt represents a process specification element, data_spec a data specification, ad an action declaration, mvd a multiple variable declaration, pd a process declaration, p a process expression, and s a sort expression. Furthermore, a stands for an action name, and P for a process reference name, which are both identifiers.

We impose the restriction that proc_spec should contain precisely one occurrence of the keyword "init".

Files

Files containing an instance of proc_spec can be parsed with the tool mcrl22lps. For the syntax of the lexical elements, see the page on lexical syntax.

The suggested extension of process specification files is ".mcrl2".

Example files can be found in the examples directory of the svn repository.

---

Data syntax

mu-calculus syntax