Works

State Machine Studio

A modeling surface for hierarchical state machines and formalization workflows.

State Machine Studio is a local React application for browsing, editing, validating, and demonstrating hierarchical state machines.

It is not just a diagramming tool. The application stores machines in a canonical nested representation designed to connect browser editing with Agda-side state-machine formalization. A high-level process can be refined into lower-level layers while every concrete state and transition keeps a link back to the abstract state or transition it refines.

What The App Shows

The seeded library has two families:

synthetic connectivity patterns for stress-testing dense and uneven graphs;
real-life-style examples for order fulfillment, media playback, hospital triage, and EV charging sessions.

Every included example has at least three levels. Some have four or five. That matters because the app is built around moving between levels and inspecting intervals between an abstract parent view and a concrete refinement.

The editor supports:

folder and machine browsing;
level tabs and interval selection;
panning, zooming, and minimap navigation;
band view and nested graph view;
state and transition editing through an inspector;
validation issues as errors or warnings;
JSON persistence through the local backend;
generated Agda preview for the selected machine.

Demo Stories

Order fulfillment moves from a business view into warehouse refinement and scanner/task detail while keeping received, processing, shipped, and exception states visible as the abstract map.

Media player moves from user-facing controls into runtime detail, packet behavior, frame handling, decoding, and clock behavior.

Hospital triage moves from patient-flow states into clinical operations and audit events across a five-layer hierarchy.

EV charging moves from driver session states into station control, socket detection, token checks, relay control, metering, diagnostics, and telemetry.

Formalization Boundary

The canonical persisted format is agda-canonical-nested-v1. The finest layer is stored first, the coarsest layer last, and collapse maps connect each finer layer to the adjacent coarser layer. That is the representation exported toward Agda.

Predicates are stored as Agda expressions in agda-ctl-predicate-v1 form. The backend currently typechecks predicate syntax and atom vocabulary against a generated Agda module. It does not yet prove satisfaction over the canonical nested machine. The next substantial formalization step is a reusable adapter from canonical nested machines to temporal models.

That boundary is worth saying clearly because it makes the product credible: the UI already reaches into Agda tooling, while the remaining model-checking bridge is a defined technical target.

State Machine Studio