[Amyssjj]

On Windows the statechart command crashed after its first TLC run. Run as the worker alone, a rule that broke read as a TLC failure.

• /bin/sh. killGroup (run.ts) and the cleanup watcher (statechart.ts) spawned /bin/sh. Node resolves that to C:\bin\sh, so the spawn failed with ENOENT, and the detached worker and its folders outlived the command. On Windows, killGroup runs taskkill /T /F /PID. The watcher is janitor.ts, run on the worker's runtime: when the command's pipe closes, it kills the worker's tree and removes the stage and temporary folders. The command kills the tree only while the worker runs, since Windows can give a finished worker's PID to another process. POSIX keeps the same /bin/sh commands.
• CRLF. Java on Windows ends lines with CRLF. outputLines, fileLines (run.ts), and linesOf (frontends/dot.ts) split on \n only, so each line kept a \r. The message and verdict regexes, which end in $, then matched nothing: TLC's exit 12 read as "its output names no rule that broke", and marks went missing from the chart. The splitters now drop the \r before each \n.
• TEMP. The worker gets TEMP and TMP beside TMPDIR, since os.tmpdir() reads TEMP on Windows. TLC's folder now sits inside the folder the command removes.
• Console windows. The detached worker has no console, so each java run opened a Windows Terminal window. The java and mise spawns pass windowsHide, which Node ignores elsewhere.

cli.test.ts replays DieHard, MediaPlayer, and MediaPlayerProps with their TLC output and dump in CRLF, and checks the chart and report. It runs on every platform. Without the CRLF fix it fails with the Windows error. harness/pstack/claude-code gets the same files, byte for byte.

Tested on Windows 11, Git Bash, Node 24.13, Temurin 25.0.5, tla2tools 1.7.4:

• Two real models (20 and 18 states) give the expected report, marks, and chart through the unmodified scripts/statechart launcher.
• Ctrl+C (a real CTRL_C_EVENT) exits 130 and leaves no java and no folder. After a forced kill of the command, the janitor kills java and removes both folders. No console window appears.
• With TLA2TOOLS set, all 33 corpus specs give the committed chart and report against real TLC, and the differential, plain-TLC, and chart-budget tests pass.
• Unit tests pass, except render.test.ts, whose execFileSync("npm") cannot start npm.cmd.

These test-harness limits on Windows are unchanged by this PR:

• The CLI tests run test/java.ts as JAVA, which Windows cannot execute. In a scratch copy that starts a .ts JAVA through Node, all 33 replays, the dump-order test, and the new CRLF test pass.
• tlc-out.test.ts compares against plain TLC's CRLF output. With CRLF normalized, all 34 tests pass.
• The non-ASCII folder test fails in setup: Node 24's fs.cpSync names spec-é as spec-é. The CLI itself checks a spec in a spec-é folder.
• config-fuzz needs a JDK to run ConfigOracle.java.
• The launcher, symlink, and SIGKILL tests need POSIX.

Not run: the suite on Linux or macOS, because no POSIX machine was at hand. The POSIX branches run the same commands, and split(/\r?\n/) equals split("\n") on LF text. CI covers it.

🤖 Generated with Claude Code