(*************************************************************************)
(* Cache Coherence Protocol (Steve German, 2001)                         *)
(*************************************************************************)
(*                                                                       *)
(* Extracted from:                                                       *)
(*                                                                       *)
(* Kai Baukus, Yassine Lakhnech, and Karsten Stahl. 2002. Parameterized  *)
(* Verification of a Cache Coherence Protocol: Safety and Liveness. In   *)
(* Revised Papers from the Third International Workshop on Verification, *)
(* Model Checking, and Abstract Interpretation (VMCAI '02), Agostino     *)
(* Cortesi (Ed.). Springer-Verlag, London, UK, UK, 317-330.              *)
(*************************************************************************)

(*

ExGntd   |------|                                 |-----------|
CurCmd   |      | <-- Chan1 (excl/shared req.) -- |           |  Invalide/
CurPtr   | Home | --- Chan2 (grants or inv.) ---> | Client(i) |  Shared/
InvSet   |      | <-- Chan3 (inv. ack) ---------- |           |  Exclusive
ShrSet   |------|                                 |-----------|

*)

type state = Invalid | Shared | Exclusive
type msg = Empty | Reqs | Reqe | Inv | Invack | Gnts | Gnte

var Exgntd : bool
var Curcmd : msg
var CurClient : proc

array Chan1[proc] : msg
array Chan2[proc] : msg
array Chan3[proc] : msg
array Cache[proc] : state
array Invset[proc] : bool
array Shrset[proc] : bool

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

(*unsafe (z1 z2) { Cache[z1] = Exclusive && Cache[z2] = Shared  }*)
(*unsafe (z1 z2) { Cache[z1] = Exclusive && Cache[z2] = Exclusive }*)
unsafe (z1 z2) { Cache[z1] = Exclusive && Cache[z2] <> Invalid }


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

transition send_req_exclusive_1(n)
requires { Cache[n] = Invalid && Chan1[n] = Empty }
{ 
  Chan1[j] := case
               | j = n : Reqe 
               | _ : Chan1[j] ;
}

transition send_req_exclusive_2(n)
requires { Cache[n] = Shared && Chan1[n] = Empty }
{
  Chan1[j] := case 
               | j = n : Reqe 
               | _ : Chan1[j] ;
}

transition recv_req_shared(n)
requires { Curcmd = Empty && Chan1[n] = Reqs }
{ 
  Curcmd := Reqs; 
  CurClient := n; 
  Invset[j] := case | _ : Shrset[j];
  Chan1[j] := case 
               | j = n: Empty 
               | _ : Chan1[j];
}

transition recv_req_exclusive(n)
requires { Curcmd = Empty && Chan1[n] = Reqe }
{ 
  Curcmd := Reqe; 
  CurClient := n; 
  Invset[j] := case | _ : Shrset[j];
  Chan1[j] := case 
               | j = n : Empty 
               | _ : Chan1[j] ;
}

transition send_inv_1(n)
requires { Chan2[n] = Empty && Invset[n] = True && Curcmd = Reqe }
{ 
  Chan2[j] := case
               | j = n : Inv 
               | _ : Chan2[j] ;
  Invset[j] := case
               | j = n : False 
               | _ : Invset[j];
}

transition send_inv_2(n)
requires { Chan2[n] = Empty && Invset[n] = True && 
          Curcmd = Reqs && Exgntd = True}
{ 
  Chan2[j] := case
               | j = n : Inv 
               | _ : Chan2[j] ;
  Invset[j] := case 
               | j = n : False 
               | _ : Invset[j] ;
}

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

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

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

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

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