bakery_lamport_na.cub

type location = NCS | Choosing | Choosen | Wait | CS | Crash

array PC[proc] : location
array Ticket[proc] : int
array Num[proc] : int
array Choose[proc] : bool

var Max : int

array Cpt[proc,proc] : bool

init (x y) { PC[x] = NCS && Num[x] = 0 && Choose[x] = False &&
             Max = 1 && Ticket[x] = 0 && Cpt[x,y] = False }

invariant () { Max < 0 }
(* invariant () { Max <= 0 } *)

unsafe (x y) { PC[x] = CS && PC[y] = CS }
(* unsafe (x y) {Num[x] = 50 && Num[y] = 10} *)

transition next_ticket ()
{ 
  (* Ticket[j] := case | _ : Max; *)
  Max := Max + 1;
}


(* transition take_ticket (x) *)
(* requires { PC[x] = NCS && *)
(*            forall_other j. Num[j] < Max } *)
(* { *)
(*   PC[x] := Choosen; *)
(*   Ticket[x] := Max; *)
(*   Choose[x] := True; *)
(* } *)


transition take_ticket (x)
requires { PC[x] = NCS }
{
  PC[x] := Choosing;
  Choose[x] := True;
}

 
transition find_ticket_found (x)
requires { PC[x] = Choosing && forall_other j. Cpt[x,j] = True }
{ 
  Cpt[i,j] := case | i = x : False | _ : Cpt[i,j];
  Ticket[x] := Max;
  PC[x] := Choosen;
}


transition find_ticket_iter (x j)
requires { PC[x] = Choosing && Cpt[x,j] = False && Num[j] < Max }
{ 
  Cpt[x,j] := True;
}

transition assigned (x)
requires { PC[x] = Choosen }
{
  Choose[x] := False;
  PC[x] := Wait;
  Num[x] := Ticket[x];
}


(* transition turn (x) *)
(* requires { PC[x] = Wait && *)
(*   forall_other j. *)
(*   ( Choose[j] = False && Num[j] = 0 || *)
(*     Choose[j] = False && Num[x] < Num[j] || *)
(*     Choose[j] = False && *)
(*       Num[x] = Num[j] && x < j ) } *)
(* { *)
(*   PC[x] := CS; *)
(* } *)


transition wait_exit (x)
requires { PC[x] = Wait && forall_other j. Cpt[x,j] = True }
{ 
  Cpt[i,j] := case | i = x : False | _ : Cpt[i,j];
  PC[x] := CS;
}

transition wait_iter1 (x j)
requires { PC[x] = Wait && Cpt[x,j] = False &&
           (* PC[j] <> Choosing && PC[j] <> Choosen && *)
           Choose[j] = False && Num[j] = 0 }
{
  Cpt[x,j] := True;
}

transition wait_iter2 (x j)
requires { PC[x] = Wait && Cpt[x,j] = False &&
           (* PC[j] <> Choosing && PC[j] <> Choosen && *)
           Choose[j] = False && Num[x] < Num[j] }
{
  Cpt[x,j] := True;
}

transition wait_iter3 (x j)
requires { PC[x] = Wait && Cpt[x,j] = False &&
           (* PC[j] <> Choosing && PC[j] <> Choosen && *)
           Choose[j] = False && Num[x] = Num[j] && x < j }
{
  Cpt[x,j] := True;
}


transition exit (x)
requires { PC[x] = CS }
{
  PC[x] := NCS;
  Num[x] := 0;
}

transition fail (x)
{
  PC[x] := Crash;
}

transition recover (x)
requires { PC[x] = Crash }
{
  PC[x] := NCS;
  Num[x] := 0;
  Choose[x] := False;
  Cpt[i,j] := case | i = x : False | _ : Cpt[i,j];
}