Learn · All the Ways It Can Break

growing

Rust Can Be the Model

An executable transition system begins with ordinary types and one deliberately pure step function.

formal-methods, stateright, rust, model-checking, state-machine, learn

You will create a blank Rust library, add Stateright 0.31.0, define hashable state and action types, implement Model, and encode a safety property. You will also identify which production details do not belong in semantic state.

Begin with a library

cargo new turnstile-model --lib
cd turnstile-model
cargo add stateright@0.31.0

If cargo add is unavailable, add stateright = "0.31.0" under [dependencies] in Cargo.toml. If the specimen reports missing trait items, confirm with cargo tree -i stateright that Cargo selected 0.31.0; examples for another release may implement a different public trait surface.

Replace src/lib.rs with the specimen, or type it in two passes. First define the carrier and the choices:

rust code/all-the-ways-it-can-break/turnstile-stateright/model.rs#state-action model.rs The derived equality and hash implementations let the checker recognize a state it has already visited.

State records facts that can change a future choice or the property. Action names one atomic choice. Logging fields, object identities, and wall-clock timestamps are absent because they do not affect this model's future.

State-space exploration visits reachable states and follows each enabled transition. The Stateright modeling tutorial develops the same interface in more detail.

Implement the transition system

rust code/all-the-ways-it-can-break/turnstile-stateright/model.rs#model model.rs actions enumerates admitted choices; next_state computes one successor; properties states what every reachable state must preserve.

Do not put an HTTP call in next_state. Model its possible outcomes as actions. Do not call a random-number generator in actions. Enumerate the choices the environment may make. Executability does not turn effects into semantics; it makes the separation more visible.

Prediction — decide which path the checker can construct.

What the traits buy

Clone lets exploration retain successors. Eq and Hash define the identity used for visited-state detection. A field included in that identity can multiply states; a field omitted from it cannot influence later behavior without making the model dishonest. This is the executable form of choosing state by future differences.

The model remains an abstraction. Compiling it proves Rust type correctness, not correspondence to a production service. The checker will later establish facts only about states reachable through these actions.

Lessons

Model separates initial states, enabled actions, transitions, and properties.
Rust types are the notation; purity and finite semantic state make them model-checkable.
Eq and Hash participate in the meaning of state identity.
Environmental outcomes become explicit actions rather than hidden effects.
An executable model is not automatically an implementation model.

Practice

Retrieval. What four obligations does the specimen's Model implementation supply?
Discrimination. Should a request identifier appear in State when properties and transitions never inspect it?
Transfer. Model a two-position door with Open, Close, and Lock; forbid locking while open.

Worked answers

Initial states, enabled actions, successor computation, and properties.
No. It distinguishes states with identical futures and increases exploration without changing an observation.
Use position and lock status as state, guard Lock by closed position, and deliberately remove the guard to obtain the negative control.

References

Stateright. Modeling tutorial. — Model, states, actions, and properties
Stateright. Model API for 0.31.0. — exact trait contract used here

← A Small Scope Still Needs a Witness The Checker Owns the Choices →

A model checker does not need a second specification language. In Stateright, ordinary Rust types can describe states and actions, while an implementation of Model supplies initial states, enabled actions, successor states, and properties. The important change is not the syntax. The transition must behave like a mathematical function: the same state and action produce the same successor without performing network, clock, filesystem, or random effects. The opening specimen is intentionally small. A turnstile admits Pay and Enter. Its broken version enables entry before payment. Its repaired version changes only the guard that generates enabled actions. This makes the first counterexample about the modeling interface rather than distributed systems.