Actors turn effects into commands

An actor receives an event, updates copy-on-write state, and emits commands through Out. During checking those commands update the modeled network and timer state; the Rust function itself performs no I/O.

The monotonic flag creates the negative control and repair from one model. The safety state remembers whether value 2 has ever arrived. Without that history, states value = 1 before 2 and value = 1 after 2 would look equal even though only the latter is a regression.

Configure the faults you mean

The shortest violating delivery order is Value(2), then Value(1). Message loss is not needed for this witness, but modeling it checks that dropping either message cannot create the same safety violation. For an invariant that does not inspect pending messages, indefinite delay can be observationally equivalent to loss; explicitly modeling both may add work without changing that property.

Timers and liveness need restraint

set_timer makes timeout a possible checker action. It does not make timeout inevitable. A retry can support progress only with assumptions about which enabled actions eventually occur. A bounded safety run can show that retries, drops, and duplicate deliveries do not violate the invariant in its explored state graph; it does not establish real-time delivery or eventual convergence.

Network semantics are selectable. An ordered network can model per-link FIFO; an unordered nonduplicating network can omit redelivery. Choose the weakest behavior the real transport promises, then state excluded faults such as corruption, partitions longer than the model, actor crashes, or durable-state loss. A convenient stronger transport can erase the failure under study.

Unlike transfer: expiring a reservation

Model a coordinator and a worker for a reservation protocol. The coordinator sends Reserve(epoch) and later Cancel(epoch); a retry may duplicate either message. The worker must never resurrect a canceled epoch when an old reserve arrives late. Use explicit epoch state rather than copying the register's boolean has_seen_latest history.

Complete the transfer when:

1. the broken worker has a concrete cancel-then-old-reserve counterexample;
2. the repaired worker rejects commands older than its greatest observed epoch;
3. a positive property or witness shows a fresh reservation can still activate;
4. loss, duplication, ordering, timeout, crash, and depth assumptions appear in the verdict.

Lessons

• Actor outputs make sends and timers visible to the model checker.
• Network order is a model choice, not a consequence of source order.
• Loss, duplication, timeout, crash, and storage behavior must be admitted explicitly.
• History belongs in state when a property depends on what happened before.
• Monotonic updates can make reordering and duplication harmless for a narrow claim.
• Safety under bounded network exploration does not imply real-time liveness.

Practice

1. Retrieval. What checker actions arise from sends, a lossy network, and a timer?
2. Discrimination. When can explicit message loss be redundant for an invariant?
3. Transfer. Build the reservation model and preserve its shortest broken trace beside the repair.

References

1. Stateright. Actor tutorial. — executable actors and checking
2. Stateright. ActorModel API for 0.31.0. — actors, properties, faults, and boundaries
3. Stateright. Network API for 0.31.0. — ordered, unordered, and duplicating semantics