statechart

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:

<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 });

Label each state with what the reader can see or cares about, such as "Paying" or "Lease held, write pending". Keep variable names out of labels. In vars, a TLA+ sequence is an object with keys from 1, so v.pc[1] is pc[1]. A set is an array.