germanish.cub

type msg = Empty | Reqs | Reqe
type state = Invalid | Shared | Exclusive

var Exgntd : bool
var Curcmd : msg
var Curptr : proc

array Cache[proc] : state
array Shrset[proc] : bool

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

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


transition req_shared (n)
requires { Curcmd = Empty && Cache[n] = Invalid }
{ 
  Curcmd := Reqs; 
  Curptr := n ;
}
    
transition req_exclusive (n)
requires { Curcmd = Empty && Cache[n] <> Exclusive }
{ 
  Curcmd := Reqe; 
  Curptr := n;
}
    
transition inv_1 (n)
requires { Shrset[n]=True  &&  Curcmd = Reqe }
{ 
  Exgntd := False;
  Cache[n] := Invalid;
  Shrset[n] :=False;
}

transition inv_2 (n)
requires { Shrset[n]=True  && Curcmd = Reqs && Exgntd=True }
{ 
  Exgntd := False;
  Cache[n] := Invalid;
  Shrset[n] := False;
}
    
transition gnt_shared (n)
requires { Curptr = n && Curcmd = Reqs && Exgntd = False }
{ 
  Curcmd := Empty;
  Shrset[n] := True;
  Cache[n] := Shared;
}

transition gnt_exclusive (n)
requires { Shrset[n] = False && Curcmd = Reqe &&
           Exgntd = False && Curptr = n &&
	   forall_other l. Shrset[l] = False }
{ 
  Curcmd := Empty; 
  Exgntd := True;
  Shrset[n] := True;
  Cache[n] := Exclusive;
}