berkeley.cub

type location = UnOwned | Exclusive | NonExclusive | Invalid

array A[proc] : location

init (z) { A[z] = Invalid }
 
unsafe (z1 z2) { A[z1] = Exclusive && A[z2] = Exclusive }
 
transition t1 (x)
requires { A[x] = Invalid }
{ 
  A[j] := case 
            | j = x : UnOwned 
	    | A[j] = Exclusive : NonExclusive 
	    | _ : A[j]; 
}

transition t2 (x)
requires { A[x] = UnOwned }
{ 
  A[j] := case	
           | j = x : Exclusive 
	   | A[j] = NonExclusive : Invalid 
	   | A[j] = UnOwned : Invalid 
	   | _ : A[j]; 
}
  
transition t3 (x)
requires { A[x] = NonExclusive }
{ 
  A[j] := case 
           | j = x : Exclusive 
	   | A[j] = UnOwned : Invalid 
	   | A[j] = NonExclusive : Invalid 
	   | _ : A[j]; 
}

transition t4 (x)
requires { A[x] = Invalid }
{ 
  A[j] := case 
           | j = x : Exclusive 
	   | A[j] = NonExclusive : Invalid 
	   | A[j] = Exclusive : Invalid 
	   | A[j] = UnOwned : Invalid 
	   |  _ : A[j]; 
}