german_pfs_data_enum.cub

(*
 :comment      SOURCE: pfs distribution
 :comment      (difficult version)

 :smt (define-type locations (subrange 1 3))
 :smt (define-type messages1  (subrange 5 7))
 :smt (define-type messages2  (subrange 7 10))
 :comment   values 5, 11 for t[x] are mapped to false and  true, resp.
 :comment   value 5 for d[x] is mapped to  7
*)

type state = Invalid | Shared | Exclusive
(*
	 Invalid -> 1
	 Shared -> 2
	 Exclusive -> 3
*)

type msg1 = Empty1 | Reqs | Reqe 
(*
	Empty1 -> 5
	Reqs -> 6
	Reqe -> 7

*)

type msg2 = Empty2 | Inv | Gnts | Gnte
(*
	Empty2 -> 7
	Gnts -> 8
	Gnte -> 9
	Inv -> 10

*)

type msg3 = Empty3 | Invack
(*
	Empty3 -> true
	Invack -> false
*)


(*
:local a locations
:local u messages1
:local d messages2
:local t bool
:local c bool
:local s bool
:local l bool
:global g bool
:global m messages1
:global f bool

*)

type data = Data1 | Data2

var Exgntd : bool
var Curcmd : msg1
var Flag : bool

var MemData : data
var AuxData : data
var Store_data : data

array CacheState[proc] : state
array CacheData[proc] : data

array Chan1Cmd[proc] : msg1
array Chan1Data[proc] : data

array Chan2Cmd[proc] : msg2
array Chan2Data[proc] : data

array Chan3Cmd[proc] : msg3
array Chan3Data[proc] : data


array Curptr[proc] : bool
array Shrset[proc] : bool
array Invset[proc] : bool


init (z) {
     CacheState[z] = Invalid &&
     Chan1Cmd[z] = Empty1 && 
     Chan2Cmd[z] = Empty2 &&
     Chan3Cmd[z] = Empty3 && 
     Curptr[z] = False && 
     Shrset[z] = False && 
     Invset[z] = False &&
     Exgntd = False && 
     Curcmd = Empty1 && 
     Flag = False &&
     MemData = Data1 && (* oblige de mettre ca sinon   *)
     AuxData = Data1    (* ca foire a cause des gardes *)
     	       		(* universelles (approx.)      *)
			&& Store_data = Data1 
}



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


(* Data *)
unsafe () { Exgntd = False && MemData <> AuxData }
unsafe (z) { CacheState[z] <> Invalid && CacheData[z] <> AuxData }






(*:comment c1    t10*)
transition send_req_shared(x)
requires { CacheState[x] = Invalid && Chan1Cmd[x] = Empty1 && Flag = False }
{
  CacheState[j] := case | j = x : Invalid | _ : CacheState[j] ;
  Chan1Cmd[j] := case | j = x : Reqs | _ : Chan1Cmd[j] ;
}


(*:comment c2 - c3     t11*)
transition send_req_exclusive(x)
requires { CacheState[x] <> Exclusive && Chan1Cmd[x] = Empty1 && Flag = False }
{ Chan1Cmd[j] := case | j = x : Reqe | _ : Chan1Cmd[j] }



(*:comment h2  t3*)
transition recv_req_shared(x)
requires { Curcmd = Empty1 && Chan1Cmd[x] = Reqs && Flag = False }
{ 
  Flag := True ; 
  (* Invset := Shrset ;  *)
  Invset[j] := case | _ : Shrset[j];
  Curcmd := Reqs;
  Chan1Cmd[j] := case | j = x : Empty1 | _ : Chan1Cmd[j] ;
  Curptr[j] := case | j = x : True | _ : False 
}

(*:comment h2  t3*)
transition recv_req_exclusive(x)
requires { Curcmd = Empty1 && Chan1Cmd[x] = Reqe && Flag = False }
{ 
  Flag := True ; 
  (* Invset := Shrset ;  *)
  Invset[j] := case | _ : Shrset[j];
  Curcmd := Reqe;
  Chan1Cmd[j] := case | j = x : Empty1 | _ : Chan1Cmd[j] ;
  Curptr[j] := case | j = x : True | _ : False 
}


(*:comment h4    t8*)
transition send_inv_1(x)
requires { Curcmd = Reqe && Invset[x] = True && 
	   Chan2Cmd[x] = Empty2 && Flag = False }
{ 
  Chan2Cmd[j] := case | j = x : Inv | _ : Chan2Cmd[j] ;
  Invset[j] := case | j = x : False | _ : Invset[j] ;
}


(*:comment h3    t7*)
transition send_inv_2(x)
requires { Curcmd = Reqs && Exgntd = True && Invset[x] = True &&
	   Chan2Cmd[x] = Empty2 && Flag = False }
{
  Chan2Cmd[j] := case | j = x : Inv | _ : Chan2Cmd[j] ;
  Invset[j] := case | j = x : False | _ : Invset[j] ;
}


