I/O Automata Description of Leader Election Algorithm

The following specification is written in IOA, a formal language for describing components in asynchronous concurrent systems.

type Status = enumeration of waiting, elected, announced

automaton Process(I: type, i: I)
  assumes RingIndex(I, String)
    input  receive(m: String, const left(i), const i) 
    output send(m: String, const i, const right(i)) where m >= name(i),
           leader(const name(i), const i)
    pending: Mset[String] := {name(i)}, 
    status:  Status := waiting
    input receive(m, j, i) where m > name(i)
      eff pending := insert(m, pending)
    input receive(m, j, i) where m < name(i)
    input receive(name(i), j, i)
      eff status := elected
    output send(m, i, j) 
      pre m \in pending
      eff pending := delete(m, pending)
    output leader(m, i)
      pre status = elected
      eff status := announced
    {send(m, j, right(j))};
    {leader(m, j)}

automaton Channel(M, Index: type, i, j: Index)
    input  send(m: M, const i, const j)
    output receive(m: M, const i, const j)
    buffer: Seq[M] := {}
    input send(m, i, j)
      eff buffer := buffer |- m
    output receive(m, i, j)
      pre buffer ~= {} /\ m = head(buffer)
      eff buffer := tail(buffer)

automaton LCR(I: type)
  assumes RingIndex(I, String)
    P[i: I]: Process(I, i);
    C[i: I]: Channel(String, I, i, right(i))
The data types used in this specification are described in auxiliary specifications written in Larch. Specifications for the types Mset (multisets) and Seq (sequences) are built into IOA. The specification for RingIndex is as follows.

RingIndex(I, J): trait 
     first:         -> I
     left, right: I -> I
     name:        I -> J
  asserts with i, j: I
    sort I generated by first, right;
    \E i (right(i) = first);
    right(i) = right(j) <=> i = j;
    left(right(i)) = i;
    name(i) = name(j) <=> i = j
  implies with i: I
    right(left(i)) = i