bakery_lamport_bogus.cub

type location = NCS | Choose | Wait | CS

array PC[proc] : location
array Ticket[proc] : int
array Number[proc] : int

var Max : int


init (x) { PC[x] = NCS && Number[x] = 0 && Max = 1 && Ticket[x] = 0 }

invariant () { Max < 0 }

unsafe (x y) { PC[x] = CS && PC[y] = CS }


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

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


transition wait (x)
requires { PC[x] = Choose }
{
  PC[x] := Wait;
  Number[x] := Ticket[x];
}


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


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