From cfd2c859172bf4ae6c0d305f6088ea252a8a16ee Mon Sep 17 00:00:00 2001 From: liuyuchen <152110621+jiangkoumo@users.noreply.github.com> Date: Mon, 26 Oct 2026 14:40:14 +0800 Subject: [PATCH] fix(statechart): route generated skill commands through Pi entry --- adapters/pi/statechart/skill-replacements.json | 17 +++++++++++++++++ adapters/pi/statechart/skill-tail.md | 4 ++-- docs/fidelity-allow.txt | 5 +++++ docs/fidelity.md | 7 +++++-- docs/port-map.json | 5 +++-- docs/skill-audit.md | 2 +- docs/validation-statechart-sync.md | 6 +++++- scripts/generate-pi-resources.mjs | 18 ++++++++++++++++-- scripts/statechart-adapter.test.mjs | 14 ++++++++++++++ skills/statechart/SKILL.md | 14 +++++++++++--- 10 files changed, 79 insertions(+), 13 deletions(-) create mode 100644 adapters/pi/statechart/skill-replacements.json diff --git a/adapters/pi/statechart/skill-replacements.json b/adapters/pi/statechart/skill-replacements.json new file mode 100644 index 0000000..4cc3553 --- /dev/null +++ b/adapters/pi/statechart/skill-replacements.json @@ -0,0 +1,17 @@ +[ + { + "from": "/scripts/statechart.mjs", + "to": "/adapters/pi/statechart/entry.mjs", + "reason": "Route help and all command examples through the Pi boundary, which never installs TLC." + }, + { + "from": "The first run installs TLC and Java with mise, which downloads about 305 MB and needs the network.", + "to": "Set TLA2TOOLS (or TLA2TOOLS_JAR) and JAVA to the already-installed TLC jar and Java binary. Pi does not automatically install mise, TLC, or Java.", + "reason": "The upstream automatic mise installation policy does not apply to Pi." + }, + { + "from": "## Pick the direction", + "to": "Run all chart commands through the Pi entry:\n\n```sh\nnode /adapters/pi/statechart/entry.mjs from-spec SPEC.tla\nnode /adapters/pi/statechart/entry.mjs from-chart CHART.mmd\nnode /adapters/pi/statechart/entry.mjs render CHART.mmd\n```\n\n## Pick the direction", + "reason": "Give executable Pi examples for each subcommand while retaining upstream descriptions of their behavior." + } +] diff --git a/adapters/pi/statechart/skill-tail.md b/adapters/pi/statechart/skill-tail.md index b221abe..dc93653 100644 --- a/adapters/pi/statechart/skill-tail.md +++ b/adapters/pi/statechart/skill-tail.md @@ -1,8 +1,8 @@ ## Pi execution and authority -Adapted from Lauren Tan's pstack, MIT. The upstream body above is byte-preserved from cursor/plugins@076f4b2f. +Adapted from Lauren Tan's pstack, MIT. The body above comes from cursor/plugins@076f4b2f, with Pi entry and installation instructions replaced by the generation adapter. -The chart entry is `node /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. +The chart entry is `node /adapters/pi/statechart/entry.mjs`. In help output, `node statechart.mjs` always means `node /adapters/pi/statechart/entry.mjs`, including Usage, render, from-spec, and from-chart examples. The help’s automatic TLC/Java installation instructions describe upstream behavior; follow the Pi installation policy in this skill. 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":"/Spec.tla","config":"/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. diff --git a/docs/fidelity-allow.txt b/docs/fidelity-allow.txt index 3da98c1..fe4f577 100644 --- a/docs/fidelity-allow.txt +++ b/docs/fidelity-allow.txt @@ -10,3 +10,8 @@ skills/setup-pstack/SKILL.md # Pi paths/tools and unshipped Cursor guide-page links. skills/poteto-help/SKILL.md skills/poteto-mode/playbooks/orchestrate.md + +# Statechart: replace raw CLI commands and automatic mise/TLC/Java installation +# with Pi entry and preinstalled tools; see adapters/pi/statechart/skill-replacements.json. +# All engineering guidance and the upstream snapshot/scripts remain unchanged. +skills/statechart/SKILL.md diff --git a/docs/fidelity.md b/docs/fidelity.md index 01d4795..7e6f5e5 100644 --- a/docs/fidelity.md +++ b/docs/fidelity.md @@ -1,6 +1,6 @@ # pi-pstack upstream fidelity -Files: 114 flagged: 4 overall kept (excluding Cursor substitutions): 4469/4752 = 94% +Files: 114 flagged: 4 overall kept (excluding Cursor substitutions): 4467/4752 = 94% Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3 @@ -48,6 +48,7 @@ Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3 | skills/poteto-mode/playbooks/eval.md | 37 | 35 | 0 | 1 | 1 | 27 | 97% | | | skills/create-verification-skill/SKILL.md | 73 | 71 | 2 | 0 | 0 | 34 | 97% | | | skills/how/references/explainer-prompt.md | 39 | 38 | 0 | 1 | 0 | 1 | 97% | | +| skills/statechart/SKILL.md | 77 | 75 | 1 | 1 | 0 | 27 | 97% | | | skills/poteto-mode/references/bugbot-triage.md | 94 | 92 | 1 | 1 | 0 | 5 | 98% | | | skills/reflect/references/synthesizer.md | 49 | 47 | 0 | 1 | 1 | 1 | 98% | | | skills/why/references/synthesizer-prompt.md | 95 | 93 | 1 | 1 | 0 | 8 | 98% | | @@ -105,7 +106,6 @@ 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 | 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% | | @@ -342,6 +342,9 @@ Thresholds: kept >= 0.85, reworded >= 0.55; flag if kept < 70% or lost > 3 ### skills/how/references/explainer-prompt.md - Use Read, Grep, and Glob as needed. +### skills/statechart/SKILL.md +- The first run installs TLC and Java with mise, which downloads about 305 MB and needs the network. + ### skills/poteto-mode/references/bugbot-triage.md - Reply with a short reason and resolve the thread. diff --git a/docs/port-map.json b/docs/port-map.json index 7276e9c..30d2cc7 100644 --- a/docs/port-map.json +++ b/docs/port-map.json @@ -1572,7 +1572,7 @@ "disposition": "ported", "phase": "P5", "destination": "skills/statechart/SKILL.md", - "reason": "已同步到 076f4b2f；上游正文原样，Pi 执行边界追加在 skill-tail.md；见 docs/validation-statechart-sync.md", + "reason": "已同步到 076f4b2f；正文入口与安装说明由 skill-replacements.json 最小替换，Pi 执行边界追加在 skill-tail.md；见 docs/validation-statechart-sync.md", "audit": { "sourceRead": true, "relativeLinks": [], @@ -1581,7 +1581,8 @@ "adaptation": { "strategy": "inherit-body", "override": null, - "append": "adapters/pi/statechart/skill-tail.md" + "append": "adapters/pi/statechart/skill-tail.md", + "replacements": "adapters/pi/statechart/skill-replacements.json" }, "evidence": "validation-statechart-sync.md", "dependencies": "from-template" diff --git a/docs/skill-audit.md b/docs/skill-audit.md index 5d47c10..f2bb314 100644 --- a/docs/skill-audit.md +++ b/docs/skill-audit.md @@ -134,4 +134,4 @@ ported 的技能与流程由技能清单导出。P2 的 setup-pstack 已由扩展命令替代，证据见 validation-p2.md；其余 substitute 条目仍需对应阶段实现及验收，deferred 已归零。审计归属不等于全量复刻。 | 技能 create-formal-verification-skill | P5 | 已适配；正文保持上游，追加 Pi 宿主执行与产物落盘约定；见 docs/validation-stage-b-batch-two.md | | 技能 maintain-formal-verification-skill | P5 | 已适配；正文保持上游，追加 Pi 宿主执行与产物落盘约定；见 docs/validation-stage-b-batch-two.md | -| 技能 statechart | P5 | 已同步到 076f4b2f；上游正文原样，Pi 执行边界追加在 skill-tail.md；见 docs/validation-statechart-sync.md | +| 技能 statechart | P5 | 已同步到 076f4b2f；正文入口与安装说明由 skill-replacements.json 最小替换，Pi 执行边界追加在 skill-tail.md；见 docs/validation-statechart-sync.md | diff --git a/docs/validation-statechart-sync.md b/docs/validation-statechart-sync.md index db53671..cb3e0e4 100644 --- a/docs/validation-statechart-sync.md +++ b/docs/validation-statechart-sync.md @@ -15,7 +15,11 @@ - 受限 `verification_exec` 的 TLC 入口和探测未改动。 - PNG：渲染器不可用时保留 `.mmd` 并提示；显式 `render` 子命令仍要求 PNG。部分渲染失败不再把已有的模型检查结果报成失败。 -以上差异记录在 `docs/port-map.json` 的 `runtimeAdapters`，原因写在同一条目。 +以上运行时差异记录在 `docs/port-map.json` 的 `runtimeAdapters`，原因写在同一条目。 + +SKILL.md 正文中的原始脚本入口、首次自动安装 TLC/Java 的说明由 `adapters/pi/statechart/skill-replacements.json` 最小替换；正文前部列出帮助、from-spec、from-chart 和 render 的 Pi 入口。生成器要求每项替换都有原文匹配和原因，缺失匹配时停止，防止上游更新后静默丢失适配。快照与脚本不变。保真白名单仅记录宿主差异，不豁免整体 94% 门禁；当前保真结果为 4467/4752 = 94.0025%（此前 4469/4752 = 94.0446%）。 + +help 保留上游输出；技能尾部明确规定其中 `node statechart.mjs` 均指 `node /adapters/pi/statechart/entry.mjs`，自动安装说明也以 Pi 规则为准。新增生成文档回归在修复前失败，修复后通过。 ## 检查 diff --git a/scripts/generate-pi-resources.mjs b/scripts/generate-pi-resources.mjs index b7e90ff..8ee3be2 100644 --- a/scripts/generate-pi-resources.mjs +++ b/scripts/generate-pi-resources.mjs @@ -115,8 +115,11 @@ for (const entry of [...map.entries, ...prepared, ...native]) { assert(!rendered.has(entry.destination), 'Duplicate destination: ' + entry.destination); assert(Array.isArray(entry.dependencies) || entry.dependencies === 'from-template', 'Missing dependency list: ' + entry.source); assert(entry.adaptation && ['override', 'inherit-body', 'verbatim'].includes(entry.adaptation.strategy), 'Unknown adaptation strategy: ' + entry.source); - const adaptationKeys = entry.adaptation.append === undefined ? ['override', 'strategy'] : ['append', 'override', 'strategy']; + const adaptationKeys = ['override', 'strategy', ...(entry.adaptation.append === undefined ? [] : ['append']), ...(entry.adaptation.replacements === undefined ? [] : ['replacements'])].sort(); assert.deepEqual(Object.keys(entry.adaptation).sort(), adaptationKeys, 'Unknown adaptation field: ' + entry.source); + if (entry.adaptation.replacements !== undefined) { + assert.equal(entry.adaptation.strategy, 'inherit-body', 'Only inherited bodies can replace host instructions: ' + entry.source); + } if (entry.adaptation.append !== undefined) { assert.equal(entry.adaptation.strategy, 'inherit-body', 'Only inherited bodies can append Pi guidance: ' + entry.source); await pathInPackage(entry.adaptation.append, 'adapters/pi/'); @@ -139,7 +142,18 @@ for (const entry of [...map.entries, ...prepared, ...native]) { output = await readFile(await pathInPackage(template, 'adapters/pi/overrides/'), 'utf8'); } else { assert.equal(entry.adaptation.override, null, 'Inherited entry has an override: ' + entry.source); - const { fields, body } = frontmatter(originals.get(entry.source), ['name', 'description', 'disable-model-invocation'], entry.source); + const { fields, body: originalBody } = frontmatter(originals.get(entry.source), ['name', 'description', 'disable-model-invocation'], entry.source); + let body = originalBody; + if (entry.adaptation.replacements !== undefined) { + assert.equal(entry.source, 'pstack/skills/statechart/SKILL.md', 'Body replacements are limited to statechart host instructions'); + await pathInPackage(entry.adaptation.replacements, 'adapters/pi/'); + const replacements = await json(entry.adaptation.replacements); + for (const replacement of replacements) { + assert(replacement.from && replacement.to && replacement.reason, 'Body replacement requires text and a reason'); + assert(body.includes(replacement.from), 'Stale statechart replacement: ' + replacement.from); + body = body.replaceAll(replacement.from, replacement.to); + } + } assert(fields.name && fields.description, 'Missing skill metadata: ' + entry.source); // P2.5 supports explicit-only skills. A changed invocation policy needs an // explicit reviewed override, rather than silently forcing the old value. diff --git a/scripts/statechart-adapter.test.mjs b/scripts/statechart-adapter.test.mjs index 791485f..fc14f13 100644 --- a/scripts/statechart-adapter.test.mjs +++ b/scripts/statechart-adapter.test.mjs @@ -51,6 +51,20 @@ test('Pi adapter uses one absolute configured jar and refuses conflicts or relat } finally { await rm(dir, { recursive: true, force: true }); } }); +test('generated statechart guidance uses the Pi entry before any command and never promises TLC installation', async () => { + const skill = await readFile(resolve(root, 'skills/statechart/SKILL.md'), 'utf8'); + const body = skill.split('## Pi execution and authority')[0]; + assert.doesNotMatch(skill, /scripts\/statechart\.mjs/); + const claims = skill.replace('Pi does not automatically install mise, TLC, or Java.', ''); + assert.doesNotMatch(claims, /first run installs|automatically installs? (?:TLC|Java|mise)|will install (?:TLC|Java|mise)|mise install|downloads about 305 MB/i); + for (const command of ['--help', 'from-spec', 'from-chart', 'render CHART.mmd']) { + assert(body.includes('node /adapters/pi/statechart/entry.mjs ' + command), command); + } + assert.match(body, /TLA2TOOLS.*TLA2TOOLS_JAR.*JAVA/); + assert.match(body, /Pi does not automatically install mise, TLC, or Java/); + assert.match(skill, /In help output, `node statechart\.mjs` always means `node \/adapters\/pi\/statechart\/entry\.mjs`/); +}); + test('adapter keeps the pinned upstream scripts byte-identical', async () => { const map = JSON.parse(await readFile(resolve(root, 'docs/port-map.json'), 'utf8')); for (const resource of map.preparedResources.filter(entry => entry.adaptation.strategy === 'verbatim')) { diff --git a/skills/statechart/SKILL.md b/skills/statechart/SKILL.md index 17d8945..fe00223 100644 --- a/skills/statechart/SKILL.md +++ b/skills/statechart/SKILL.md @@ -9,7 +9,15 @@ license: MIT The chart shows how a system moves between states, in the words of the person who reads it. The scripts call that person the reader, as in `readerActions` and reader steps. The reader decides whether the behavior is right. The reader can be a PM who reads a product flow, an engineer who reads a protocol or a service, or a reviewer who reads a design. Label each state with what the reader can observe or cares about, such as "Paying" in an app or "Lease held, write pending" in a lock service. Label each step with the event that moves the system, such as "tap Pay" in an app, "the request reads the count" in a service, or "the lease expires" in a lock service. Keep variable and action names out of labels. -Run `node /scripts/statechart.mjs --help` for the commands and for how to read a chart. Work in a scratch folder outside the repo. The command writes its files next to its input. The first run installs TLC and Java with mise, which downloads about 305 MB and needs the network. The help's TLC section tells how to use a TLC and Java that you have. +Run `node /adapters/pi/statechart/entry.mjs --help` for the commands and for how to read a chart. Work in a scratch folder outside the repo. The command writes its files next to its input. Set TLA2TOOLS (or TLA2TOOLS_JAR) and JAVA to the already-installed TLC jar and Java binary. Pi does not automatically install mise, TLC, or Java. The help's TLC section tells how to use a TLC and Java that you have. + +Run all chart commands through the Pi entry: + +```sh +node /adapters/pi/statechart/entry.mjs from-spec SPEC.tla +node /adapters/pi/statechart/entry.mjs from-chart CHART.mmd +node /adapters/pi/statechart/entry.mjs render CHART.mmd +``` ## Pick the direction @@ -38,9 +46,9 @@ Give the PNG and the Mermaid source of each chart to the person who must decide. ## Pi execution and authority -Adapted from Lauren Tan's pstack, MIT. The upstream body above is byte-preserved from cursor/plugins@076f4b2f. +Adapted from Lauren Tan's pstack, MIT. The body above comes from cursor/plugins@076f4b2f, with Pi entry and installation instructions replaced by the generation adapter. -The chart entry is `node /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. +The chart entry is `node /adapters/pi/statechart/entry.mjs`. In help output, `node statechart.mjs` always means `node /adapters/pi/statechart/entry.mjs`, including Usage, render, from-spec, and from-chart examples. The help’s automatic TLC/Java installation instructions describe upstream behavior; follow the Pi installation policy in this skill. 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":"/Spec.tla","config":"/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.