model consistencyprotocol {

var   Idle,ServeS,GrantS,ServeE,GrantE,ex,Null,WaitS,WaitE,Shared,Exclusive;

states e0;


transition reqS := {
	from :=e0;
	to:=e0;
	guard :=
		Idle>=1 && Null>=1 
	;
	action :=         
	  Idle' = Idle - 1,
          ServeS' = ServeS + 1,
          Null' = Null - 1,
          WaitS' = WaitS + 1
	;
};
  	      
transition inv1 := {
	from :=e0;
	to:=e0;
	guard :=
 	  ServeS >= 1 && ex = 1 && Exclusive >= 1          	 
	;
	action :=
          ServeS' = ServeS - 1,
          GrantS' = GrantS + 1,
          ex' = 0,
          Exclusive' = Exclusive - 1,
          Null' = Null + 1
	;
};


transition inv2 := {
	from :=e0;
	to:=e0;
	guard :=
		ServeE>=1
	;
	action :=
          ServeE' = ServeE - 1,
          GrantE' = GrantE + 1,
          Null' = Null + Shared + Exclusive,
          Shared' = 0,
          Exclusive' = 0
	;
};

transition nonex := {
	from :=e0;
	to:=e0;
	guard :=
	  ServeS >= 1 && ex = 0
	;
	action :=
          ServeS' = ServeS - 1,
          GrantS' = GrantS + 1
	;
};
	
transition grantS := {
	from :=e0;
	to:=e0;
	guard :=
	  GrantS >= 1 && WaitS >= 1
	;
	action :=
          GrantS' = GrantS - 1,
          Idle' = Idle + 1,
          WaitS' = WaitS - 1,
          Shared' = Shared + 1
	;
};

transition reqE1 := {
	from :=e0;
	to:=e0;
	guard :=
	  Idle >= 1 && Null >= 1
	;
	action :=
          Idle' = Idle - 1,
          ServeE' = ServeE + 1,
          Null' = Null - 1,
          WaitE' = WaitE + 1
	;
};

transition reqE2 := {
	from :=e0;
	to:=e0;
	guard :=
	  Idle >= 1 && Shared >= 1
	;
	action :=
          Idle' = Idle - 1,
          ServeE' = ServeE + 1,
          Shared' = Shared - 1,
          WaitE' = WaitE + 1
	;
};

transition grantE := {
	from :=e0;
	to:=e0;
	guard :=
	  GrantE >= 1 && WaitE >= 1
	;
	action :=
          GrantE' = GrantE - 1,
          Idle' = Idle + 1,
          WaitE' = WaitE - 1,
          Exclusive' = Exclusive + 1,
          ex' = 1
	;
};

}

strategy s1 {

setMaxState(0);
setMaxAcc(100);


Region init :=
	{state=e0 && Idle=1 && ServeS=0 && GrantS=0 && ServeE=0 && GrantE =0 &&
	 ex=0 && Null>=1 && WaitS=0 && WaitE=0 && Shared=0 && Exclusive=0};

Transitions t := {reqS, inv1, inv2, grantS, reqE1, reqE2, grantE};

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

	
}