[rudycelekli]

chart-to-tla.mjs generated UNCHANGED == when a valid chart used UNCHANGED as a transition label. UNCHANGED is a TLA+ keyword, so the generated module could not be parsed.

The converter now reserves UNCHANGED when it creates action identifiers, producing UNCHANGED2 instead. The generated harness tree includes the same fix and regression test.

Validation: the regression produces UNCHANGED == on base and UNCHANGED2 == after this change. The focused test passes; the full statechart suite was attempted but exhausted the machine's temporary-disk space after unrelated tests.

---

Note

Low Risk
Small change to identifier reservation in the chart-to-TLA generator plus a focused regression test; no runtime or security impact.

Overview
Fixes invalid TLA+ output when a Mermaid transition label is UNCHANGED, which is a TLA+ operator and must not be used as a generated action definition name.

chart-to-tla.mjs now treats UNCHANGED like other reserved spec symbols (Init, Next, etc.), so the ident uniquifier emits UNCHANGED2 (or similar) for that label while the spec body can still use the real UNCHANGED stuttering operator.

A regression test runs the converter on a chart whose edge label is UNCHANGED and asserts the .tla file defines UNCHANGED2 == and not UNCHANGED ==.

^{Reviewed by Cursor Bugbot for commit 6760078. Bugbot is set up for automated code reviews on this repo. Configure here.}