[rudycelekli]

Anyone charting a spec whose variable starts as a range of integers hits this. For example, Init == free = Seats with Seats == 1..3, or any x \in SUBSET (1..N). TLC prints a set it has not rebuilt as 1..3 in both the state graph and the traces. parseValue only read numbers, so the whole value came back as the string "1..3". A map that writes ${v.free.length} free then labels the start state "4 free" (the string's length), and the chart and the replay disagree with the spec on the very first state.

parseValue now reads a..b after an integer as the list of integers from a to b, the same shape it already gives a set like {1, 2, 3}. An empty range such as 1..0 becomes an empty list. Every other value form is read exactly as before.

Validation: a new test/tlc-interval.test.mjs checks parseValue on plain, negative, and nested ranges plus parseState, and runs tlc-to-chart.mjs on a hand-written graph whose start state is free = 1..3. It expects "3 free, 0 held" and no "4 free". Both tests fail on origin/main and pass with this change. With TLC 1.7.4, statechart.mjs from-spec on the seat spec now starts its trace at "3 free, 0 held" where it said "4 free" before. node scripts/validate-plugins.mjs, node scripts/generate-pstack-harness-trees.mjs --check, and git diff --check pass. On macOS, the rest of the statechart suite gives the same results as origin/main: 13 tests there expect a /tmp temp path and fail on both.

---

Note

Low Risk
Narrow parser change for TLC output format with regression tests; no auth, data, or API surface changes.

Overview
parseValue in the statechart TLC parser now expands TLC’s interval shorthand a..b (consecutive integer sets) into a numeric array, matching how explicit sets like {1, 2, 3} were already represented. Before this, values such as 1..3 stayed as strings, which broke maps that use .length on set variables and produced wrong initial state labels (e.g. “4 free” instead of “3 free”).

Empty or inverted ranges resolve to an empty list via Math.max(0, …). Other literal forms (booleans, bare numbers, records, etc.) are unchanged.

A new tlc-interval.test.mjs covers parseValue/parseState for positive and negative ranges and an end-to-end tlc-to-chart.mjs run on a DOT graph whose start state uses free = 1..3.

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