dsh-model-everything

dsh plugin --profile web add dsh-model-everything

设计与代码的建模审查 · 架构可视化（dsh-model-everything）

<p align="center"><a href="README.en-US.md">English</a> · <strong>中文</strong></p>

<p align="center">

<a href="https://github.com/AmethystLuna/dsh-model-everything/actions/workflows/dsh-bundle.yml"><img src="https://github.com/AmethystLuna/dsh-model-everything/actions/workflows/dsh-bundle.yml/badge.svg" alt="CI"></a>

<a href="LICENSE"><img src="https://img.shields.io/badge/license-MIT-blue.svg" alt="License: MIT"></a>

<a href="https://nodejs.org/"><img src="https://img.shields.io/badge/node-%3E%3D20-blue.svg" alt="Node 20+"></a>

<a href="https://afdian.com/a/amethystluna"><img src="https://img.shields.io/badge/%E7%88%B1%E5%8F%91%E7%94%B5-Afdian-946CE6" alt="在爱发电上赞助"></a>

</p>

把设计与代码里的断言抽象成模型，交给引擎跑一遍：结论带出处与哈希，能复算、能比对。让结论来自一次运行，而不是一次通盘推理：把「想清楚」变成「跑一遍」。

同一套模型也能画：架构图从源码直接渲染，父子分组可折叠，结构可按预算量，两版设计可按包含关系比对。

DeepSeek Harness 原生插件。把设计与代码里关于行为的断言变成可运行、可审查、可导出的模型：

• 核验断言：逐条对着源码检查，引用到 file:line。
• 跑模型：状态机、协议、多机协作、数据模型先建成可执行模型，再交给引擎跑。
• 审图：UML 图按模型读、按模型审，并与模型对照。
• 画架构：Mermaid / PlantUML 源码直接出图，嵌套分组、折叠、深浅色；diagram_review 量结构，diagram_diff 比两版。
• 对照重构：重构前后各建一份模型，两份报告摆一起比。
• 留痕：结论固化成带哈希的报告，可复算、可比对、可导出。

专精于中大型、中高复杂度项目的建模审查

这个工具专做一件事：把项目里关于行为、结构、数据的断言建成模型，跑一遍，拿回一条可复算的结论，而不是一段读起来像结论的散文。

它专精的尺度是中大型、中高复杂度的项目：几万行代码、上百个文件、跨模块的协议与状态机。在那个尺度上，一次判定替代的是几十次阅读，技能正文与工具定义那部分固定开销也随之摊开；我们测到的成本比在这一档回落到 0.93×–1.11×。

它交回三样东西：

• 一条可复算的结论：哈希、verdict、出处；
• 一条反例路径：哪几步、哪个事件序列让断言不成立；
• 一份可导出的模型：同一条结论能交给 UPPAAL、TLA+、PRISM、SPIN 复核。

它专精的对象，是人已经抽象好的小模型：状态机、有限词自动机、数据模型与迁移、设计声明、依赖图。模型大到枚举不动时，它报 truncated 并点名未决的检查；减模型（去掉性质不读的变量、合并对称状态），或把那份模型交给 SPIN 的偏序归约、NuSMV 的符号化、CBMC 的有界 SAT，都能接着往下走。

报告卡片

每份报告在终端里照常显示全文，同时在支持渲染的界面里给一张卡片。这不是第二份结论：卡片是同一次计算的另一种排布。

• 先给判定，再给首条问题，最后给下一步；
• diff 把两件事分开写：这次改动新增了什么，以及当前报告本身是什么判定——它们只会在「干净改动落到一份本来就失败的报告上」时不一致；
• 设计审阅分三级：violation 决定判定，signal 是结构事实，fact 是测量；三者不会合并成一个数字；
• 交错扫描读完只说明「已把断言路由给能判定它的工具」，卡片上写着它没有证明任何一条；
• 没有卡片时退回原始文本，不会因为界面不支持而丢掉结论。

卡片不节省任何 token：模型看到的仍是全文。

