Make the race explicit

The system has four modeled fields: the latest generation, one running generation, one visible generation, and a depth counter. A start action moves authority to a newer generation. A finish action may publish only when the completed generation still equals the latest generation.

use stateright::{Checker, Model, Property};

#[derive(Clone, Debug, Hash, PartialEq, Eq)]
struct State {
    generation: u8,
    running: Option<u8>,
    published: Option<u8>,
    depth: u8,
}

#[derive(Clone, Copy, Debug, Hash, PartialEq, Eq)]
enum Action {
    Start(u8),
    Finish,
}

#[derive(Clone, Copy, Debug)]
struct Publication;

fn publication_is_current(_: &Publication, state: &State) -> bool {
    state.published.is_none_or(|value| value == state.generation)
}

impl Model for Publication {
    type State = State;
    type Action = Action;

    fn init_states(&self) -> Vec<State> {
        vec![State { generation: 0, running: None, published: None, depth: 0 }]
    }

    fn actions(&self, state: &State, actions: &mut Vec<Action>) {
        if state.generation < 2 {
            actions.push(Action::Start(state.generation + 1));
        }
        if state.running.is_some() {
            actions.push(Action::Finish);
        }
    }

    fn next_state(&self, state: &State, action: Action) -> Option<State> {
        let mut next = state.clone();
        match action {
            Action::Start(generation) => {
                next.generation = generation;
                next.running = Some(generation);
                next.published = None;
            }
            Action::Finish => {
                let completed = next.running.take()?;
                if completed == next.generation {
                    next.published = Some(completed);
                }
            }
        }
        next.depth += 1;
        Some(next)
    }

    fn properties(&self) -> Vec<Property<Self>> {
        vec![Property::always("only the current generation publishes", publication_is_current)]
    }

    fn within_boundary(&self, state: &State) -> bool {
        state.depth <= 4
    }
}

#[test]
fn every_bounded_event_order_preserves_publication_authority() {
    Publication.checker().threads(1).spawn_bfs().join().assert_properties();
}

The Model trait separates four jobs. init_states creates the roots. actions lists choices enabled in one state. next_state applies one choice. properties names claims over reached states. within_boundary stops the introductory search after four events.

Run the model:

cargo test

Inject the stale-publication defect

Remove next.published = None from the Start arm. Then run the check again. Stateright prints a counterexample with this shape:

Start(1)
Finish
Start(2)

After the final action, generation 2 owns publication authority while generation 1 remains visible. The property fails even before generation 2 finishes. Clearing the previous publication on start repairs that specific contract. Another product could retain the old visible value while labeling it as stale. That product needs a different state and property.

Relate the model to a spreadsheet

The generation is a workbook revision. Start(2) represents an edit that invalidates earlier work. Finish represents a worker completion. published is the generation displayed in the sheet. The production adapter may use threads, processes, or remote workers. The model refuses those mechanisms and keeps their observable competition.

The depth bound admits up to four actions, generations 1 and 2, and at most one modeled running result. The model does not cover three overlapping workers, partial cell publication, cancellation acknowledgments, or process failure. Those omissions belong in the result report.

Practice

1. Add a Cancel action that removes the running generation.
2. State a property that requires a canceled generation never to publish.
3. Explain why increasing depth alone does not model two simultaneous workers.

Worked answer

1. Add Cancel to Action, enable it when running.is_some(), and set running to None in its transition.
2. The state must retain canceled generation identities. The property can then reject any published identity in that set.
3. The carrier has only one running: Option<u8> slot. More steps cannot create a second slot that the state type cannot represent.

Lessons

• Stateright models transitions in ordinary Rust.
• The checker explores only choices that the model exposes.
• A counterexample names an action sequence and a final false state.
• The state type itself places structural bounds on the search.
• A production refinement must connect worker effects to modeled actions.

References

1. Jonathan Nadal. “Getting Started.” Stateright. — models, actors, properties, and checker execution.
2. Jonathan Nadal. “Comparison with TLA+.” Stateright. — executable Rust models and behavioral specifications.