model futurbus {

var 
     sharedU,
     exclusiveU,
     exclusiveM,
     invalid,
     pendingW,
     pendingR,
     pendingEMR,
     pendingSU,
     pendingEMW ;	


states ss;


transition r2 := { 
	from:= ss;
	to :=   ss;
         guard :=
           invalid >= 1 && pendingW=0
	;
         action := 
	      invalid'=invalid-1,
	      sharedU'=0,
	      exclusiveU'=0,
	      exclusiveM'=0,    
              pendingR'=pendingR+1,
	      pendingEMR'=pendingEMR+exclusiveM,
	      pendingSU'=sharedU+exclusiveU+pendingSU
;
};	      

transition r3  := { 
	from:= ss;
	to :=   ss;
       		guard:=      pendingEMR >=1
	;
         action := 
	      sharedU'=sharedU+pendingR+1,
	      pendingR'=0,	      
	      pendingEMR'=pendingEMR-1
;
};

transition r4  := {        
	from:= ss;
	to :=   ss;
        	guard:=   pendingR=1   && pendingEMR =0  && pendingSU=0  
	;
         action := 
	   exclusiveU'=exclusiveU+1,
	   pendingR'=0 
;
};

transition r5  := {
	from:= ss;
	to :=   ss;
        guard:=   	pendingR>=2   && pendingEMR =0  && pendingSU=0              
	;
         action :=   
	      	pendingR' = 0,    
	       	sharedU'=sharedU+pendingR	 	
;
};
         
transition r6  := {
	from:= ss;
	to :=   ss;
        	guard:=   	pendingSU >=1
	;
         action :=  
	        sharedU'=sharedU+pendingSU+pendingR,
		pendingR'=0,
		pendingSU'=0
;
};
          

transition r7  := {
	from:= ss;
	to :=   ss;
	guard:=           	invalid>=1 && pendingW=0
	;
         action := 
	  	pendingW'=1,
	   	invalid'=invalid + sharedU+ exclusiveU+pendingR+pendingSU+pendingEMR-1,
	  	pendingEMW'=pendingEMW+ exclusiveM,
		sharedU'=0,
		exclusiveU'=0,
		exclusiveM'=0,
		pendingR'=0,
		pendingSU'=0,
		pendingEMR'=0
;
};
	  

transition r8  := {
	from:= ss;
	to :=   ss;
        guard:=   	pendingEMW=0
	;
         action :=  
	        exclusiveM'= exclusiveM + pendingW,
		pendingW'=0
;
};

transition r9  := {
	from:= ss;
	to :=   ss;
	guard:=           	sharedU >=1
	;
         action := 
	        invalid'=invalid+sharedU-1,
		sharedU'=0,
		exclusiveM'=exclusiveM+1
;
};

transition r10  := {
	from:= ss;
	to :=   ss;
	guard:=
           	exclusiveU >=1 
	;
         action := 
	        exclusiveU'=exclusiveU-1,
		exclusiveM'=exclusiveM+1
;
};

}

strategy s1 {

setMaxState(0);
setMaxAcc(100);


Region init :=
	{state=ss && sharedU=0 && exclusiveU=0 && exclusiveM=0 && invalid>0 &&
	pendingW=0 &&	pendingR=0 && 	pendingEMR=0 && pendingSU=0 && 	pendingEMW=0 	};

Transitions t := {r2,r3,r4,r5,r6,r7,r8,r9,r10};

Region reach := post*(init, t);

	
}