MODULE
MODULE


VAR
VAR
: ;
: ;
INIT

INIT

TRANS

TRANS

INVAR

INVAR

DEFINE
DEFINE
:= ;
:= ;
ASSIGN
ASSIGN
:= ;
:= ;
init( ) init( ) boolean boolean { , } { , } ( , ) ( , ) array of array of process process . . [ ] [ ] 0 0 1 1 ( ) ( ) | | & & ! ! case
esac case
esac

: ;

: ;
next( ) next( ) + + - - * * / / mod mod = = < < > > <= <= >= >= { , } { , } .. .. - - + + ( , ) ( , )