german_pfs2.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

*)


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

array Cache[proc] : state
array Chan1[proc] : msg1
array Chan2[proc] : msg2
array Chan3[proc] : msg3
array Curptr[proc] : bool
array Shrset[proc] : bool
array Invset[proc] : bool


init (z) {
     Cache[z] = Invalid &&
     Chan1[z] = Empty1 && 
     Chan2[z] = Empty2 &&
     Chan3[z] = Empty3 && 
     Curptr[z] = False && 
     Shrset[z] = False && 
     Invset[z] = False &&
     Exgntd = False && 
     Curcmd = Empty1 && 
     Flag = 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 }



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


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


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

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

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


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


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


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


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


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



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


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



(*:comment c4         t12*)
transition t12(x)
requires { Chan2[x] = Inv && Chan3[x] = Empty3 && Flag = False }
{ 
  Cache[j] := case | j = x : Invalid | _ : Cache[j] ;
  Chan2[j] := case | j = x : Empty2 | _ : Chan2[j] ;
  Chan3[j] := case | j = x : Invack | _ : Chan3[j] 
}


(*:comment c5   t13*)
transition t13(x)
requires { Chan2[x] = Gnts && Flag = False }
{ 
  Cache[j] := case | j = x : Shared | _ : Cache[j] ;
  Chan2[j] := case | j = x : Empty2 | _ : Chan2[j] 
}


(*:comment c6    t14*)
transition t14(x)
requires { Chan2[x] = Gnte && Flag = False }
{
  Cache[j] := case | j = x : Exclusive | _ : Cache[j] ;
  Chan2[j] := case | j = x : Empty2 | _ : Chan2[j] 
}