feat(statechart): sync upstream to 076f4b2f and make --cover explicit

.github/workflows/statechart-compat.yml

@@ -0,0 +1,65 @@
+name: statechart-compat
+
+# Real statechart regression + PNG rendering on both CI platforms and both supported Node lines.
+# This workflow is additive: check.yml keeps running the dependency-free `npm test` job.
+on:
+  push:
+    branches: [main]
+  pull_request:
+    paths:
+      - "skills/statechart/**"
+      - "adapters/pi/statechart/**"
+      - "scripts/statechart-*.test.mjs"
+      - "scripts/check-statechart-png.mjs"
+      - "scripts/fixtures/statechart-sync/**"
+      - ".github/workflows/statechart-compat.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: statechart-compat-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  compat:
+    name: statechart (${{ matrix.os }}, node ${{ matrix.node }})
+    runs-on: ${{ matrix.os }}
+    timeout-minutes: 20
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        node: ["22", "24"]
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
+      - uses: actions/setup-node@49933ea5288caeca8642d1e84afbd3f7d6820020 # v4.4.0
+        with:
+          node-version: ${{ matrix.node }}
+          cache: npm
+      - uses: actions/setup-java@c5195efecf7bdfc987ee8bae7a71cb8b11521c00 # v4.7.1
+        with:
+          distribution: temurin
+          java-version: "21"
+      - name: Install TLC 1.8.0
+        # The jar URL is pinned to the TLA+ release the regression was verified against locally.
+        # If this asset moves, replace the URL rather than downgrading the assertions.
+        run: |
+          curl --fail --location --retry 3 \
+            --output "$RUNNER_TEMP/tla2tools.jar" \
+            https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
+          echo "TLA2TOOLS=$RUNNER_TEMP/tla2tools.jar" >> "$GITHUB_ENV"
+          echo "JAVA=$JAVA_HOME/bin/java" >> "$GITHUB_ENV"
+      - name: Install dependencies
+        run: npm ci --include=dev
+      - name: TLC version
+        run: "$JAVA -cp $TLA2TOOLS tlc2.TLC -help 2>&1 | head -5"
+      - name: CoverGap regression (adapter entry, real TLC)
+        env:
+          STATECHART_PNG_REQUIRE: "1"
+        run: node --test scripts/statechart-sync.test.mjs
+      - name: PNG smoke (real --png, PNG signature and size)
+        env:
+          STATECHART_PNG_REQUIRE: "1"
+        run: node scripts/check-statechart-png.mjs

CHANGELOG.md

@@ -2,6 +2,11 @@
 
 Changes to the Pi adaptation are recorded here. Upstream pstack remains pinned to the revision documented in [sources](docs/sources.md).
 
+## Unreleased
+
+- Sync only statechart to cursor/plugins@076f4b2f for #40, retaining upstream scripts and tests byte-for-byte. `--cover` is explicit and reports omitted states/transitions; remove the retired OutputFolder example.
+- Add a Pi execution adapter that never installs TLC/Java/mise and preserves `.mmd` output when PNG rendering is unavailable. Pele/resvg remain optional downloads in the upstream user cache, outside the npm package.
+
 ## 0.3.13
 
 - Fix #35 (part 2): formal verification gate triggers on read tool calls only when upgraded in the same turn by write/edit to workspace skill directories (`.pi/skills/**` or `.agents/skills/**`); read alone no longer triggers the gate (read 单独不再触发).

README.md

@@ -8,7 +8,7 @@
 
 pstack 是一套工程方法：24 条工程原则、23 个工作流程（调查、修 bug、做功能、重构、自主运行……）、独立审阅、多模型分工，以及形式化验证。这个包把它们做成原生的 Pi 技能和扩展，装上就能用。
 
-> 非官方移植。上游固定在 pstack 0.15.30（`eb4db2b5`）。
+> 非官方移植。上游基线为 pstack 0.15.30（`eb4db2b5`）；仅 statechart 同步到 `076f4b2f`，来源与适配见 [来源记录](docs/sources.md)。
 
 ## 能做什么
 

THIRD_PARTY_NOTICES.md

@@ -5,7 +5,9 @@
 - 作者：Lauren Tan（@poteto）。
 - 官方仓库：https://github.com/cursor/plugins/tree/eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10/pstack
 - 参考版本：0.15.30。
