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)) where m >= name(i),
leader(const name(i), const i)
states
pending: Mset[String] := {name(i)},
status: Status := waiting
transitions
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
tasks
{send(m, j, right(j))};
{leader(m, j)}
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))
The data types used in this specification are described in auxiliary
specifications written in
RingIndex(I, J): trait
introduces
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