Spin Version 3.0 -- Promela Grammar Definition

The following list defines the grammar of the input language for the SPIN model checker version 3.0. The notational conventions are as follows.

• Choices are separated by vertical bars: |
• Optional parts are included in square brackets: [ ... ]
• A Kleene star * indicates zero or more repetitions of the immediately preceding fragment
• Literals are enclosed in single quotes: ' ... '
• Uppercase names refer to tokens (i.e., terminals) representing keywords. In Promela models, the keywords are spelled like these token names, but in lowercase instead of uppercase.
• Lowercase names refer to grammar rules from this list.

The statement separator used in this list is the semi-colon ';'. In most cases the semi-colon can be replaced with a two-character arrow symbol: '->', without change of meaning.

In the list that follows all non-terminals are linked to the production rule where they are defined, and all terminals are linked to the online man-pages for the defining elements of the language.

Grammar Rules

spec	: module [ module ] *



module	: proctype	/* proctype declaration */

	| init		/* init process         */

	| never		/* never claim          */

	| trace		/* event trace, 3.0 only*/

	| utype		/* user defined types   */

	| mtype		/* mtype declaration    */

	| decl_lst	/* global vars, chans   */



proctype: [ active ] PROCTYPE name '(' [ decl_lst ]')'

	  [ priority ] [ enabler ] '{' sequence '}'



init	: INIT [ priority ] '{' sequence '}'



never	: NEVER	'{' sequence '}'



trace	: TRACE '{' sequence '}'



utype	: TYPEDEF name '{' decl_lst '}'



mtype	: MTYPE [ '=' ] '{' name [ ',' name ] * '}'



decl_lst: one_decl [ ';' one_decl ] *



one_decl: [ visible ] typename  ivar [',' ivar ] *



typename: BIT | BOOL | BYTE | SHORT | INT | MTYPE | CHAN

	| uname	/* user defined type names (see utype) */



active  : ACTIVE [ '[' const ']' ]	/* instantiation */



priority: PRIORITY const	/* simulation priority */



enabler : PROVIDED '(' expr ')'	/* execution constraint */



visible	: HIDDEN | SHOW



sequence: step [ ';' step ] *



step    : stmnt	[ UNLESS stmnt ]

	| decl_lst

	| XR varref [',' varref ] *

	| XS varref [',' varref ] *



ivar    : name [ '[' const ']' ] [ '=' any_expr | '=' ch_init ]



ch_init : '[' const ']' OF '{' typename [ ',' typename ] * '}'



varref	: name [ '[' any_expr ']' ] [ '.' varref ]



send    : varref '!' send_args		/* normal fifo send */

	| varref '!' '!' send_args	/* sorted send */



receive : varref '?' recv_args		/* normal receive */

	| varref '?' '?' recv_args	/* random receive */

	| varref '?' '<' recv_args '>'	/* poll with side-effect */

	| varref '?' '?' '<' recv_args '>'	/* ditto */



poll    : varref '?' '[' recv_args ']'	/* poll without side-effect */

	| varref '?' '?' '[' recv_args ']'	/* ditto */



send_args: arg_lst | any_expr '(' arg_lst ')'



arg_lst  : any_expr [ ',' any_expr ] *



recv_args: recv_arg [ ',' recv_arg ] *  |  recv_arg '(' recv_args ')'



recv_arg : varref | EVAL '(' varref ')' | [ '-' ] const



assign  : varref '=' any_expr	/* standard assignment */

	| varref '+' '+'	/* increment */

	| varref '-' '-'	/* decrement */



stmnt	: IF options FI		/* selection */

	| DO options OD		/* iteration */

	| ATOMIC '{' sequence '}'	/* atomic sequence */

	| D_STEP '{' sequence '}'	/* deterministic atomic */

	| '{' sequence '}'	/* normal sequence */

	| send

	| receive

	| assign

	| ELSE			/* used inside options */

	| BREAK			/* used inside iterations */

	| GOTO name

	| name ':' stmnt	/* labeled statement */

	| PRINT '(' string [ , arg_lst ] ')'

	| ASSERT expr    

	| expr			/* condition */



options : ':' ':' sequence [ ':' ':' sequence ] *



andor	: '&' '&' | '|' '|'



binarop	: '+' | '-' | '*' | '/' | '%' | '&' | '^' | '|'

	| '>' | '<' | '>' '=' | '<' '=' | '=' '=' | '!' '='

	| '<' '<' | '>' '>' | andor



unarop	: '~' | '-' | '!'



any_expr: '(' any_expr ')'

	| any_expr binarop any_expr

	| unarop any_expr

	| '(' any_expr '-' '>' any_expr ':' any_expr ')'

	| LEN '(' varref ')'	/* nr of messages in chan */

	| poll

	| varref

	| const 

	| TIMEOUT

	| NP_			/* non-progress system state */

	| ENABLED '(' any_expr ')'		/* refers to a pid */

	| PC_VAL '(' any_expr ')'		/* refers to a pid */

	| name '[' any_expr ']' '@' name	/* refers to a pid */

	| RUN name '(' [ arg_lst ] ')' [ priority ]



expr	: any_expr

	| '(' expr ')'

	| expr andor expr

	| chanpoll '(' varref ')'	/* may not be negated */



chanpoll: FULL | EMPTY | NFULL | NEMPTY



string	: '"' [ any_ascii_char ] * '"'



uname	: name



name	: alpha [ alpha | number ] *



const	: TRUE | FALSE | SKIP | number [ number ] *



alpha	: 'a' | 'b' | 'c' | 'd' | 'e' | 'f' | 'g' | 'h' | 'i' | 'j'

	| 'k' | 'l' | 'm' | 'n' | 'o' | 'p' | 'q' | 'r' | 's' | 't'

	| 'u' | 'v' | 'w' | 'x' | 'y' | 'z'

	| 'A' | 'B' | 'C' | 'D' | 'E' | 'F' | 'G' | 'H' | 'I' | 'J'

	| 'K' | 'L' | 'M' | 'N' | 'O' | 'P' | 'Q' | 'R' | 'S' | 'T'

	| 'U' | 'V' | 'W' | 'X' | 'Y' | 'Z'

	| '_'



number	: '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9'