type Status = enumeration of  waiting, elected, announced

automaton Process(I: type, i: I)
  assumes RingIndex(I, String)
  signature 
    input  receive(m: String, const left(i), const i) 
    output send(m: String, const i, const right(i)),
           leader(m: String, const i)
  states 
    pending: Mset[String] := {name(i)}, 
    status:  Status := waiting
  transitions 
    input receive(m, j, i) 
      eff if m > name(i) then pending := insert(m, pending)
          elseif m = name(i) then status := elected
          fi 
    output send(m, i, j) 
      pre m \in pending
      eff pending := delete(m, pending)
    output leader(m, i)
      pre status = elected /\ m = name(i)
      eff status := announced

automaton Channel(M, Index: type, i, j: Index)
  signature 
    input  send(m: M, const i, const j)
    output receive(m: M, const i, const j)
  states 
    buffer: Seq[M] := {}
  transitions 
    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)
  components
    P[i: I]: Process(I, i);
    C[i: I]: Channel(String, I, i, right(i))


invariant of LCR : \A i : I \A j : I \A k : I (
(name(i) \in P[k].pending /\ inbetween(i,j,k) /\ i ~= j)  => name(i) > name(j) )

invariant of LCR : \A i : I \A j : I \A k : I (
(name(i) \in C[k].buffer /\ inbetween(i,j,k) /\ i ~= j)   => name(i) > name(j) )

invariant of LCR : \A i : I \A j : I (
                    (P[i].status ~= waiting /\ i ~= j ) => name(i) > name(j)  )

invariant of LCR : \A i : I \A j : I (
                 (P[i].status ~= waiting  /\ P[j].status ~= waiting) => i = j  )