能力范围

域 · 做什么

事实核验 · 把一份设计/规格/评审意见里的可验证断言列出来，逐条对着代码核验并给出出处。核不了的直接说明

行为验证 · 状态机与协议：结构检查、对抗性探测、预算与时限、before/after 回归。多机组合查死锁，以及永不发生的会合（握手事件）。有限词自动机判语言关系（等价、包含）并给出最短反例词

图 · UML 2.5 各图族的渲染、解析与建模审查（含 render→parse 往返一致性对照），覆盖 Mermaid 与 PlantUML 两种记号

结构 · 组件/包/类/部署图按依赖图审计：孤立节点、悬空引用、环、矩阵与分层违规、缺失的必需边

数据 · 数据模型与迁移：结构、迁移覆盖、拷贝一致性、回滚对称、前后数据回归

并发 / 同步 / 异步 · 挖掘"工作怎么被执行"的断言（线程安全、锁、中断、async/await、事件循环…）并路由到能判定它的工具；它自己不证明

导出 · 已验证模型导出为 UPPAAL / TLA+ / PRISM / SPIN 的输入

报告 · 报告正文渲染、基线比对（report_diff）、哈希规范。每份报告另带一份给界面用的摘要：verdict、首条问题、下一步，正文照旧给模型

架构可视化 · 源码直接画图（Mermaid / PlantUML 的可画子集）、按预算量结构、按包含关系比两版设计。父子分组是一等公民：嵌套框、折叠、深浅色与配色方案，以及右栏白板

架构可视化

画图在这里不是「让报告好看」，而是读设计的入口。三件事分开做，因为它们是三个不同的问题：

你要的 · 工具 · 它回答 · 它不回答

把源码画出来 · diagram_render · 这张图长什么样 · 图里说的系统对不对

这张图是不是太挤 · diagram_review · 每个包多宽、嵌套多深、整图多少节点 · 这些包该不该存在

两版设计差在哪 · diagram_diff · 哪个边界新增/消失/改名/换了父组，哪个组件换了归属 · 这个改动是不是改进

父子分组是一等公民。 Mermaid 的 subgraph 与 PlantUML 的 package 都读成边界，边界可以嵌套，布局按「组内竖排、父组包住子组」来算——因为一个成员飘在包外面的分层图，并没有在表达包含关系。点一个边界就把它折成一个盒子，再点展开；折叠是模型变换，不是绘制模式，所以连线会跟着改指到盒子上。

连线绕开组件，穿过组件的不画。 直连没有障碍时就是一条直线；一旦有盒子挡在中间，改走稀疏网格——候选坐标取每个盒子四边外一点点，构成一张很小的图，再用 A\* 找最短路，并对拐弯计费。这是 Graphviz（visibility graph）、ELK / yFiles（orthogonal router）、mxGraph 共用的做法：不做像素网格，用盒子边界构造 O(盒子数) 的候选线，成本才是可接受的。搜索失败时保留直线，丢一条边比绕远路更糟。

排版先量文字，再定盒子。 标签里的 <br> / <br/> 是硬换行，过长的标签自动折行；盒子尺寸由它实际要画的那几行决定，行高取该行最高的盒子。边标签会沿自己的边找位置，找不到就退到边的一侧——和 Graphviz 把一个标签当虚拟节点、为它留位是同一个思路：文字先量，几何后算。盒子按文字定宽，所以溢出不靠运气。

画不了的行会说清楚。 序列表、类图、甘特图、click/classDef 这类指令，以及 PlantUML 的 actor/note，一律按行号拒绝。悄悄丢掉生命线的时序图看起来是完整的，这比不画更糟。

深浅色跟着页面走。 背景亮度决定用深色板还是浅色板，四套配色可选（default、github、high-contrast、print）；底色画在 SVG 里，所以外层换皮肤也改不了图的对比度。右栏还有一个白板标签页：贴源码就出图，不依赖任何工具结果。

