# State machines and statecharts

A state machine encodes a finite set of states and the legal
transitions between them. A *statechart* (Harel's extension (Harel 1987)[^harel1987]) adds
hierarchy, history, and orthogonal regions, useful when the flat
state set explodes. Making the state machine *an explicit artifact
that the code refers to* changes what the compiler can enforce: the
states have names, the transitions are values, the compiler can check
exhaustiveness, and reviewers can read the machine without reading
the implementation.

## What it catches

- **Illegal transitions.** A `PaymentRefunded` event fired on an
  `Unpaid` order should be a compile-time error, not a 500. The
  state machine makes "what events are valid in which states" a
  type-checked question.
- **Forgotten states.** Adding a new state (e.g., `PartiallyPaid`)
  and forgetting to handle one of the events in that state is a
  reviewer-visible omission when the chart is in the repo.
- **Implicit state in code that should have explicit states.**
  Order-status enums that drift; payment-flow paths the code
  navigates by string comparison; UI screens whose enabled/disabled
  state depends on an undocumented combination of booleans. The
  chart names the states the code was navigating anyway.
- **Drift between design and implementation.** When the chart is
  the source of truth and the implementation is generated or
  consulted, divergence is a code bug, caught at the test that
  drives the implementation through the chart.
- **Concurrent state in protocol code.** Statecharts with orthogonal
  regions model "two things happening at once" in a way that flat
  state machines and ad-hoc booleans don't; verifying the
  interleavings between regions is a separate job for [model
  checking](https://quality.stereobooster.com/model-checking.md).

What state machines do **not** catch: anything outside the
transition graph. Logic *inside* a transition (the side effect,
the persistence write, the network call) is unchecked by the
chart; pair with [property-based
testing](https://quality.stereobooster.com/property-based-testing.md) or
[contracts](https://quality.stereobooster.com/contracts-and-runtime-assertions.md) on the
transition bodies.

## Tools

### Library-supported statecharts

- **[XState](https://stately.ai/docs/xstate)** (TypeScript/JavaScript) — statechart library;
  visual editor; treats the chart as the source of truth, the code
  follows. Closest mainstream implementation of Harel statecharts.
- **Stateflow** (MATLAB / Simulink) — used in aerospace,
  automotive, and embedded-systems toolchains.
- **[SCXML](https://www.w3.org/TR/scxml/)** (W3C) — state-chart XML standard; supported by
  [Apache Commons SCXML](https://commons.apache.org/proper/commons-scxml/) and others.

### Per-ecosystem state-machine libraries

- **Rust:** **[statig](https://github.com/mdeloof/statig)**, **[state_machine_future](https://github.com/fitzgen/state_machine_future)**, **[sm](https://github.com/rustic-games/sm)**,
  **[rust-fsm](https://github.com/eugene-babichenko/rust-fsm)**.
- **Go:** **[looplab/fsm](https://github.com/looplab/fsm)**, **[qmuntal/stateless](https://github.com/qmuntal/stateless)**.
- **Java/Kotlin:** **[Spring Statemachine](https://spring.io/projects/spring-statemachine)**, **[Tinder StateMachine](https://github.com/Tinder/StateMachine)**
  (Kotlin DSL).
- **Python:** **[transitions](https://github.com/pytransitions/transitions)**, **[python-statemachine](https://github.com/fgmacedo/python-statemachine)**.
- **Elixir:** **[gen_statem](https://www.erlang.org/doc/apps/stdlib/gen_statem.html)** (OTP, since Erlang/OTP 19).
- **C/C++:** **[Boost.MSM](https://www.boost.org/doc/libs/release/libs/msm/)**, **[Boost.SML](https://boost-ext.github.io/sml/)**.

### State machines as plain typed code

- Any typed language can encode a state machine as a sum
  type with a transition function. Often the cheapest path: no
  library, no DSL, exhaustive matching enforced by the compiler.
  Elm, Rust, OCaml, Haskell, and TypeScript discriminated unions
  all fit this idiom.

### Model-check the chart

- **[TLA+](https://lamport.azurewebsites.net/tla/tla.html)** / **[Alloy](https://alloytools.org/)** / **[SPIN](https://spinroot.com/spin/whatispin.html)** — when the state space is
  important enough, lift the chart into a model checker. See
  [model checking](https://quality.stereobooster.com/model-checking.md).
- **[PRISM](https://www.prismmodelchecker.org/)** — probabilistic model checker for stochastic
  transitions (retry policies, backoff). See
  [statistical model checking](https://quality.stereobooster.com/probabilistic-model-checking.md).

### Verify the chart directly

Beyond a library, some tools analyze the chart itself: unreachable
states, nondeterministic transitions, and temporal properties, checked
statically over the model.

- **[Ansys SCADE](https://www.ansys.com/products/embedded-software/ansys-scade-suite)** (commercial): synchronous-language
  statecharts with formal verification and qualified code generation
  (DO-178C); the safety-critical avionics and rail toolchain.
- **[Simulink Design Verifier](https://www.mathworks.com/products/simulink-design-verifier.html)**
  (commercial): proves properties and detects dead logic on Stateflow
  charts, and generates tests from them.
- **itemis**'s statechart IDE (formerly Yakindu Statechart Tools) and
  **IBM Rhapsody** (both commercial): statechart / UML-state-machine
  authoring with model validation and code generation.

### Generate tests from the chart

With the chart as the source of truth, model-based testing generates the
tests that drive the implementation through it: each state and
transition is a path to exercise.

- **[GraphWalker](https://github.com/GraphWalker/graphwalker-project)** generates and walks test paths over
  an FSM model; **[AltWalker](https://github.com/altwalker/altwalker)** executes GraphWalker
  models against the implementation.
- **[fMBT](https://github.com/intel/fMBT)** (Intel) and **ModelJUnit** (JVM) generate
  sequences from a model.

### Learn a chart from a black box

Active automata learning (Angluin's L\*) recovers a chart from a system
that has none: it infers an FSM by querying the implementation, and the
inferred machine is then checked. It has been used to analyze protocol
implementations (TLS, SSH, TCP).

- **[LearnLib](https://github.com/LearnLib/learnlib)** (JVM) and **[AALpy](https://github.com/DES-Lab/AALpy)** (Python)
  learn automata by active querying.
- **[TorXakis](https://github.com/TorXakis/TorXakis)** and **JTorX** do model-based conformance
  testing (`ioco`) against a labeled-transition-system spec.

## When to use, when not

**Use:**

- For any feature with a non-trivial lifecycle. Orders, payments,
  subscriptions, multi-step forms, dialog flows, document
  workflows.
- For UI components where enabled/disabled state depends on
  context: the chart makes that context explicit, and Wayne
  recommends it as the lightweight formal method for UI (Wayne 2018)[^wayne2018c].
- For protocol code at the application layer (HTTP retry/backoff
  state, connection lifecycle, cache state).
- When stakeholders need to read the flow. Statecharts are visual
  and approachable.

**Don't:**

- For simple toggles or two-state flows. The ceremony exceeds the
  value.
- For decision logic that doesn't have state. Use
  [decision tables](https://quality.stereobooster.com/decision-tables.md) instead.
- For deeply concurrent or distributed protocols where the
  interleavings matter. Lift to [model checking](https://quality.stereobooster.com/model-checking.md).

## Evidence

The empirical literature on state machines as a *practice* (rather
than as a formalism) is thin; the case rests on the definitional
points: illegal transitions become type errors, forgotten
transitions become visible omissions, and a mechanically checked
chart cannot silently diverge from the code.

## Classification

- **Quality dimensions:** Functionality.
- **Area:** UI flow control, order / payment / subscription lifecycles, protocol state, embedded control logic, asynchronous workflows, anything with explicit transitions.
- **Guarantee:** Exhaustive over the declared state × event space — every state and transition is enumerated, and illegal or forgotten transitions are rejected (compiler-checked, or model-checked over the transition graph).

## Referenced by

- [Automated test generation](https://quality.stereobooster.com/automated-test-generation.md) · Methods
- [Decision tables](https://quality.stereobooster.com/decision-tables.md) · Methods
- [Formal methods](https://quality.stereobooster.com/formal.md) · Methods
- [Temporal-logic falsification](https://quality.stereobooster.com/temporal-logic-falsification.md) · Methods
- [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI

## References

[^harel1987]: Harel, David. 1987. "[Statecharts: A Visual Formalism for Complex Systems](https://www.weizmann.ac.il/math/harel/sites/math.harel/files/users/user50/Statecharts.pdf)." *Science of Computer Programming* 8 (3): 231–74. <https://doi.org/10.1016/0167-6423(87)90035-9>.
[^wayne2018c]: Wayne, Hillel. 2018. *[Formally Specifying UIs](https://www.hillelwayne.com/formally-specifying-uis/)*. <https://www.hillelwayne.com/formally-specifying-uis/>.

## Acronyms

- DSL — domain-specific language
- FSM — finite state machine