statechart does not run on Windows (/bin/sh, CRLF in TLC output, temp folder, EPERM on empty --out) #17

statechart at 6c75f4e (current main) does not work on Windows. Observed on Windows 11 with Node.js 22.23.4, TLC 1.7.4 (TLA2TOOLS) and JDK 25 (JAVA).

Problems

1. The command dies at start with Error: spawn /bin/sh ENOENT, whatever the spec. The janitor in scripts/statechart.ts and killGroup in scripts/run.ts spawn /bin/sh directly.
2. A broken rule is not reported. With /bin/sh worked around, a spec whose INVARIANT breaks exits 2 with TLC exited 12 on <spec>, but its output names no rule that broke, and writes no chart or report. TLC's -tool output on Windows ends each @!@!@ENDMSG ... @!@!@ line with CRLF (23 of 101 lines in one run). The other lines end with LF. outputLines / fileLines in run.ts and linesOf in frontends/dot.ts split on "\n", so a \r stays at the end and the $-anchored patterns in frontends/messages.ts never match. Running the same spec and cfg with plain tlc2.TLC prints Error: Invariant <name> is violated.
3. The worker's temp folder survives a killed run. statechart.ts passes TMPDIR to the worker so its os.tmpdir() lands inside the folder the janitor removes. On Windows, os.tmpdir() reads TEMP / TMP and ignores TMPDIR, so the worker's statechart-* folder is created in the system temp folder and stays there after the parent is killed.
4. --out with an existing empty folder fails with EPERM, although the usage says the folder "must be new or empty". On Windows, renaming a folder onto an existing folder returns EPERM even when the target is empty. The renameSync(done, dest) fallback only handles ENOTEMPTY / EEXIST.
5. The test suite cannot run on Windows. Most of node --test test/*.test.ts spawns the statechart shell launcher directly and fails with spawn EFTYPE, so none of the above is covered there.

Repro

Any spec reproduces 1. For 2, a minimal spec whose invariant breaks in a few steps is enough. For 4, mkdir out then statechart Spec.tla --out out.

A fix we use downstream

This patch covers 1 to 3 and keeps the POSIX commands unchanged:
https://github.com/yasuyuki/agent-skills/blob/1d5d597607719817d68fa8d93ddb7b29aba07f81/bundles/pstack/patches/statechart-windows.patch

• On win32, killGroup runs taskkill /T /F /PID <pid>. The janitor is a small script evaluated by the same runtime (-e, or eval under Deno). It waits for stdin to end, then runs taskkill and removes the stage and temp folders.
• The worker gets TEMP and TMP as well as TMPDIR.
• TLC output and dot text are split on /\r?\n/.

With the patch on Windows, a spec where every rule holds exits 0 with its chart. A spec with two broken invariants exits 1 and names both rules with their shortest paths. Killing the parent mid-run leaves no java process, stage folder or temp folder. 4 and 5 are not addressed by the patch.