bakery_na.cub

type t = Idle | Wait | Crit | Linf | Lsup

array A[proc] : t

array Cpt[proc,proc] : bool


init (z y) { A[z] = Idle && Cpt[z, y] = False }

unsafe (x y) { A[x] = Crit && A[y] = Crit }



transition t1 (z)
requires { A[z] = Idle }
{ 
  A[z] := Lsup;
}

transition sup_exit (z)
requires { A[z] = Lsup && forall_other j. Cpt[z,j] = True }
{ 
  Cpt[x,y] := case | x = z : False | _ : Cpt[x,y];
  A[z] := Wait;
}
 
transition sup_incr1 (z j)
requires { A[z] = Lsup && j < z && Cpt[z,j] = False }
{ 
  Cpt[z,j] := True;
}

transition sup_incr2 (z j)
requires { A[z] = Lsup &&  z < j && A[j] = Idle && Cpt[z,j] = False }
{ 
  Cpt[z,j] := True;
}

transition sup_abort (z j)
requires { A[z] = Lsup &&  z < j && A[j] <> Idle && Cpt[z,j] = False }
{ 
  Cpt[x,y] := case | x = z : False | _ : Cpt[x,y];
}


transition t2 (z)
requires { A[z] = Wait }
{
  A[z] := Linf
}

transition inf_exit (z)
requires { A[z] = Linf && forall_other j. Cpt[z,j] = True }
{ 
  Cpt[x,y] := case | x = z : False | _ : Cpt[x,y];
  A[z] := Crit;
}

transition inf_incr1 (z j)
requires { A[z] = Linf && z < j && Cpt[z,j] = False }
{ 
  Cpt[z,j] := True;
}

transition inf_incr2 (z j)
requires { A[z] = Linf &&  j < z && A[j] = Idle && Cpt[z,j] = False }
{ 
  Cpt[z,j] := True;
}

transition inf_abort (z j)
requires { A[z] = Linf &&  j < z && A[j] <> Idle && Cpt[z,j] = False }
{ 
  Cpt[x,y] := case | x = z : False | _ : Cpt[x,y];
}

transition tr3 (z)
requires { A[z] = Crit }
{ 
  A[z] := Idle
}