val N:ℕ; // the number of processes
val M:ℕ; // the maximum number of messages in a channel
axiom notNull ⇔ N ≠ 0;

type Process = ℕ[N-1];
type Message = Process; // we send process ids as messages
type Channel = Record[n:ℕ[M],p:ℕ[M],m:Array[M,Message]];

// the empty channel
val empty:Channel = ⟨n:0,p:0,m:Array[M,Message](0)⟩;

// test whether channel "c" is empty or full
pred isempty(c:Channel) ⇔ c.n = 0;
pred isfull(c:Channel) ⇔ c.n = M;

// adds message "m" to channel "c"
proc add(c:Channel,m:Message):Channel
  requires ¬isfull(c);
{
  var c0:Channel = c;
  c0.m[(c0.p+c0.n)%M] = m;
  c0.n = c0.n+1;
  return c0;
}

// returns the oldest message in "c"
fun first(c:Channel):Message 
  requires ¬isempty(c);
= c.m[c.p];

// removes the oldest message from "c"
proc remove(c:Channel):Channel
  requires ¬isempty(c);
{
  var c0:Channel = c;
  c0.p = (c0.p+1)%M;
  c0.n = c0.n-1;
  return c0;
}

// the status of a process
type Status = ℕ[2]; 
val idle = 0; val waiting = 1; val leader = 2;

// the id of the next process
fun next(i:Process):Process = (i+1)%N;

shared system LeaderElection
{
  var c: Array[N,Channel] = Array[N,Channel](empty);
  var s: Array[N,Status] = Array[N,Status](idle);
  var b: Bool = ⊥;

  action start(i:Process) with
   s[i] = idle ∧ ¬isfull(c[next(i)]);
  {
    var i0:Process = next(i);
    c[i0] ≔ add(c[i0],i);
    s[i] ≔ waiting;
  }
  
  action forward(i:Process) with
    s[i] = idle ∧ ¬isempty(c[i]) ∧ ¬isfull(c[next(i)]);
  {
    var j:Process = first(c[i]);
    c[i] ≔ remove(c[i]);
    var i0:Process = next(i);
    c[i0] ≔ add(c[i0],j);
  }
}