Project overview

statechart-art turns small TLA+ models of a boba shop into hand-drawn-style statecharts. Each plate is a square image sized to read on a phone, and the four plates cover different modeling ideas: an order with a branch and a loop, a day structured as a parent state, two concurrent regions (barista and pot), and a rule violation that TLC finds along with the path to it.

The pipeline is the point: a TLA+ spec and config define what can happen and which rules must hold; TLC checks every reachable state; a /statechart skill writes a Mermaid chart using wording from view.mjs; pele lays out the chart; and a per-plate Node script draws the layout in pen and coloured pencil on a simulated paper surface. The drawing is seeded, so the same code produces the same image. The result is useful to people learning statechart notation or TLA+ through a concrete, low-stakes example, and to people curious about programmatic illustration.

The finished plates are viewable on the project site.

Quick start

The drawing tools need Node (the project was made with Node 24). From the repository root:

cd tools && npm install

Then draw a plate from the repository root:

node business/art/order.js

The plate scripts are order.js, day.js, counter.js and bug.js. Each writes business/out/<plate>.png (2160 px), a 2048 px X/Twitter variant <plate>-x.jpg, a 1080 px preview, and <plate>-pele.json with layout boxes used by the site. Add --fast to draw at half size for a quick look. After the plates, node business/art/cards.js draws the icons and share card.

To build the site into docs/ and preview it at http://localhost:5297:

node site/build.js
node site/serve.mjs

SITE and REPO can be set when building to change the share-link address and code link, for example SITE=https://example.com/boba/ REPO=https://github.com/you/boba node site/build.js.

To check a model and regenerate its chart, run the /statechart skill against a new or empty output folder, e.g. ~/.claude/skills/statechart/scripts/statechart business/order/Order.tla --view business/order/view.mjs --out business/order/chart-new. The skill refuses to write into an existing non-empty folder, so compare the new output with the checked-in chart/ directory. The bug model is expected to exit with status 1 because its rule fails.

Constraints and layout

The workflow assumes the custom /statechart skill is installed at ~/.claude/skills/statechart/, which is not part of the repository; regenerating charts is therefore unavailable on a clean checkout without it. Node is required; the project was made with Node 24 and no other runtime requirements are stated. The bug plate intentionally exits non-zero, so wrap it in the usual way if running it in a scripted pipeline. When a chart changes, its output must be copied into layout.mmd while keeping the config and direction lines.

Repository layout: business/<chart>/ holds each model, view, generated chart and layout; business/art/ holds the plate scripts and shop elements; tools/lib/ and tools/kit/ contain the drawing primitives and dry-media simulation; tools/fonts/ holds Kevin Serif and Kevin Sans; site/ builds the site; docs/ is the built output served by GitHub Pages. Everything, including code, models, drawings and fonts, is MIT-licensed.

HotRepo's take

The repository entered the HotRepo new-project list on 2026-11-02, recording 51 stars gained over a roughly 24-hour window starting 2026-11-01 15:45 UTC, reaching 153 stars and 12 forks. The hourly samples during that window rise fairly steadily from around 100 to 153, but this is a single recorded snapshot and short observation period, so it doesn't support conclusions about sustained growth. The draw is the combination of a genuinely checked formal model with an unusual illustration pipeline; the code itself is approachable enough to run and inspect.