illinois.cub

type location = L1 | L2 | L3 | L4

array A[proc] : location

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

unsafe (z1 z2) { A[z1] = L3 && A[z2] = L2 }

transition t1 (x y)
requires { A[x] = L1 && A[y] = L2 }
{ A[j] := case | j = x : L3 | j = y : L3 | _ : A[j]; }

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

transition t3 (x)
requires { A[x] = L1 }
{ A[j] := case
 | j = x : L2
 | A[j] = L2 : L1
 | A[j] = L3 : L1
 | A[j] = L4 : L1
 | _ : A[j];
}

transition t4 (x)
requires { A[x] = L2 }
{ A[j] := case | j = x : L1 | _ : A[j]; }

transition t5 (x y)
requires { A[x] = L1 && A[y] = L3 }
{ A[j] := case | j = x : L3 | A[j] = L4 : L3 | _ : A[j]; }

transition t5bis (x y)
requires { A[x] = L1 && A[y] = L4 }
{ A[j] := case | j = x : L3 | A[j] = L4 : L3 | _ : A[j]; }

transition t6 (x)
requires { A[x] = L3 }
{ A[j] := case | j = x : L2 | A[j] = L3 : L1 | _ : A[j]; }

transition t7 (x)
requires { A[x] = L3 }
{ A[j] := case | j = x : L1 | _ : A[j]; }

transition t8 (x)
requires { A[x] = L4 }
{ A[j] := case | j = x : L1 | _ : A[j]; }

transition t9 (x)
requires { A[x] = L4 }
{ A[j] := case | j = x: L2 | _ : A[j]; }