germanish5.cub

type req = Empty | Reqs | Reqe | Inv | Invack | Gnts | Gnte
type cstate = Invalid | Shared | Exclusive

var Exgntd : bool
var Curcmd : req
var Curptr : proc

array Cache[proc] : cstate
array Shrset[proc] : bool
array Chan[proc] : req

init (z) { Cache[z] = Invalid && Shrset[z] = False &&
           Exgntd = False && Curcmd = Empty && Chan[z]=Empty }

unsafe (z1 z2) { Cache[z1] = Exclusive && Cache[z2] = Shared }

transition send_shared (n)
requires { Chan[n] = Empty && Cache[n] = Invalid }
{ 
  Chan[j] := case 
  	      | j = n : Reqs 
	      | _ : Chan[j] 
}

transition recv_shared (n)
requires { Curcmd = Empty && Chan[n] = Reqs }
{ 
  Curcmd := Reqs; 
  Curptr := n;
  Chan[j] := case 
  	      | j = n : Empty 
	      | _ : Chan[j] 
}
    
transition send_exclusive (n)
requires { Chan[n] = Empty && Cache[n] <> Exclusive }
{
  Chan[j] := case
  	      | j = n : Reqe 
	      | _ : Chan[j] 
}

transition recv_exclusive (n)
requires { Curcmd = Empty && Chan[n] = Reqe }
{ 
  Curcmd := Reqe; 
  Curptr := n;
  Chan[j] := case 
  	      | j = n : Empty 
	      | _ : Chan[j] 
}
    
transition sendinv_1 (n)
requires { Chan[n] = Empty && Shrset[n]=True  &&  Curcmd = Reqe }
{ 
  Chan[j] := case
  	      | j = n : Inv 
	      | _ : Chan[j] 
}

transition sendinv_2 (n)
requires { Chan[n] = Empty && Shrset[n]=True  &&
	   Curcmd = Reqs && Exgntd=True }
{ 
  Chan[j] := case
  	      | j = n : Inv 
	      | _ : Chan[j] 
}

transition recv_inv(n)
requires { Chan[n] = Inv }
{ 
  Chan[j] := case
  	      | j = n : Invack 
	      | _ : Chan[j] ;
  Cache[j] := case 
  	       | j = n : Invalid 
	       | _ : Cache[j] 
}
    
transition recv_invack(n)
requires { Chan[n] = Invack && Curcmd <> Empty }
{ 
  Exgntd := False;
  Chan[j] := case 
  	      | j = n : Empty 
	      | _ : Chan[j];
  Shrset[j] := case 
  	        | j = n : False 
		| _ : Shrset[j] 
}

transition send_gnt_shared(n)
requires { Curptr = n && Curcmd = Reqs && 
	   Exgntd = False && Chan[n] = Empty }
{ 
  Curcmd := Empty;
  Chan[j] := case 
  	      | j = n : Gnts 
	      | _ : Chan[j];
  Shrset[j] := case 
  	        | j = n : True 
		| _ : Shrset[j] 
}

transition send_gnt_exclusive(n)
requires { Curptr = n && Curcmd = Reqe && Chan[n] = Empty && 
	   forall_other j.  Shrset[j] = False }
{ 
  Curcmd := Empty; 
  Exgntd := True;
  Chan[j] := case 
  	      | j = n : Gnte 
	      | _ : Chan[j];
  Shrset[j] := case 
  	       	| j = n : True 
		| _ : Shrset[j] 
}

transition recv_gnt_shared(n)
requires {Chan[n] = Gnts}
{ 
  Cache[j] := case 
  	       | j = n : Shared 
	       | _ : Cache[j];
  Chan[j] := case 
  	       | j = n : Empty 
	       | _ : Chan[j] 
}

transition recv_gnt_exclusive(n)
requires { Chan[n] = Gnte }
{ 
  Cache[j] := case 
  	       | j = n : Exclusive 
	       | _ : Cache[j];
  Chan[j] := case
  	      | j = n : Empty 
	      | _ : Chan[j] 
}