xerox_dragon.cub

(* from "Regular Model Checking without Transducers 
         (on efficient verification of parameterized systems)"
   	Adulla et. al.
	Tech report 2006-052 Uppsala Universitet
*)

type t = Invalid | SClean | SDirty | Exclusive | Dirty

array A[proc] : t

init (z) { A[z] = Invalid }

unsafe (z1 z2) { A[z1] = Dirty && A[z2] = SClean }
unsafe (z1 z2) { A[z1] = Dirty && A[z2] = SDirty }
unsafe (z1 z2) { A[z1] = Dirty && A[z2] = Exclusive }
unsafe (z1 z2) { A[z1] = Dirty && A[z2] = Dirty }
unsafe (z1 z2) { A[z1] = Exclusive && A[z2] = Exclusive }

transition t1 (x)
requires { A[x] = SDirty && 
	   forall_other j. (A[j] <> SClean && A[j] <> SDirty) }
{
 A[j] := case 
      	  | j = x : Dirty
	  | _ : A[j]
}

transition t2 (x)
requires { A[x] = Invalid && forall_other j. A[j] = Invalid }
{
 A[j] := case 
      	  | j = x : Exclusive
	  | _ : A[j]
}

transition t3 (x)
requires { A[x] = SClean &&
	   forall_other j. ( A[j] <> SClean && A[j] <> SDirty) }
{
 A[j] := case 
      	  | j = x : Dirty
	  | _ : A[j]
}

transition t4 (x)
requires { A[x] = Invalid && forall_other j. A[j] = Invalid }
{
 A[j] := case 
      	  | j = x : Dirty
	  | _ : A[j]
}

transition t5_1 (x y)
requires { A[x] = SDirty && A[y] = SClean }
{
 A[j] := case 
      	  | j = x : SDirty
	  | A[j] = SDirty : SClean
	  | _ : A[j]
}


transition t5_2 (x y)
requires { A[x] = SDirty && A[y] = SDirty }
{
 A[j] := case 
      	  | j = x : SDirty
	  | A[j] = SDirty : SClean
	  | _ : A[j]
}

transition t6 (x)
requires { A[x] = Exclusive }
{
 A[j] := case 
      	  | j = x : Dirty
	  | _ : A[j]
}

transition t7_1 (x y)
requires { A[x] = SClean && A[y] = SClean }
{
 A[j] := case 
      	  | j = x : SDirty
	  | A[j] = SDirty : SClean
	  | _ : A[j]
}


transition t7_2 (x y)
requires { A[x] = SClean && A[y] = SDirty }
{
 A[j] := case 
      	  | j = x : SDirty
	  | A[j] = SDirty : SClean
	  | _ : A[j]
}

transition t8 (x y)
requires { A[x] = Invalid && A[y] <> Invalid }
{
 A[j] := case 
          | j = x : SClean
	  | A[j] = Dirty : SDirty
	  | A[j] = Exclusive : SClean
	  | _ : A[j]
}

transition t9 (x y)
requires { A[x] = Invalid && A[y] <> Invalid }
{
 A[j] := case
      	  | j = x : SDirty
	  | A[j] <> Invalid : SClean
	  | _ : A[j]
}