(*:comment c4         t12*)
transition send_invack_noex(x)
requires { Chan2Cmd[x] = Inv && Chan3Cmd[x] = Empty3 &&
	   Flag = False && CacheState[x] <> Exclusive }
{ 
  CacheState[j] := case | j = x : Invalid | _ : CacheState[j] ;
  Chan2Cmd[j] := case | j = x : Empty2 | _ : Chan2Cmd[j] ;
  Chan3Cmd[j] := case | j = x : Invack | _ : Chan3Cmd[j] 
}

(*:comment c4         t12*)
transition send_invack_ex(x)
requires { Chan2Cmd[x] = Inv && Chan3Cmd[x] = Empty3 &&
	   Flag = False && CacheState[x] = Exclusive }
{ 
  CacheState[j] := case | j = x : Invalid | _ : CacheState[j] ;
  Chan2Cmd[j] := case | j = x : Empty2 | _ : Chan2Cmd[j] ;
  Chan3Cmd[j] := case | j = x : Invack | _ : Chan3Cmd[j] ;
  Chan3Data[j] := case | j = x : CacheData[x] | _ : Chan3Data[j] ;
}



(*:comment h5   t9*)
transition recv_invack_noex(x)
requires { Curcmd <> Empty1 && Chan3Cmd[x] = Invack && Flag = False &&
	   Exgntd = False }
{ Chan3Cmd[j] := case | j = x : Empty3 | _ : Chan3Cmd[j] ;
  Shrset[j] := case | j = x : False | _ : Shrset[j] 
}

(*:comment h5   t9*)
transition recv_invack_ex(x)
requires { Curcmd <> Empty1 && Chan3Cmd[x] = Invack && Flag = False &&
	   Exgntd = True }
{ Exgntd := False;
  Chan3Cmd[j] := case | j = x : Empty3 | _ : Chan3Cmd[j] ;
  Shrset[j] := case | j = x : False | _ : Shrset[j] ;
  MemData := Chan3Data[x];
}


(*:comment h0    t1*)
transition send_gnt_shared(x)
requires { Curcmd = Reqs && Exgntd = False && Chan2Cmd[x] = Empty2 &&
	   Curptr[x] = True && Flag = False }
{ Curcmd := Empty1 ;
  Chan2Cmd[j] := case | j = x : Gnts | _ : Chan2Cmd[j] ;
  Chan2Data[j] := case | j = x : MemData | _ : Chan2Data[j] ;
  Shrset[j] := case | j = x : True | _ : Shrset[j] ;
}


(*:comment h1    t2*)
transition send_gnt_exclusive(x)
requires { Shrset[x] = False && Curcmd = Reqe && Chan2Cmd[x] = Empty2 &&
	   Curptr[x] = True && Flag = False &&
           forall_other j. Shrset[j] = False}
{ Curcmd := Empty1 ; Exgntd := True ;
  Chan2Cmd[j] := case | j = x : Gnte | _ : Chan2Cmd[j] ;
  Chan2Data[j] := case | j = x : MemData | _ : Chan2Data[j] ;
  Shrset[j] := case | j = x : True | _ : Shrset[j] ;
}



(*:comment c5   t13*)
transition recv_gnt_shared(x)
requires { Chan2Cmd[x] = Gnts && Flag = False }
{ 
  CacheState[j] := case | j = x : Shared | _ : CacheState[j] ;
  CacheData[j] := case | j = x : Chan2Data[x] | _ : CacheData[j] ;
  Chan2Cmd[j] := case | j = x : Empty2 | _ : Chan2Cmd[j] 
}


(*:comment c6    t14*)
transition recv_gnt_exclusive(x)
requires { Chan2Cmd[x] = Gnte && Flag = False }
{
  CacheState[j] := case | j = x : Exclusive | _ : CacheState[j] ;
  CacheData[j] := case | j = x : Chan2Data[x] | _ : CacheData[j] ;
  Chan2Cmd[j] := case | j = x : Empty2 | _ : Chan2Cmd[j] 
}




(*:comment n1   t4 t5 *)
transition sh_to_inv_pending(x)
requires { Flag = True }
{ Invset[j] := case | j = x : Shrset[x] | _ : Invset[j] }


(*:comment n3   t6*)
transition sh_to_inv_finished(x)
requires { Flag = True && Invset[x] = Shrset[x] 
           && forall_other j. Invset[j] = Shrset[j] }
{ Flag := False }



(* transition store (x) *)
(* requires { CacheState[x] = Exclusive } *)
(* { *)
(*   AuxData := Store_data; *)
(*   CacheData[j] := case  *)
(*     	       	  | j = x : Store_data *)
(* 	       	  | _  : CacheData[j]; *)
(* } *)

transition store1 (x)
requires { CacheState[x] = Exclusive }
{
  AuxData := Data1;
  CacheData[j] := case 
    	       	  | j = x : Data1
	       	  | _  : CacheData[j];
}

transition store2 (x)
requires { CacheState[x] = Exclusive }
{
  AuxData := Data2;
  CacheData[j] := case 
    	       	  | j = x : Data2
	       	  | _  : CacheData[j];
}