Language quick reference
A program contains interfaces and algorithms. An algorithm implements one interface and uses others: Net (network) and Rounds (synchronous rounds) are provided by the simulator; the rest you write yourself, and they are wired together automatically.
upon event ⟨instance, Event | pattern⟩ where condition do … end upon condition expression do … end upon exists x in S where condition do … end trigger ⟨instance, Event | arg1, arg2⟩ forall q in neighbors where q ≠ p do … end if … then … elif … then … else … end starttimer(t, 100ms) canceltimer(t) ⟨timer, Timeout | t⟩ assert cond, "msg" log x
function name(a, b) … return value … end call name(x, y) uses PerfectLinks as pl via AckLinks
Functions live inside an algorithm, see its state and parameters, and may trigger events; use them in expressions, or with call as a statement. via picks which algorithm implements a used interface when there are several.
Indications go up, requests go down. Undeclared all-caps words (HEARTBEAT) are atoms. In patterns, a new name captures the value; an atom or a known name must match.
Built-ins: self, Π, N, neighbors, round, now(), DELTA PHI RHO (only when known in the assumed model), min max choose size keys values map() get(m,k,default) remove(c,x) random(a,b) pick(S) append head tail last sort reverse slice range sum mean argmin argmax toset str abs sqrt ln exp pow floor ceil round. Tuples are 0-indexed; #S is the cardinality. Durations (50ms) are numbers in microseconds.
ASCII equivalents: < > for ⟨ ⟩, union inter minus in notin subseteq, != <= >=, and or not, Procs for Π, {} for ∅. Inside an ASCII trigger, wrap comparisons in parentheses.
One event per line: TIME NODE Event | arguments, where * means every process. Examples: 0ms 1 Broadcast | "hello", 0ms * Propose | random(1, 9). Events must be requests of the main algorithm. You can also select a process during playback and inject an event at the current time.
Faults
Processes not listed in a partition form one more group together, so 3 alone isolates p3. Leave Until empty for a permanent failure. A recovered process restarts with its volatile state reset: variables declared stable keep their value, and each module receives Recovery if it handles it, Init otherwise. During playback you can also select a process or a link and inject a crash, recovery, isolation or link failure at the current time.
Run
Run over many seeds
The same scenario, one run per seed, in the background. Properties and failed assertions are reported per seed; click a seed to open that run.