Traffic light — the minimal musil model

What this teaches: how to express a finite-state machine as states + guarded actions, prove a safety invariant, and export the reachable graph as Graphviz DOT.

The system

A traffic light cycles through three colours: red → green → yellow → red. There is exactly one state field (color) and one action per edge in the cycle. The safety invariant says the colour is always one of the three known values — nothing stranger can happen.

This is the smallest model that exercises every core concept at once:

• a frozen dataclass as the state type
• three Action objects as the transitions
• an invariant checked in every reachable state
• to_dot for a visual sanity check

What musil finds

The BFS explores three states (red, green, yellow) and confirms the invariant holds in all of them. No counterexample, no deadlock.

Result(ok=True, states=3)

to_dot emits Graphviz DOT that you can pipe to dot -Tsvg to get a picture of the three-node cycle.

Source

"""A traffic light: the smallest useful musil model — safety + a DOT render.

Run: python examples/traffic_light.py
"""

from __future__ import annotations

from dataclasses import dataclass, replace

from musil import Action, Model, check, to_dot


@dataclass(frozen=True)
class Light:
    color: str = "red"


MODEL = Model(
    init=Light("red"),
    actions=[
        Action("go", lambda s: s.color == "red", lambda s: replace(s, color="green")),
        Action("slow", lambda s: s.color == "green", lambda s: replace(s, color="yellow")),
        Action("stop", lambda s: s.color == "yellow", lambda s: replace(s, color="red")),
    ],
    invariants={"known-color": lambda s: s.color in {"red", "green", "yellow"}},
)


if __name__ == "__main__":
    print(check(MODEL))
    print("\n--- DOT (pipe to: dot -Tsvg) ---")
    print(to_dot(MODEL))

Run it

python examples/traffic_light.py

See also

• Service lifecycle — builds a model directly from a transition table using status_field_actions, so the spec and the code share a single source of truth.
• Lost update — the next step: two actors sharing state, where the bug lives in the interleaving.