From 5250a48cb7ac7e82d5a9604f45ed82a5055739df Mon Sep 17 00:00:00 2001
From: younes-io <git@younes.io>
Date: Sat, 11 Jul 2026 15:28:41 +0200
Subject: [PATCH] fix(tla-check): support TLC 1.7.4

---
 .claude-plugin/marketplace.json               |   4 +-
 .github/workflows/skill-ci.yml                |  33 +++
 VERSION                                       |   2 +-
 .../.claude-plugin/plugin.json                |   2 +-
 .../tla-workbenches/.codex-plugin/plugin.json |   2 +-
 .../tla-workbenches/skills/tla-check/SKILL.md |   6 +-
 .../skills/tla-check/scripts/tlc_check.sh     | 154 +++++++++++-
 .../tla-check/scripts/tlc_trace_summary.sh    |   2 +-
 scripts/tests/tla_check_test.sh               | 230 ++++++++++++++++++
 skills/tla-check/SKILL.md                     |   6 +-
 skills/tla-check/scripts/tlc_check.sh         | 154 +++++++++++-
 skills/tla-check/scripts/tlc_trace_summary.sh |   2 +-
 12 files changed, 562 insertions(+), 35 deletions(-)
 create mode 100755 scripts/tests/tla_check_test.sh

diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json
index dea11aa..7e2403a 100644
--- a/.claude-plugin/marketplace.json
+++ b/.claude-plugin/marketplace.json
@@ -5,13 +5,13 @@
   },
   "metadata": {
     "description": "Portable TLA+ agent skills for Claude Code and other Agent Skills clients.",
-    "version": "0.1.6"
+    "version": "0.1.7"
   },
   "plugins": [
     {
       "name": "tla-workbenches",
       "description": "TLA+ skills for checking specs and writing proofs.",
-      "version": "0.1.6",
+      "version": "0.1.7",
       "author": {
         "name": "younes-io"
       },
diff --git a/.github/workflows/skill-ci.yml b/.github/workflows/skill-ci.yml
index db03fa0..5cbc9f5 100644
--- a/.github/workflows/skill-ci.yml
+++ b/.github/workflows/skill-ci.yml
@@ -7,6 +7,39 @@ on:
       - main
 
 jobs:
+  tla-check:
+    name: TLC Script Tests
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Set up Java
+        uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: 17
+
+      - name: Shell syntax checks
+        run: |
+          set -euo pipefail
+          bash -n scripts/tests/tla_check_test.sh
+          bash -n skills/tla-check/scripts/tlc_check.sh
+          bash -n skills/tla-check/scripts/tlc_trace_summary.sh
+
+      - name: Run TLC behavioral tests
+        run: |
+          set -euo pipefail
+          jar_path="$RUNNER_TEMP/tla2tools.jar"
+          curl --fail --location --silent --show-error --retry 3 \
+            https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar \
+            --output "$jar_path"
+          printf '%s  %s\n' \
+            '936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88' \
+            "$jar_path" | sha256sum --check
+          ./scripts/tests/tla_check_test.sh --jar "$jar_path"
+
   tla-proof:
     name: TLA Proof Script Tests
     runs-on: ubuntu-latest
diff --git a/VERSION b/VERSION
index c946ee6..1180819 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-0.1.6
+0.1.7
diff --git a/plugins/tla-workbenches/.claude-plugin/plugin.json b/plugins/tla-workbenches/.claude-plugin/plugin.json
index 869792a..7795ff5 100644
--- a/plugins/tla-workbenches/.claude-plugin/plugin.json
+++ b/plugins/tla-workbenches/.claude-plugin/plugin.json
@@ -1,6 +1,6 @@
 {
   "name": "tla-workbenches",
-  "version": "0.1.6",
+  "version": "0.1.7",
   "description": "TLA+ skills for checking specs and writing proofs.",
   "author": {
     "name": "younes-io"
diff --git a/plugins/tla-workbenches/.codex-plugin/plugin.json b/plugins/tla-workbenches/.codex-plugin/plugin.json
index 1dc393e..5ecbc63 100644
--- a/plugins/tla-workbenches/.codex-plugin/plugin.json
+++ b/plugins/tla-workbenches/.codex-plugin/plugin.json
@@ -1,6 +1,6 @@
 {
   "name": "tla-workbenches",
-  "version": "0.1.6",
+  "version": "0.1.7",
   "description": "TLA+ skills for checking specs and writing proofs.",
   "author": {
     "name": "younes-io",
diff --git a/plugins/tla-workbenches/skills/tla-check/SKILL.md b/plugins/tla-workbenches/skills/tla-check/SKILL.md
index 335a62e..c0357cd 100644
--- a/plugins/tla-workbenches/skills/tla-check/SKILL.md
+++ b/plugins/tla-workbenches/skills/tla-check/SKILL.md
@@ -9,7 +9,7 @@ description: "Write and iteratively refine executable TLA+ specs (.tla) and TLC
 
 - TLA+ spec(s): `*.tla`
 - TLC config(s): `*.cfg`
-- TLC run artifacts: `.tla-check/runs/<run-id>/...` (logs, json trace if any)
+- TLC run artifacts: `.tla-check/runs/<run-id>/...` (logs and a JSON trace when TLC reports a counterexample)
 
 ## Non-Negotiables (Honesty Rules)
 
@@ -103,6 +103,8 @@ Run (from the `tla-check` skill directory):
 scripts/tlc_check.sh --spec path/to/Foo.tla --cfg path/to/Foo.cfg
 ```
 
+The runner uses TLC's stable `-tool` messages and converts counterexample states to JSON. This keeps it compatible with released TLA+ distributions without scraping presentation-oriented console text.
+
 This writes a run directory under the spec folder:
 - `.tla-check/runs/<run-id>/summary.json`
 - `.tla-check/runs/<run-id>/tlc.stdout`
@@ -124,7 +126,7 @@ If TLC passes:
 ## Resources
 
 ### scripts/
-- `scripts/tlc_check.sh`: run TLC with `-dumpTrace json`, capture logs, emit `summary.json`
+- `scripts/tlc_check.sh`: run TLC in tool mode, capture logs, and emit `summary.json`
 - `scripts/tlc_trace_summary.sh`: summarize a `counterexample.json` into step-by-step diffs (optional helper)
 
 ### references/
diff --git a/plugins/tla-workbenches/skills/tla-check/scripts/tlc_check.sh b/plugins/tla-workbenches/skills/tla-check/scripts/tlc_check.sh
index 2766177..5ad5abe 100755
--- a/plugins/tla-workbenches/skills/tla-check/scripts/tlc_check.sh
+++ b/plugins/tla-workbenches/skills/tla-check/scripts/tlc_check.sh
@@ -158,6 +158,133 @@ quote_cmd() {
   printf '%s\n' "$out"
 }
 
+write_tool_trace() {
+  local input="$1"
+  local output="$2"
+  local tmp_output
+  local trace_filter
+
+  tmp_output="$(mktemp "${output}.tmp.XXXXXX")"
+  trace_filter='
+def capture_value($capture; $name):
+  $capture.captures[] | select(.name == $name) | .string;
+
+def parse_vars:
+  [
+    match(
+      "(?ms)^(?:/\\\\[[:space:]]+)?(?<name>[A-Za-z_][A-Za-z0-9_]*)[[:space:]]*=[[:space:]]*(?<value>.*?)(?=^(?:/\\\\[[:space:]]+)?[A-Za-z_][A-Za-z0-9_]*[[:space:]]*=|\\z)";
+      "g"
+    )
+    | {
+        "key": capture_value(.; "name"),
+        "value": (capture_value(.; "value") | sub("[[:space:]]+$"; ""))
+      }
+  ] | from_entries;
+
+[
+  match(
+    "(?ms)@!@!@STARTMSG 2217:[0-9]+ @!@!@\\n(?<body>.*?)@!@!@ENDMSG 2217 @!@!@";
+    "g"
+  )
+  | capture_value(.; "body")
+  | capture("(?s)^(?<num>[0-9]+): <(?<label>[^>]+)>\\n(?<vars>.*)$")
+  | {
+      "num": (.num | tonumber),
+      "label": .label,
+      "vars": (.vars | parse_vars)
+    }
+  | select((.vars | length) > 0)
+] as $parsed
+| if ($parsed | length) == 0 then
+    error("no parsable states")
+  else
+    ($parsed | map([.num, .vars])) as $states
+    | {
+        "counterexample": {
+          "state": $states,
+          "action": [
+            range(1; ($parsed | length)) as $i
+            | [
+                $states[$i - 1],
+                {
+                  "name": ($parsed[$i].label | capture("^(?<name>[^[:space:]]+)").name),
+                  "source": $parsed[$i].label
+                },
+                $states[$i]
+              ]
+          ]
+        }
+      }
+  end
+'
+
+  if jq -MRse "$trace_filter" "$input" >"$tmp_output"; then
+    mv "$tmp_output" "$output"
+    return 0
+  fi
+  rm -f "$tmp_output"
+  return 1
+}
+
+collect_descendants() {
+  local root_pid="$1"
+  local frontier
+  local descendants
+  local next_frontier
+  local pid
+  local children
+
+  frontier="$root_pid"
+  descendants=""
+  while [[ -n "$frontier" ]]; do
+    next_frontier=""
+    for pid in $frontier; do
+      children="$(
+        ps -eo pid=,ppid= 2>/dev/null | awk -v p="$pid" '$2 == p { print $1 }'
+      )"
+      if [[ -n "$children" ]]; then
+        descendants="${descendants}${descendants:+$'\n'}${children}"
+        next_frontier="${next_frontier}${next_frontier:+ }${children//$'\n'/ }"
+      fi
+    done
+    frontier="$next_frontier"
+  done
+
+  if [[ -n "$descendants" ]]; then
+    printf '%s\n' "$descendants" | awk '!seen[$0]++'
+  fi
+}
+
+terminate_process_tree() {
+  local root_pid="$1"
+  local pids
+  local descendants
+
+  descendants="$(collect_descendants "$root_pid" || true)"
+  pids=""
+  if [[ -n "$descendants" ]]; then
+    pids="${descendants//$'\n'/ }"
+  fi
+  pids="${pids}${pids:+ }${root_pid}"
+  if [[ -n "$pids" ]]; then
+    kill $pids 2>/dev/null || true
+  fi
+
+  sleep 2
+
+  descendants="$(collect_descendants "$root_pid" || true)"
+  pids=""
+  if [[ -n "$descendants" ]]; then
+    pids="${descendants//$'\n'/ }"
+  fi
+  if kill -0 "$root_pid" 2>/dev/null; then
+    pids="${pids}${pids:+ }${root_pid}"
+  fi
+  if [[ -n "$pids" ]]; then
+    kill -9 $pids 2>/dev/null || true
+  fi
+}
+
 find_tla2tools_jar() {
   local spec_dir="$1"
   local explicit="${2:-}"
@@ -339,13 +466,11 @@ cmd=(
   "-cp"
   "$jar_path"
   "tlc2.TLC"
+  "-tool"
   "-workers"
   "$WORKERS"
   "-metadir"
   "$meta_root"
-  "-dumpTrace"
-  "json"
-  "$trace_path"
   "-config"
   "$cfg_arg"
   "$module"
@@ -367,9 +492,7 @@ if (( TIMEOUT_SECS > 0 )); then
     sleep "$TIMEOUT_SECS"
     if kill -0 "$tlc_pid" 2>/dev/null; then
       : >"$timeout_flag"
-      kill "$tlc_pid" 2>/dev/null || true
-      sleep 2
-      kill -9 "$tlc_pid" 2>/dev/null || true
+      terminate_process_tree "$tlc_pid"
     fi
   ) &
   watchdog_pid=$!
@@ -398,15 +521,22 @@ duration_ms=$(( (finished_epoch - started_epoch) * 1000 ))
 
 metadir_used="$(pick_metadir "$meta_root" || true)"
 trace_exists=false
-if [[ -f "$trace_path" ]]; then
-  trace_exists=true
+trace_parse_error=false
+if grep -Fq '@!@!@STARTMSG 2217:' "$stdout_path"; then
+  if write_tool_trace "$stdout_path" "$trace_path" >/dev/null 2>&1; then
+    trace_exists=true
+  else
+    trace_parse_error=true
+  fi
 fi
 
-if [[ "$trace_exists" == true ]]; then
-  status="fail"
-elif [[ "$timed_out" == true ]]; then
+if [[ "$timed_out" == true ]]; then
   status="timeout"
-elif [[ "$exit_code" -eq 0 ]]; then
+elif [[ "$trace_exists" == true ]]; then
+  status="fail"
+elif [[ "$trace_parse_error" == true ]]; then
+  status="error"
+elif [[ "$exit_code" -eq 0 ]] && grep -Fq '@!@!@STARTMSG 2193:0 @!@!@' "$stdout_path"; then
   status="pass"
 else
   status="error"
diff --git a/plugins/tla-workbenches/skills/tla-check/scripts/tlc_trace_summary.sh b/plugins/tla-workbenches/skills/tla-check/scripts/tlc_trace_summary.sh
index a9030ce..29fc76a 100755
--- a/plugins/tla-workbenches/skills/tla-check/scripts/tlc_trace_summary.sh
+++ b/plugins/tla-workbenches/skills/tla-check/scripts/tlc_trace_summary.sh
@@ -5,7 +5,7 @@ set -euo pipefail
 
 usage() {
   cat <<'EOF'
-Summarize a TLC -dumpTrace json counterexample.
+Summarize a TLC counterexample trace JSON file.
 
 Usage:
   tlc_trace_summary.sh --trace path/to/counterexample.json [options]
diff --git a/scripts/tests/tla_check_test.sh b/scripts/tests/tla_check_test.sh
new file mode 100755
index 0000000..0c59be8
--- /dev/null
+++ b/scripts/tests/tla_check_test.sh
@@ -0,0 +1,230 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+usage() {
+  printf 'Usage: %s --jar path/to/tla2tools.jar\n' "${0##*/}"
+}
+
+jar=""
+while [[ $# -gt 0 ]]; do
+  case "$1" in
+    --jar)
+      [[ $# -ge 2 ]] || { usage >&2; exit 2; }
+      jar="$2"
+      shift 2
+      ;;
+    -h|--help)
+      usage
+      exit 0
+      ;;
+    *)
+      printf 'unknown argument: %s\n' "$1" >&2
+      exit 2
+      ;;
+  esac
+done
+
+[[ -n "$jar" ]] || { usage >&2; exit 2; }
+[[ -f "$jar" ]] || { printf 'tla2tools.jar not found: %s\n' "$jar" >&2; exit 2; }
+command -v java >/dev/null 2>&1 || { printf 'missing required command: java\n' >&2; exit 2; }
+command -v jq >/dev/null 2>&1 || { printf 'missing required command: jq\n' >&2; exit 2; }
+
+repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd -P)"
+runner="$repo_root/skills/tla-check/scripts/tlc_check.sh"
+tmp_root="$(mktemp -d "${TMPDIR:-/tmp}/tla-check-test.XXXXXX")"
+child_pid_file="$tmp_root/timeout-child.pid"
+
+cleanup() {
+  if [[ -f "$child_pid_file" ]]; then
+    child_pid="$(cat "$child_pid_file" 2>/dev/null || true)"
+    [[ -z "$child_pid" ]] || kill -9 "$child_pid" 2>/dev/null || true
+  fi
+  rm -rf "$tmp_root"
+}
+trap cleanup EXIT
+
+fail() {
+  printf 'FAIL: %s\n' "$1" >&2
+  exit 1
+}
+
+assert_json() {
+  local path="$1"
+  local filter="$2"
+  local message="$3"
+  jq -e "$filter" "$path" >/dev/null || fail "$message"
+}
+
+summary_under() {
+  local root="$1"
+  local summary
+  summary="$(find "$root" -name summary.json -type f | head -n 1 || true)"
+  [[ -n "$summary" ]] || fail "missing summary.json under $root"
+  printf '%s\n' "$summary"
+}
+
+fixture="$tmp_root/fake"
+mkdir -p "$fixture"
+printf '%s\n' '---- MODULE Spec ----' 'Init == TRUE' 'Next == FALSE' '====' >"$fixture/Spec.tla"
+printf '%s\n' 'INIT Init' 'NEXT Next' >"$fixture/Spec.cfg"
+: >"$fixture/tla2tools.jar"
+
+fake_java="$fixture/java"
+cat >"$fake_java" <<'FAKE_JAVA'
+#!/usr/bin/env bash
+set -euo pipefail
+
+case "${FAKE_TLC_MODE:-pass}" in
+  pass)
+    printf '%s\n' \
+      '@!@!@STARTMSG 2193:0 @!@!@' \
+      'Model checking completed. No error has been found.' \
+      '@!@!@ENDMSG 2193 @!@!@'
+    ;;
+  error)
+    printf 'TLC internal error\n' >&2
+    exit 3
+    ;;
+  counterexample)
+    printf '%s\n' \
+      '@!@!@STARTMSG 2110:1 @!@!@' \
+      'Invariant Safety is violated.' \
+      '@!@!@ENDMSG 2110 @!@!@' \
+      '@!@!@STARTMSG 2217:4 @!@!@' \
+      '1: <Initial predicate>' \
+      '/\ x = 0' \
+      '@!@!@ENDMSG 2217 @!@!@' \
+      '@!@!@STARTMSG 2217:4 @!@!@' \
+      '2: <Increment line 1, col 1 to line 1, col 2 of module Spec>' \
+      '/\ x = 1' \
+      '@!@!@ENDMSG 2217 @!@!@'
+    ;;
+  malformed)
+    printf '%s\n' \
+      '@!@!@STARTMSG 2217:4 @!@!@' \
+      'not a state' \
+      '@!@!@ENDMSG 2217 @!@!@'
+    ;;
+  timeout)
+    (sleep 30) &
+    child_pid=$!
+    printf '%s\n' "$child_pid" >"$FAKE_TLC_CHILD_PID_FILE"
+    wait "$child_pid"
+    ;;
+esac
+FAKE_JAVA
+chmod +x "$fake_java"
+
+run_fake() {
+  local mode="$1"
+  local expected_exit="$2"
+  local out_root="$tmp_root/fake-$mode"
+  local actual_exit
+  local extra_args=()
+
+  if [[ "$mode" == timeout ]]; then
+    extra_args+=(--timeout-secs 1)
+  fi
+
+  set +e
+  FAKE_TLC_MODE="$mode" FAKE_TLC_CHILD_PID_FILE="$child_pid_file" \
+    "$runner" \
+      --spec "$fixture/Spec.tla" \
+      --cfg "$fixture/Spec.cfg" \
+      --jar "$fixture/tla2tools.jar" \
+      --java "$fake_java" \
+      --out-root "$out_root" \
+      ${extra_args[@]+"${extra_args[@]}"} \
+      >/dev/null 2>&1
+  actual_exit=$?
+  set -e
+
+  [[ "$actual_exit" -eq "$expected_exit" ]] || fail "$mode expected exit $expected_exit, got $actual_exit"
+  summary_under "$out_root"
+}
+
+pass_summary="$(run_fake pass 0)"
+assert_json "$pass_summary" '.status == "pass" and (.command | any(. == "-tool"))' "fake pass classification"
+
+error_summary="$(run_fake error 12)"
+assert_json "$error_summary" '.status == "error" and .exit_code == 3' "fake error classification"
+
+counterexample_summary="$(run_fake counterexample 10)"
+assert_json "$counterexample_summary" '
+  .status == "fail" and
+  .counterexample_summary.states_total == 2 and
+  .counterexample_summary.steps[1].action.name == "Increment"
+' "counterexample conversion"
+
+malformed_summary="$(run_fake malformed 12)"
+assert_json "$malformed_summary" '.status == "error" and .counterexample_json_path == null' "malformed trace classification"
+
+timeout_summary="$(run_fake timeout 11)"
+assert_json "$timeout_summary" '.status == "timeout" and .timed_out == true and .exit_code == 124' "timeout classification"
+child_pid="$(cat "$child_pid_file")"
+sleep 1
+kill -0 "$child_pid" 2>/dev/null && fail "timeout left a descendant process running"
+
+real_fixture="$tmp_root/real"
+mkdir -p "$real_fixture"
+cat >"$real_fixture/Flawed.tla" <<'EOF'
+------------------------------ MODULE Flawed ------------------------------
+EXTENDS Naturals
+VARIABLE x
+Vars == <<x>>
+Init == x = 0
+Next == /\ x = 0 /\ x' = 1
+Safety == x = 0
+Spec == Init /\ [][Next]_Vars
+=============================================================================
+EOF
+cat >"$real_fixture/Flawed.cfg" <<'EOF'
+SPECIFICATION Spec
+INVARIANT Safety
+CHECK_DEADLOCK FALSE
+EOF
+cat >"$real_fixture/Fixed.tla" <<'EOF'
+------------------------------- MODULE Fixed -------------------------------
+EXTENDS Naturals
+VARIABLE x
+Vars == <<x>>
+Init == x = 0
+Next == /\ x = 0 /\ x' = 1
+Safety == x \in 0..1
+Spec == Init /\ [][Next]_Vars
+=============================================================================
+EOF
+cat >"$real_fixture/Fixed.cfg" <<'EOF'
+SPECIFICATION Spec
+INVARIANT Safety
+CHECK_DEADLOCK FALSE
+EOF
+
+run_real() {
+  local module="$1"
+  local expected_exit="$2"
+  local out_root="$tmp_root/real-$module"
+  local output="$tmp_root/$module.summary.json"
+  local actual_exit
+
+  set +e
+  "$runner" \
+    --spec "$real_fixture/$module.tla" \
+    --cfg "$real_fixture/$module.cfg" \
+    --jar "$jar" \
+    --workers 1 \
+    --out-root "$out_root" >"$output"
+  actual_exit=$?
+  set -e
+
+  [[ "$actual_exit" -eq "$expected_exit" ]] || fail "$module expected exit $expected_exit, got $actual_exit"
+  printf '%s\n' "$output"
+}
+
+flawed_summary="$(run_real Flawed 10)"
+assert_json "$flawed_summary" '.status == "fail" and .counterexample_summary.states_total == 2' "real counterexample"
+
+fixed_summary="$(run_real Fixed 0)"
+assert_json "$fixed_summary" '.status == "pass" and .counterexample_json_path == null' "real passing model"
+
+printf 'PASS: tla-check behavioral tests\n'
diff --git a/skills/tla-check/SKILL.md b/skills/tla-check/SKILL.md
index 335a62e..c0357cd 100644
--- a/skills/tla-check/SKILL.md
+++ b/skills/tla-check/SKILL.md
@@ -9,7 +9,7 @@ description: "Write and iteratively refine executable TLA+ specs (.tla) and TLC
 
 - TLA+ spec(s): `*.tla`
 - TLC config(s): `*.cfg`
-- TLC run artifacts: `.tla-check/runs/<run-id>/...` (logs, json trace if any)
+- TLC run artifacts: `.tla-check/runs/<run-id>/...` (logs and a JSON trace when TLC reports a counterexample)
 
 ## Non-Negotiables (Honesty Rules)
 
@@ -103,6 +103,8 @@ Run (from the `tla-check` skill directory):
 scripts/tlc_check.sh --spec path/to/Foo.tla --cfg path/to/Foo.cfg
 ```
 
+The runner uses TLC's stable `-tool` messages and converts counterexample states to JSON. This keeps it compatible with released TLA+ distributions without scraping presentation-oriented console text.
+
 This writes a run directory under the spec folder:
 - `.tla-check/runs/<run-id>/summary.json`
 - `.tla-check/runs/<run-id>/tlc.stdout`
@@ -124,7 +126,7 @@ If TLC passes:
 ## Resources
 
 ### scripts/
-- `scripts/tlc_check.sh`: run TLC with `-dumpTrace json`, capture logs, emit `summary.json`
+- `scripts/tlc_check.sh`: run TLC in tool mode, capture logs, and emit `summary.json`
 - `scripts/tlc_trace_summary.sh`: summarize a `counterexample.json` into step-by-step diffs (optional helper)
 
 ### references/
diff --git a/skills/tla-check/scripts/tlc_check.sh b/skills/tla-check/scripts/tlc_check.sh
index 2766177..5ad5abe 100755
--- a/skills/tla-check/scripts/tlc_check.sh
+++ b/skills/tla-check/scripts/tlc_check.sh
@@ -158,6 +158,133 @@ quote_cmd() {
   printf '%s\n' "$out"
 }
 
+write_tool_trace() {
+  local input="$1"
+  local output="$2"
+  local tmp_output
+  local trace_filter
+
+  tmp_output="$(mktemp "${output}.tmp.XXXXXX")"
+  trace_filter='
+def capture_value($capture; $name):
+  $capture.captures[] | select(.name == $name) | .string;
+
+def parse_vars:
+  [
+    match(
+      "(?ms)^(?:/\\\\[[:space:]]+)?(?<name>[A-Za-z_][A-Za-z0-9_]*)[[:space:]]*=[[:space:]]*(?<value>.*?)(?=^(?:/\\\\[[:space:]]+)?[A-Za-z_][A-Za-z0-9_]*[[:space:]]*=|\\z)";
+      "g"
+    )
+    | {
+        "key": capture_value(.; "name"),
+        "value": (capture_value(.; "value") | sub("[[:space:]]+$"; ""))
+      }
+  ] | from_entries;
+
+[
+  match(
+    "(?ms)@!@!@STARTMSG 2217:[0-9]+ @!@!@\\n(?<body>.*?)@!@!@ENDMSG 2217 @!@!@";
+    "g"
+  )
+  | capture_value(.; "body")
+  | capture("(?s)^(?<num>[0-9]+): <(?<label>[^>]+)>\\n(?<vars>.*)$")
+  | {
+      "num": (.num | tonumber),
+      "label": .label,
+      "vars": (.vars | parse_vars)
+    }
+  | select((.vars | length) > 0)
+] as $parsed
+| if ($parsed | length) == 0 then
+    error("no parsable states")
+  else
+    ($parsed | map([.num, .vars])) as $states
+    | {
+        "counterexample": {
+          "state": $states,
+          "action": [
+            range(1; ($parsed | length)) as $i
+            | [
+                $states[$i - 1],
+                {
+                  "name": ($parsed[$i].label | capture("^(?<name>[^[:space:]]+)").name),
+                  "source": $parsed[$i].label
+                },
+                $states[$i]
+              ]
+          ]
+        }
+      }
+  end
+'
+
+  if jq -MRse "$trace_filter" "$input" >"$tmp_output"; then
+    mv "$tmp_output" "$output"
+    return 0
+  fi
+  rm -f "$tmp_output"
+  return 1
+}
+
+collect_descendants() {
+  local root_pid="$1"
+  local frontier
+  local descendants
+  local next_frontier
+  local pid
+  local children
+
+  frontier="$root_pid"
+  descendants=""
+  while [[ -n "$frontier" ]]; do
+    next_frontier=""
+    for pid in $frontier; do
+      children="$(
+        ps -eo pid=,ppid= 2>/dev/null | awk -v p="$pid" '$2 == p { print $1 }'
+      )"
+      if [[ -n "$children" ]]; then
+        descendants="${descendants}${descendants:+$'\n'}${children}"
+        next_frontier="${next_frontier}${next_frontier:+ }${children//$'\n'/ }"
+      fi
+    done
+    frontier="$next_frontier"
+  done
+
+  if [[ -n "$descendants" ]]; then
+    printf '%s\n' "$descendants" | awk '!seen[$0]++'
+  fi
+}
+
+terminate_process_tree() {
+  local root_pid="$1"
+  local pids
+  local descendants
+
+  descendants="$(collect_descendants "$root_pid" || true)"
+  pids=""
+  if [[ -n "$descendants" ]]; then
+    pids="${descendants//$'\n'/ }"
+  fi
+  pids="${pids}${pids:+ }${root_pid}"
+  if [[ -n "$pids" ]]; then
+    kill $pids 2>/dev/null || true
+  fi
+
+  sleep 2
+
+  descendants="$(collect_descendants "$root_pid" || true)"
+  pids=""
+  if [[ -n "$descendants" ]]; then
+    pids="${descendants//$'\n'/ }"
+  fi
+  if kill -0 "$root_pid" 2>/dev/null; then
+    pids="${pids}${pids:+ }${root_pid}"
+  fi
+  if [[ -n "$pids" ]]; then
+    kill -9 $pids 2>/dev/null || true
+  fi
+}
+
 find_tla2tools_jar() {
   local spec_dir="$1"
   local explicit="${2:-}"
@@ -339,13 +466,11 @@ cmd=(
   "-cp"
   "$jar_path"
   "tlc2.TLC"
+  "-tool"
   "-workers"
   "$WORKERS"
   "-metadir"
   "$meta_root"
-  "-dumpTrace"
-  "json"
-  "$trace_path"
   "-config"
   "$cfg_arg"
   "$module"
@@ -367,9 +492,7 @@ if (( TIMEOUT_SECS > 0 )); then
     sleep "$TIMEOUT_SECS"
     if kill -0 "$tlc_pid" 2>/dev/null; then
       : >"$timeout_flag"
-      kill "$tlc_pid" 2>/dev/null || true
-      sleep 2
-      kill -9 "$tlc_pid" 2>/dev/null || true
+      terminate_process_tree "$tlc_pid"
     fi
   ) &
   watchdog_pid=$!
@@ -398,15 +521,22 @@ duration_ms=$(( (finished_epoch - started_epoch) * 1000 ))
 
 metadir_used="$(pick_metadir "$meta_root" || true)"
 trace_exists=false
-if [[ -f "$trace_path" ]]; then
-  trace_exists=true
+trace_parse_error=false
+if grep -Fq '@!@!@STARTMSG 2217:' "$stdout_path"; then
+  if write_tool_trace "$stdout_path" "$trace_path" >/dev/null 2>&1; then
+    trace_exists=true
+  else
+    trace_parse_error=true
+  fi
 fi
 
-if [[ "$trace_exists" == true ]]; then
-  status="fail"
-elif [[ "$timed_out" == true ]]; then
+if [[ "$timed_out" == true ]]; then
   status="timeout"
-elif [[ "$exit_code" -eq 0 ]]; then
+elif [[ "$trace_exists" == true ]]; then
+  status="fail"
+elif [[ "$trace_parse_error" == true ]]; then
+  status="error"
+elif [[ "$exit_code" -eq 0 ]] && grep -Fq '@!@!@STARTMSG 2193:0 @!@!@' "$stdout_path"; then
   status="pass"
 else
   status="error"
diff --git a/skills/tla-check/scripts/tlc_trace_summary.sh b/skills/tla-check/scripts/tlc_trace_summary.sh
index a9030ce..29fc76a 100755
--- a/skills/tla-check/scripts/tlc_trace_summary.sh
+++ b/skills/tla-check/scripts/tlc_trace_summary.sh
@@ -5,7 +5,7 @@ set -euo pipefail
 
 usage() {
   cat <<'EOF'
-Summarize a TLC -dumpTrace json counterexample.
+Summarize a TLC counterexample trace JSON file.
 
 Usage:
   tlc_trace_summary.sh --trace path/to/counterexample.json [options]