ORIENTED RING / MESSAGE-ONLY FAULTS
Trace the algorithm, agent by agent.
Port 0 is clockwise. Port 1 is counterclockwise.
Only messages can deviate from the protocol.
Every adversary
Check every black-hole location and every placement of up to f Byzantine agents, including every adaptive sequence of legal messages. Equivalent cases are merged using the proved reduction.
Choose n and f, then start. The tour shows one run per equivalence class; Rust checks every message branch in that class.
The theorem covers all f > 0; executable checks cover your selected n and f. This is an exact reduction, not random sampling.
Action schedule
Writing events, not guessed roundsNo overrides. Choose actions live, or add an event above.
Execution trace
Observer view · includes omissions and destructionModel & protocol assumptions
Timed scouts · every positive f
Use 2f + 2 agents: f + 1 scouts and f + 1 guards. For each clockwise depth d = 1, 2, …, scouts take turns: walk d edges forward, d edges back, then write RETURN_OK(d) at home. Each slot lasts exactly 2d + 1 rounds. Everyone else waits.
After every scout’s slot, guards read their local home board in a separate round. Any completed-trip receipt proves vd safe. If there are none, vd is the black hole: a safe trip would have produced at least one honest scout’s receipt. Guards then patrol the safe path indefinitely. They never consult remote deaths or the observer’s marker.
There are at least one honest scout and one honest guard. False warnings cannot forge a completed-trip receipt. Exactly f + 1 scouts are lost; at least one honest guard survives. Identification takes h[(f + 1)(h + 2) + 1] rounds for a hole at depth h. Each patrol period takes 2(n − 2) rounds. Read the proof and exhaustive-check scope.
A deliberately restricted adversary
An oriented synchronous ring, one always-active black hole, and a safe home v0. Port 0 leads to (v + 1) mod n; port 1 to (v − 1) mod n. All agents, including Byzantine agents, are destroyed on entry to the black hole.
Byzantine agents follow every movement and waiting instruction. At each writing opportunity they may only omit their own write or append an attributed false claim that their current port-0 or port-1 neighbor is the black hole. They cannot forge identities, erase records, write remotely, or send false safety reports.
The repository’s 1,2,2 algorithm
A1 walks clockwise alone. P1=(A2,A3) and P2=(A4,A5) wait at home through A1’s n-round epoch deadline. P1 then explores clockwise: its leader moves out, returns, and only then do the two members advance together. P2 is released only after P1 is interrupted and no valid certificate reaches home.
A hole is identified by interrupted own trails from two distinct IDs. A missing report cannot impersonate the missing agent or add another ID. A certificate travels back with its carrier; agents waiting at home learn it only when it arrives there. Survivors then patrol the safe path indefinitely. Play pauses after each patrol period; Step continues.
Source: OPODIS.tex, known-size algorithm and pseudocode and algorithms.tex. This viewer specializes that construction to your always-active black hole and message-only faults.
Two forward, one back · all agents
Every agent follows its own repeating port sequence 0, 0, 1 from its launch round. A configurable launch gap separates the agents. Each second-forward departure creates a backward-return obligation; a later agent can read expired obligations on the local whiteboard. Two distinct unresolved own records certify the next clockwise neighbor. That reader then switches to safe-path patrol.
This is the requested all-agent movement experiment, not the draft’s full unknown-size lockstep construction. It can lose every agent, particularly with simultaneous starts or a black hole adjacent to home. The viewer reports those failures. It never turns the observer’s black-hole marker into an agent’s knowledge.
Reproduce an adversarial run
In live mode, play pauses before each Byzantine writing event. Only Byzantine agents with a prescribed write in that round receive a choice. Waiting agents do not write. Arrival records appear in the next read/write phase, before the next movement. In scheduled mode, event overrides take precedence over per-agent defaults. An illegal explicit override stops the run for correction; it is never silently substituted.
The timeline replays computed rounds. Continuing from an earlier round replaces the later execution. Export stores configuration, defaults, overrides, and the exact committed decisions; import validates and replays them through Rust. Hiding the black-hole marker changes only the drawing. The search never receives that marker as evidence.