Repository navigation
statechart: a relative TLA2TOOLS or JAVA path fails, because TLC runs in the snapshot folder #973
Description
What happens
findTlc in pstack/skills/statechart/scripts/tlc-tools.mjs checks that TLA2TOOLS and JAVA exist from the caller's working directory, then returns them as given. tlc() in statechart.mjs starts java with cwd set to the folder of the spec's snapshot copy under $TMPDIR/statechart-inputs-*/. Java resolves a relative -cp against that folder, so it cannot find the jar, and from-spec exits with cannot run TLC. A relative JAVA with a slash, such as ./jdk/bin/java, starts from the same folder.
Reproduce
Tested at 9e88dad on macOS with Node 25.8.0. The stand-in java prints the folder it runs in and whether it can see the -cp jar.
mkdir repro && cd repro && mkdir tools && touch tools/tla2tools.jar
cat > fake-java <<'EOF'
#!/bin/sh
cp=""; prev=""; for a in "$@"; do [ "$prev" = "-cp" ] && cp="$a"; prev="$a"; done
echo "java runs in: $PWD" >&2
if [ -e "$cp" ]; then echo "jar $cp: found" >&2; else echo "jar $cp: not found" >&2; fi
exit 1
EOF
chmod +x fake-java
printf -- '---- MODULE Spec ----\nEXTENDS Naturals\nVARIABLE x\nInit == x = 0\nNext == x'"'"' = x\n====\n' > Spec.tla
printf 'INIT Init\nNEXT Next\n' > Spec.cfg
S=/path/to/pstack/skills/statechart/scripts/statechart.mjs
export JAVA=$PWD/fake-java
TLA2TOOLS=tools/tla2tools.jar node $S from-spec Spec.tla # writes Spec.map.mjs
TLA2TOOLS=tools/tla2tools.jar node $S from-spec Spec.tla
TLA2TOOLS=$PWD/tools/tla2tools.jar node $S from-spec Spec.tlaWith the relative path:
cannot run TLC with .../fake-java -cp tools/tla2tools.jar: java exited 1:
java runs in: $TMPDIR/statechart-inputs-B8EIpr/<absolute path of repro>
jar tools/tla2tools.jar: not found
With the absolute path, java runs in the same snapshot folder and prints jar <absolute path>: found.
Expected
A TLA2TOOLS or JAVA path that exists from the caller's directory, which findTlc already checks, also works when TLC runs.
Activity
deanrie commentedon Oct 27, 2026
Hey @dameronma-ma, this survived the rewrite in #977. The files you name are gone, but the same shape is in
scripts/run.tsonmain164ced1:findTlcreturnsTLA2TOOLSandJAVAexactly as given (line 195), andrunJavaspawns java withcwdset to the fresh temp folder (line 296), so a relative-cpis resolved against$TMPDIR/statechart-*/and a relativeJAVAwith a slash is looked up there too.Your repro adapted to the new entry point (
statechart Spec.tla --out DIR, Node 25.9, macOS):The message now comes from the SANY step rather than TLC, since that is the first java call, but the cause is the same.
path.resolve()on both values infindTlcwhen they contain a path separator would close it; themisebranch already returns absolute paths.kairan commentedon Oct 31, 2026
Confirming from our side on macOS (Node 25.x): still reproducible on
mainat 4dd1d05 with the current entry point.We use the statechart skill from a user-level install (
npx skills/~/.agents/skills) when redrawing NapTap sleep charts. SettingTLA2TOOLS=tools/tla2tools.jar(relative to the cwd) fails becauserunJavausescwd: dirunder$TMPDIR/statechart-*/, so the relative-cpjar is not found. An absoluteTLA2TOOLS=$PWD/tools/tla2tools.jarworks.Same minimal repro as @deanrie’s comment, adapted to
statechart Spec.tla --out out:We closed kairan/NapTap#110 (vendoring the skill) partly because this upstream behavior makes a repo-local relative jar path unreliable unless
findTlcresolves env paths against the caller’s cwd before spawning Java.Would be great if
findTlcreturnedpath.resolve(cwd, TLA2TOOLS)(and similarly for relativeJAVAwith a slash) when env overrides are set.Ehsan-hash commentedon Oct 31, 2026
Thanks @kairan for confirming this with the current entry point. #1017 addresses the same case: it resolves relative
TLA2TOOLSand path-shapedJAVAvalues against the caller's directory before Java starts in the temporary directory. It is still awaiting maintainer review, so using an absolute path remains the workaround on main.