Turn a TLA+ model or an agreed system flow into a Mermaid statechart, a diagram of states and transitions. It highlights numbered paths that break stated rules, helps check whether modeled bugs occur in code, and can create a TLA+ skeleton from a chart.
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.
Run score Not tested
See how to installReview the instructions the agent will receive before you install.
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.
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.
Next as a disjunction of the actions, such as YouPressPlay \/ YouPressStop. If you do not, TLC names every step Next.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().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:
export const state = (v) => (v.paid ? "Paid" : "Paying");export const state = (v) => v.main.split(".");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.
The view can also export step(action, from, to). It gets the TLC action name and the values before and after the step, and it returns the label of the arrow. Write each step label as the user sees it happen, such as "you press play" or "the connect fails". Do not name the code or the TLA+ action. Two actions that end the same in the chart get the same label, so that they share one arrow.
When a step can occur only in some conditions, end its label with the condition in brackets, in the reader's words, such as you press play [while the file loads]. In a regions chart, the command writes the condition on the other regions on the arrow, in the words of their labels, such as [when Offline]. Your brackets replace it, and two arrows from one state can then look the same. So in a regions chart, do not write brackets for a condition on another region. When a value that no label shows decides where a step goes, name the result in the label, such as "the roster read fails".
The view can also export these:
group(vars) returns the name of a phase. Each chart state gets the color of its group. When the model states behind one chart state are in different groups, that state gets no color.colors gives each group name a color class.title is a string that the chart shows at the top.The command calls state() and group() at most once for each model state, and step() at most once for each step. The chart and the report both use those answers. So make each function depend only on its arguments.
The chart does not draw a step that stays in one label. Split a label when the reader must see such a step.
Aim for about 20 arrows or fewer, because a busier chart is hard to read. First return coarser labels from state(). Give one label to values that act the same, and leave out a detail that the reader does not need, such as a call in flight whose return changes nothing. Keep each state of a bug path, and keep each mark. When a merge changes a breaks state to mayBreak, it hides where a rule breaks. Do not merge two states that break different rules, because the reader then cannot see which rule breaks where. If the chart is still too busy, return null from step() for the steps that the reader does not need, such as a reset that every state has, or a step whose arrow repeats what other arrows show. Obey these rules when you hide steps:
breaks. When only some model states behind it break the rule, it has the class mayBreak. The Legend names the rules of each mark. When two rules break, it names both on one mark, so say in the hand-off which state breaks which rule. In a regions chart, a state gets a mark when each combination of region states that includes it can break a rule. When a combination can break a rule and none of its states has a mark, each state in that combination gets a mark.tlc.out is what TLC printed on the config as written. When the chart does not show the bug path of a rule that breaks, tlc-RULE.out is what TLC printed for the run that found it. When TLC repeats its first warning, plain TLC prints it twice, but tlc.out shows it once, because TLC leaves the second copy out of the output that this command reads. That happens only when Java runs with -XX:+UseParallelGC, since otherwise TLC's first warning is its advice to pass that flag, which it prints once.Show chart.mmd to the user as a mermaid code block. The chart has a budget of 500 states, counted by TLC on the config as written. Above that, the chart draws only the paths to the rules that break, and when no rule breaks, the command writes no chart.mmd. It still checks each rule, and the report gives the state count and each bug path. To see the whole graph, make the model smaller.
Render charts with Pele. When the user asks for an image, or a chart is too large to read as text, follow references/render.md. Do not use a different renderer unless the user asks for it.
Give each chart and its Mermaid text to the person who must decide. Add one line for each bug: the rule, the reader's sentence for that rule, and the path as the report numbers it. Say what the model leaves out. Give the command that makes the files again, with a new --out folder.
When the model describes code, replay each bug path against the real code, as a test or a live repro, one step for each action. If a bug does not occur, think that the model is wrong until you show that it is not.
No reviews yet. Tell others what you thought.
No login needed. Share how it worked for you, ask a question, or note where it did not run.
No comments yet. Be the first to write one.
Plan types, function inputs and outputs, and module boundaries before implementation. Compare structurally different designs from multiple AI models, document the chosen approach, and guide coding while tracking changes to the agreed design.
Generate several candidate solutions in parallel, compare them against concrete criteria, and choose a base. Combine useful parts from other candidates, then verify the final artifact and document why each major choice was made.
Turn recurring work habits and communication preferences into a personal agent skill. It combines evidence from workspace conversations with direct questions, then drafts or updates instructions for how agents should work with you.
Monitor an open pull request, fix failing automated checks and merge conflicts, and address straightforward review feedback. Recheck after updates, report the resulting status, and hand decisions requiring design judgment back to the user.
Checks whether performance measurements support a speedup, slowdown, or technology choice. It examines bottlenecks, production settings, errors, repeatability, and completed work, then guides reporting with run counts, ranges, and a clear verdict.
Investigate what a code change could break beyond the edited files. Trace downstream effects, identify the key assumption behind its safety, and test that assumption with real code while clearly reporting unresolved risks.