它不证明设计是对的：一张好看的图只是一个可读的模型，判断仍然是 model_verify 与 uml_structure_verify 的事。

典型用法

每个场景都只讲「给什么、看哪个字段、它不管什么」。

重构 harness

1. 重构前抽 BEFORE 模型；数据侧留一份旧 schema。

2. 重构。

3. 抽 AFTER 模型。

4. model_verify 带 beforeModel 与 stateMapping；数据侧用 model_datamodel_verify 的 fieldMapping。

5. report_diff 拿基线报告比对：新增的 error 就是拒绝这次重构的理由。

它比的是两份模型，不是两份代码；也不读 diff、不改代码、不跑测试。

状态机与流程图

1. 图交给 uml_parse，或直接按 schema 写模型。

2. model_verify 跑结构检查与对抗探测：不可达、吸收环、被静默忽略的事件、预算、时限。

3. 把「永远 / 绝不」写进 invariants，拿回最短反例路径。

4. 只看图本身用 uml_review：分支是否穷尽、有没有死端。

5. 每条 error 回到代码核验；改模型用 model_edit，一次调用拿回结构 diff 与发现 diff。

图画对了不等于代码写对了——那一步由抽取负责。

审计一张依赖图

1. 给图，或给 repoPath 让 uml_structure_verify 直接从源码建图。

2. 有规则就给矩阵：layers 加 rules。

3. 读发现：环、孤立节点、悬空端点、越层边、缺失的必需边。解析器报标签漂移时，uml_explain_labels 打印该记号接受的写法。

事实归它，规则不归它：某条边到底存不存在，问这个工具；该不该允许，是 model_design_review。

让设计对自己作出的声明负责

1. 把设计与它声明的规则写成 DesignModelV1。

2. model_design_review 报三类：violations 决定判定，signals 只是信号，facts 是测量。

3. 没声明任何可对照的东西时，对应检查是 skip，不是 pass。

它不按外部标准评判设计，只问：它就自己的说法而言站得住吗。

两台必须互相配合的机器

1. 各自建模，一起给 model_compose_verify。

2. 需要双方同时就绪的会合写进 rendezvous。

3. 读 C1 死锁与 C2 永不触发的会合，各自带逐机理由与最短反例。

单台机器自己的问题回 model_verify；组合里没有速率比，也没有公平性。

并发声明：挖掘并路由

1. model_interleaving_scan 扫文本，按 family 报出绝对断言（线程安全、lock-free、ISR 安全…）。

2. 每条点名能判定它的分析：TSan / Helgrind、CBMC、TLA+、RTOS 感知分析。

3. 本插件不运行那个分析，也不对并发安全作任何证明。

一次干净的扫描不是健康证明——它的含义只是没找到声明。

一次迁移：前后两份模型

1. 前后各一份数据模型。

2. 给 fieldMapping；来源不是自己旧名字的字段用 migrationMappings。

3. model_datamodel_verify 查迁移覆盖、拷贝一致性、回滚对称、前后数据回归。

4. DS2_REQUIRED_FIELD_UNSOURCED 是 warning：它是要你做的决定，不是引擎能替你宣布的失败。

语言包含：两台自动机

1. 把规范与实现各自写成自动机：states、alphabet、transitions、accepting。

2. model_automaton_verify 带 other 与 relation（equivalent / subset / superset）。

3. 关系不成立时拿走最短反例词——一个实现接受、规范拒绝的词，可以直接在两台机器上重放。

只判有限词。liveness、公平性与时序需要 Büchi 或时间自动机，这个族不做。

图的导入与导出：冻结与迭代

1. uml_render 写出 Mermaid / PlantUML 源，uml_parse 读回模型。

2. 图源、模型与那次验证的报告一起提交，作为某个时间点的设计记录。

3. 下次改动重抽、重跑，用 report_diff 与冻结的那份比对。

4. 要交给外部检查器，用 model_export 出 UPPAAL / TLA+ / PRISM / SPIN

…(truncated)