-- 固定提交：eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10。
+- 固定基线提交：eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10。
+- statechart 单独固定到 [076f4b2f57844ff9eb4ada914d4763884d40146e](https://github.com/cursor/plugins/tree/076f4b2f57844ff9eb4ada914d4763884d40146e/pstack/skills/statechart)，仅更新 `pstack/skills/statechart/**`，其他技能保持基线。原始脚本与测试逐字节生成；Pi 的 TLC 来源与 PNG 降级行为放在 `adapters/pi/statechart/`，SKILL.md 的宿主说明放在适配模板。
+- `--png` 沿用上游按需安装 `pele@1.8.0`（MIT）与 `@resvg/resvg-js@2.6.2`（MPL-2.0）的方式，依赖位于用户缓存；它们及平台原生二进制不包含在此 npm 包。依赖许可随按需下载的包分发。
 - 许可：MIT，Copyright (c) 2026 Lauren Tan。
 - 许可原文：[LICENSES/pstack.txt](LICENSES/pstack.txt)。
 

adapters/pi/statechart/entry.mjs

@@ -0,0 +1,35 @@
+#!/usr/bin/env node
+// Pi execution boundary for the byte-preserved statechart snapshot.
+import assert from 'node:assert/strict';
+import { registerHooks } from 'node:module';
+
+const upstream = new URL('../../../skills/statechart/scripts/statechart.mjs', import.meta.url).href;
+const tools = new URL('./tlc-tools.mjs', import.meta.url).href;
+
+function replaceOnce(source, before, after) {
+  assert.equal(source.split(before).length, 2, 'Statechart adapter no longer matches the pinned upstream; review the adapter before updating the snapshot');
+  return source.replace(before, after);
+}
+
+registerHooks({
+  resolve(specifier, context, nextResolve) {
+    if (context.parentURL === upstream && specifier === './tlc-tools.mjs') {
+      return { url: tools, shortCircuit: true };
+    }
+    return nextResolve(specifier, context);
+  },
+  load(url, context, nextLoad) {
+    const loaded = nextLoad(url, context);
+    if (url !== upstream) return loaded;
+    let source = typeof loaded.source === 'string' ? loaded.source : Buffer.from(loaded.source).toString('utf8');
+    source = replaceOnce(source,
+      '  } catch (e) {\n    throw new CannotFinish(e.message);\n  }\n}\n\nconst rel',
+      '  } catch (e) {\n    if (command === "render") throw new CannotFinish(`${e.message}\\nThe input .mmd file is still available.`);\n    console.error(`PNG unavailable: ${e.message}\\nContinuing with .mmd output.`);\n    return null;\n  }\n}\n\nconst rel');
+    source = replaceOnce(source,
+      '  if (renderer && pngs.length < charts.length) return 2;',
+      '  if (renderer && pngs.length < charts.length) console.error("PNG unavailable for some charts; the .mmd files still contain the full charts.");');
+    return { ...loaded, source };
+  },
+});
+
+await import(upstream);

adapters/pi/statechart/skill-tail.md

@@ -0,0 +1,13 @@
+## Pi execution and authority
+
+Adapted from Lauren Tan's pstack, MIT. The upstream body above is byte-preserved from cursor/plugins@076f4b2f.
+
+The chart entry is `node <package>/adapters/pi/statechart/entry.mjs`. It keeps the upstream scripts unchanged and applies only the Pi execution boundary. Run it from the parent shell. Set `TLA2TOOLS` (or `TLA2TOOLS_JAR`) to the same absolute `tla2tools.jar` the operator declared for `verification_exec`, and `JAVA` to the Java binary. This package bundles no Java, TLC, or mise, and never installs them; when they are missing, report the installation hint and stop.
+
+`verification_exec` with `{"command":"tlc","spec":"<repo>/Spec.tla","config":"<repo>/Spec.cfg","options":["-cleanup","-noGenerateSpecTE","-noGenerateSpecTEBin"]}` remains the restricted TLC entry. It runs one TLC invocation, resolves repository paths, and writes private scratch only, so it cannot draw a chart. Keep chart runs in the parent shell and never report them as `verification_exec` runs.
+
+`--png` uses Pele and resvg, downloaded by the upstream script into the user cache on first use. Those packages and their platform binaries are not part of this npm package. If the renderer cannot be installed or run, keep `chart.mmd`, `stories.md`, and `summary.json`, report that PNG is unavailable, and never claim a PNG exists. `render CHART.mmd` still requires a PNG.
+
+A chart from a run that never executed TLC proves nothing. When TLC is unavailable, say `未做形式化验证，原因是缺少 TLC`, test the real code with generated inputs, and never report fixture or generated tests as a formal pass.
+
+Use read for contents, ls for directories, fffind/ffgrep when available and find/grep otherwise, edit/write for authorized changes, and codemode to batch independent reads. Bash is for execution and Git with an explicit working directory, never a substitute file reader or searcher. Loading this skill grants no permission to commit, push, merge, deploy, delete, or send messages.

adapters/pi/statechart/tlc-tools.mjs

@@ -0,0 +1,43 @@
+// Unlike upstream, Pi only uses an operator-provided or already-installed TLC.
+import { spawnSync } from 'node:child_process';
+import { statSync, realpathSync } from 'node:fs';
+import { tmpdir } from 'node:os';
+import { isAbsolute, join } from 'node:path';
+
+const INSTALL_HINT = 'Install Java 11+ and tla2tools.jar yourself, then set TLA2TOOLS (or TLA2TOOLS_JAR) to the absolute jar path and JAVA to the Java binary. If using mise, install TLC and Java explicitly first. Pi never installs mise, TLC, or Java automatically.';
+const run = (...args) => spawnSync('mise', args, {
+  cwd: tmpdir(),
+  env: { ...process.env, MISE_CEILING_PATHS: tmpdir() },
+  encoding: 'utf8', timeout: 10_000, maxBuffer: 1024 * 1024,
+});
+const existing = (file, name) => {
+  if (!isAbsolute(file)) throw new Error(`${name} must be an absolute path. ${INSTALL_HINT}`);
+  try {
+    if (statSync(file).isFile()) return realpathSync(file);
+  } catch { /* Report a missing/non-file path consistently. */ }
+  throw new Error(`${name} is ${file}, which is not an existing file. ${INSTALL_HINT}`);
+};
+
+export function findTlc() {
+  const declared = [process.env.TLA2TOOLS, process.env.TLA2TOOLS_JAR].filter(v => v?.trim()).map(v => v.trim());
+  if (new Set(declared).size > 1) throw new Error(`Conflicting TLA2TOOLS and TLA2TOOLS_JAR paths. Use the same jar for statechart and verification_exec. ${INSTALL_HINT}`);
+  const java = process.env.JAVA ? existing(process.env.JAVA, 'JAVA') : null;
+  if (declared.length) return { jar: existing(declared[0], 'TLA2TOOLS'), java: java ?? 'java' };
+
+  // `where` and `which` query installed tools; never invoke mise install/exec.
+  // Explicit pins match the snapshot without silently selecting a new release.
+  const { TLC_TOOL, JAVA_TOOL } = installedToolPins;
+  const home = run('where', TLC_TOOL);
+  if (home.error || home.status !== 0 || !home.stdout.trim()) {
+    throw new Error(`Cannot find TLC${home.error?.code === 'ENOENT' ? ' (mise is not installed)' : ' in the installed mise tools'}. ${INSTALL_HINT}`);
+  }
+  const jar = existing(join(home.stdout.trim(), 'tla2tools.jar'), 'mise TLC jar');
+  if (java) return { jar, java };
+  const found = run('which', 'java', '--tool', JAVA_TOOL);
+  if (found.error || found.status !== 0 || !found.stdout.trim()) throw new Error(`Cannot find an installed Java for TLC. ${INSTALL_HINT}`);
+  return { jar, java: existing(found.stdout.trim(), 'mise Java') };
+}
+
+// Importing the upstream resolver defines constants only; it never calls findTlc.
+import * as installedToolPins from '../../../skills/statechart/scripts/tlc-tools.mjs';
+export { cannotRunTlc } from '../../../skills/statechart/scripts/tlc-tools.mjs';

docs/fidelity.md

@@ -1,6 +1,6 @@
 # pi-pstack upstream fidelity
 
-Files: 114  flagged: 4  overall kept (excluding Cursor substitutions): 4439/4722 = 94%
+Files: 114  flagged: 4  overall kept (excluding Cursor substitutions): 4469/4752 = 94%
 
 Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3
 
@@ -105,7 +105,7 @@ Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3
 | skills/reflect/references/judgment-reviewer.md | 44 | 42 | 0 | 0 | 2 | 0 | 100% |  |
 | skills/reflect/references/tooling-reviewer.md | 54 | 52 | 0 | 0 | 2 | 0 | 100% |  |
 | skills/sharpen/SKILL.md | 8 | 8 | 0 | 0 | 0 | 4 | 100% |  |
-| skills/statechart/SKILL.md | 47 | 47 | 0 | 0 | 0 | 23 | 100% |  |
+| skills/statechart/SKILL.md | 77 | 77 | 0 | 0 | 0 | 21 | 100% |  |
 | skills/tdd/SKILL.md | 32 | 32 | 0 | 0 | 0 | 0 | 100% |  |
 | skills/technical-writing/SKILL.md | 136 | 136 | 0 | 0 | 0 | 0 | 100% |  |
 | skills/typescript-best-practices/SKILL.md | 33 | 33 | 0 | 0 | 0 | 1 | 100% |  |