// number of processes
val N:ℕ; 
axiom processNumber ⇔ N ≥ 2;
type Process = ℕ[N-1];

// maximum value of ticket numbers
val M:ℕ;

// the bakery algorithm
shared system Bakery
{
  var e:  Array[N,Bool] = Array[N,Bool](⊥);
  var n:  Array[N,ℕ[M]] = Array[N,ℕ[M]](0);
  var j:  Array[N,ℕ[N]] = Array[N,ℕ[N]](0);
  var m:  Array[N,ℕ[M]] = Array[N,ℕ[M]](0);
  var pc: Array[N,ℕ[4]] = Array[N,ℕ[4]](0);
  
  invariant ⊤;
  
  action start(i:Process) with ⊤;
  { }
}