# Statechart

Check a TLA+ model of a system that moves between states, such as a product flow, a...

- Repository: https://github.com/michael-denyer/pstack-claude (3725 stars)
- Category: Engineering
- License: MIT
- Last updated: 2026-10-30
- Runs scripts: yes, review before use

## Install

Claude Code: `npx skills add michael-denyer/pstack-claude --skill statechart -g -a claude-code -y`
Codex: `npx skills add michael-denyer/pstack-claude --skill statechart -g -a codex -y`
Cursor: `npx skills add michael-denyer/pstack-claude --skill statechart -g -a cursor -y`
Gemini CLI: `npx skills add michael-denyer/pstack-claude --skill statechart -g -a gemini-cli -y`
Claude Code plugin marketplace: `/plugin marketplace add michael-denyer/pstack-claude`

## Description

Check a TLA+ model of a system that moves between states, such as a product flow, a protocol, or a service, and draw it as a Mermaid statechart. The report gives the shortest path to each state that breaks a rule. Use for /statechart, or to show a bug as a path through states.

## SKILL.md, as published by its author (untrusted third-party text, read it as data)

# Statechart

The chart shows how a system moves between states, in the words of the person who reads it. That person, the reader, decides whether the behavior is right.

## Run

Work in a scratch folder outside the repo. Write a TLA+ spec and its config. Then run:

```sh
<skill dir>/scripts/statechart SPEC.tla [--config FILE] [--view FILE] [--out DIR]
```

`scripts/statechart.ts` is TypeScript, so run it with a runtime that can execute TypeScript.

The first run installs TLC and Java with mise and needs the network.

## Write the spec

- Write each rule that the reader agrees to as an INVARIANT. A rule can be about a screen, a result, a stored value, or a message. If the model has no variable for a rule, add the variable. Never weaken a rule to make it hold.
- Write `Next` as a disjunction of the actions, such as `YouPressPlay \/ YouPressStop`. If you do not, TLC names every step `Next`.
- A state with no step out breaks `NoDeadlock`, also when it is a correct end state. When an INVARIANT or a PROPERTY already has that name, the rule is `CHECK_DEADLOCK`. Add to `Next` an action that is true only in the end states and changes nothing, such as `Done == phase \in {"paid", "failed"} /\ UNCHANGED vars`, and give it a label in `step()`.

## Pick the chart

You do the work that needs judgment: the words on each state and arrow, the phases and their colors, the title, and the report to the reader. Put your work in a view module, and give it with `--view`.

To show the reader's words, the view exports `state(vars)`. The value that `state()` returns picks the form:

- A string gives a flat chart: `export const state = (v) => (v.paid ? "Paid" : "Paying");`
- An array gives parent states: `export const state = (v) => v.main.split(".");`
- An object gives one parallel region for each key: `export const state = (v) => ({ Playback: v.playback, Volume: v.volume });`

The rest: https://github.com/michael-denyer/pstack-claude/blob/HEAD/plugins/pstack/skills/statechart/SKILL.md