/* edited by Yan Rongjie */
/*    general instructions   */
//---------------------------------------------------------------------
The model should be compiled firstly:
Compiler example.cta
This command creates a file: example.obj
Then the property example.pro will be compiled by the propery compiler:
prop example.pro
This command will update the obj file by adding property information.
With the updated obj file, verifier can be executed:
ReachModelChecker example.obj
//---------------------------------------------------------------------
Attentation:
If no property is compiled, the verifier will explore the whole state space.

//---------------------------------------------------------------------
There are some options on ReachModelChecker:
ReachModelChecker filename.obj [option]

	-t: the property is on clock valuations;
	-p: print the DSs during the verification;
	-n: don't use location based maximal lower and upper bounds expolation;
//---------------------------------------------------------------------	
The grammar for model description:

Model ::= ¡®module¡¯ [ID] ¡®{¡¯ [GlobalDec] Body[ ¡®,¡¯ Body]* ¡®}¡¯
Body ::= ¡®process¡¯ ID ¡®{¡¯ [InnerDecls] SubBody¡®}¡¯

GlobalDecl  ::= (GlobalVariableDecls | ChannelDecls )*
ConstantDecls ::= 'const' ConstantDecl (',' ConstantDecl)* ';'
ConstantDecl  ::= ID '=' NUM  
ChannelDecls ::=£¨'channel' | 'broadcast'£©ID,(',' ID)* ';'

GloType::= 'int' Range| 'bool' 

VarDecl::=GloType ID (¡®,¡¯ ID)*¡¯;¡¯
VarDecls::=VarDecl(¡®,¡¯ VarDecl)*¡¯;¡¯
Declaration::= VarDecls | ConstantDecls
GlobalVariableDecls ::= 'global ' Declaration (',' Declaration)* ';'

Range       ::= '[' NUM ',' NUM ']'		
Inner::= GloType| ¡®clock¡¯ range	|¡¯inspect¡¯
InnerDecl::=Inner ID (¡®,¡¯ ID)*¡¯;¡¯
InnerDecls::= ¡®Declaration:¡¯	InnerDecl(¡®,¡¯ InnerDecl)*¡¯;¡¯

SubBody ::= ItemList
ItemList ::= ¡®Location:¡¯ (Location)+ | ¡®Transition:¡¯ (Edge)+ | ¡®init:¡¯ ID
Location :: = ID ¡®:(¡® [ID ¡¯;¡¯] [ComparisonExp] ¡®);¡¯
Edge :: = ID ¡®->¡¯ ID ¡®:(¡¯ [¡®urgent¡¯] [ComparisonExp]) ¡®;¡¯ [SynchExp] ¡®;¡¯ [AssignExp] ¡®);¡¯

SynchExp ::= ID('!' | '?')							
	
AssignExp	::£½	AssignExpSub(¡®,¡¯AssignExpSub)*
AssignExpSub	::=ID Assign Expression 	
Expression::= NUM | ID | Expression Operation Expression | Unary Expression | ComparisonExpSub £¿Expression : Expression	
Unary::= '+' | '-' | '!' | 'not'
Operation::=¡¯+¡¯|¡¯-¡¯|¡¯*¡¯|¡¯/¡¯|¡¯%¡¯
ComparisonExp::= ComparisonExpSub(¡®,¡¯ComparisonExpSub)*
ComparisonExpSub ::= Expression Comparison Expression

Assign ::= ':='
Comparison::= '<' | '<=' | '==' | '!=' | '>=' | '>'
ID ::=[a-z,A-Z]([a-z,A-Z,0-9,_])*
Binary::=  '&' | '|'	
NUM	::=Number([0-9])*|0   
NUMBER :: =1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9      

//---------------------------------------------------------------------
//------an example of fischer's mutual example
          
module Fischer {
int k[7];
const a=4,b=2;
process p1{
//-------Declaration: 
clock x[5];
//-------Location:
l0: (idle; );
l1: (req; x<a);
l2: (wait; );
l3: (critical; );
//--------Transition:
l0 -> l1: (k=0; ; x:=0);
l1 -> l2: (; ; k:=1,x:=0);
l2 -> l3: (k=1,x>=b ; ;);
l2 -> l0: (k!=1,x>=b; ;);
l3 -> l0: ( ; ; k:=0);
//--------Initial locaiton
init l0;
}
}