PAT: Process Analysis Toolkit

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

How to write Process Definitions

This document presents the EBNF syntax of the specifica tion language used in our model checker. The name vCSP stands for variables enriched Communicating Sequential Processes.

SYNTAX

NOTE: the rules for expression and definition are written using a hierarchical order to show the precedences between these rules.

the starting rule for the specification
specification : specBody*;

specBody : letDefintion global definitions
| definition process definitions
| assertion assertion definitions
| alpha alphabets definitions
| define global constants and condition declarations
| channel global channel declarations
;

various assertion definitions
assertion : ‘#’ ‘assert’ definitionRef
(
( ‘|=’ ( ‘(‘ | ‘)’ | ‘[]’ | ‘<>’ | ID | ‘!’ | ‘&&’ | ‘||’ | ‘->’ | ‘<->’ | ‘/\’ | ‘/’ | ‘.’ | INT )+ ) LTL checking
| ‘deadlockfree’ deadlock testing
| ‘feasible’ feasibility testing
| ‘reachable’ ID reachability testing
| ‘=T=’ definitionRef trace equivalence
| ‘=F=’ definitionRef falure equivalence
| ‘=FD=’ definitionRef falure divergence equivalence
| ‘[T=’ definitionRef trace refinement
| ‘[F=’ definitionRef falure refinement
| ‘[FD=’ definitionRef falure divergence refinement
)
‘;’
;
definitionRef : ID actualParameterList;

alphabets definitions for CSP processes
alpha : ‘alpha’ ‘(‘ ID ‘)’ ‘=’ ‘{‘ eventName (‘,’ eventName )* ‘}’ ‘;’ ;

define : ‘#’ ‘define’ ID INT ‘;’ global Int constant declaration
| ‘#’ ‘define’ ID (‘true’ | ‘false’) ‘;’ global Boolean constant declaration
| ‘#’ ‘define’ ID conditionalOrExpression ‘;’global condition declaration, used in assertions
;

global channel declarations
channel : ‘channel’ ID additiveExpression;

statement expression
statement : block
| funExpression
| recfunExpression
| applicationExpression
| ifExpression
| whileExpression
| letExpression
| expression ‘;’!
| ‘;’!
;

block : ‘{‘ statement+ ‘}’ ;
funExpression : ‘fun’ notEmptyIdentifierList ‘->’ statement ;
notEmptyIdentifierList : ‘(‘ ID (‘,’ ID)* ‘)’;
recfunExpression :’recfun’ ID notEmptyIdentifierList ‘->’ statement;
applicationExpression : ‘(‘ expression notEmptyExpressionList ‘)’ ;
notEmptyExpressionList : expression+ ;
ifExpression : ‘if’ ‘(‘ expression ‘)’ s1=statement (‘else’ s2=statement)? ;
whileExpression : ‘while’ ‘(‘ expression ‘}’ statement ;
recordExpression : ‘[‘ expression (‘,’ expression)* ‘]’ ;
letExpression : ‘let’ letDefintion+ ‘in’ expression;
letDefintion : ID ‘=’ expression ‘;’
| ID ‘=’ recordExpression ‘;’
| ID ‘=’ funExpression ‘;’
| ID ‘=’ recfunExpression ‘;’
| ID'[‘ expression ‘]’ ‘;’ integer array with initial values 0
;

expression : conditionalOrExpression (‘=’ expression)? ;
conditionalOrExpression : conditionalAndExpression ( ‘||’ conditionalAndExpression )* ;
conditionalAndExpression : equalityExpression ( ‘&&’ equalityExpression)* ;
equalityExpression : relationalExpression ( (‘==’ |’!=’) relationalExpression)* ;
relationalExpression : additiveExpression ( (‘<‘ | ‘>’ | ‘<=’ | ‘>=’) additiveExpression)* ;
additiveExpression : multiplicativeExpression ( (‘+’ | ‘-‘) multiplicativeExpression)* ;
multiplicativeExpression : unaryExpression ( (‘*’ | ‘/’ | ‘%’ ) unaryExpression)* ;
unaryExpression : ‘+’ unaryExpression
| ‘-‘ unaryExpression
| unaryExpressionNotPlusMinus
;
unaryExpressionNotPlusMinus
: ID (‘[‘ conditionalOrExpression ‘]’)?
| INT
| ‘true’
| ‘false’
| ‘(‘ conditionalOrExpression ‘)’
| ‘!’ conditionalOrExpression negation
;

CSP process definition
definition : ID formalParameters ‘=’ ifExpr ‘;’ ;
formalParameters : ‘(‘ (ID (‘,’ ID )*)? ‘)’ ;
ifExpr : ‘if’ (ifExprCondition+ (‘else’ ifExpr)? ) ‘fi’
| interleaveExpr
;
ifExprCondition : (conditionalOrExpression ‘:’ ifExpr);

interleaveExpr : parallelExpr (‘|||’ parallelExpr)*
| ‘|||’ (paralDef (‘;’ paralDef )*) ‘@’ ifExpr
;
parallelExpr : internalChoiceExpr (‘||’ internalChoiceExpr)*
| ‘||’ (paralDef (‘;’ paralDef )*) ‘@’ ifExpr
;
paralDef : ID ‘:’ ‘{‘ additiveExpression (‘,’ additiveExpression)* ‘}’
| ID ‘:’ ‘{‘ additiveExpression ‘..’ additiveExpression ‘}’
;
internalChoiceExpr : conditionalChoiceExpr (‘<>’ conditionalChoiceExpr)*;
conditionalChoiceExpr : externalChoiceExpr ( conditionalOrExpression >> externalChoiceExpr)* ;
externalChoiceExpr : interruptExpr (‘[]’ interruptExpr)* ;
interruptExpr : hidingExpr (‘|>’ hidingExpr)*;
hidingExpr : sequentialExpr (‘\’ ‘{‘ eventM (‘,’ eventM )* ‘}’)? ;
sequentialExpr : guardExpr (‘;’ guardExpr)*;
guardExpr : channelExpr
| ‘[‘ conditionalOrExpression ‘]’ ‘@’ channelExpr
;
channelExpr : (‘wl’ | ‘sl’ | ‘sf’ | ‘wf’) ‘(‘ ID ‘!’ expression ‘)’ ‘->’ eventExpr
| (‘wl’ | ‘sl’ | ‘sf’ | ‘wf’) ‘(‘ ID ‘?’ ID ‘)’ ‘->’ eventExpr
| ID ‘!’ expression ‘->’ eventExpr
| ID ‘?’ ID ‘->’ eventExpr
| eventExpr
;

eventExpr : eventM (block)? ‘->’ eventExpr
| atom
;
atom : ID actualParameterList
| ‘Skip’ (‘(‘ ‘)’)?
| ‘Stop’ (‘(‘ ‘)’)?
| ‘(‘ ifExpr ‘)’
;

actualParameterList : ‘(‘ (expression (‘,’ expression )*)? ‘)’ ;

eventM : eventName
| (‘wl’|’sl’|’wf’|’sf’) ‘(‘ eventName ‘)’
;
eventName : ID ( ‘.’ additiveExpression)* ;

ID : (‘a’..’z’|’A’..’Z’|’_’) (‘a’..’z’|’A’..’Z’|’0′..’9’|’_’)* ;
INT : (‘0’..’9′)+ ;

COMMENT : ‘/*’ TEXT ‘*/’ ;
LINE_COMMENT : ‘‘ TEXT ‘r’? ‘n’;

OPERATOR PRECEDENCE

The operators at the top of the table bind more tightly than those lower down.

Class Operators Description Associativity


Sequential -> prefix right

; sequence left


Hiding hiding


Choice |> interrupt left

[] external choice left

<b> external choice left

<> internal choice left


Parallel || parallel left

||| interleave left

EXAMPLES

The spefication of two Dining Philoshpors:
phi0()=((t0->phi0())[](wl(g01)->(g00->(e0->(p01->(p00->phi0()))))));
f0()=((g00->(wl(p00)->f0()))[](g10->(wl(p10)->f0())));
phi1()=((t1->phi1())[](wl(g10)->(g11->(e1->(p10->(p11->phi1()))))));
f1()=((g11->(wl(p11)->f1()))[](g01->(wl(p01)->f1())));
DiningPhilosophers()=(phi0()||f0()||phi1()||f1());