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’;

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());