dsh-model-everything

设计与代码的建模审查 · 架构可视化（dsh-model-everything） English · 中文 把设计与代码里的断言抽象成模型，交给引擎跑一遍：结论带出处与哈希，能复算、能比对。让结论来自一次运行，而不是一次通盘推理：把「想清楚」变成「跑一遍」。同一套模型也能 画 ：架构图从源码直接渲染，父子分组可折叠，结构可按预算量，两版设计可按包含关系比对。DeepSeek Harness 原生插件。把设计与代码里 关于行为的断言 变成可运行、可审查、可导出的模型： - 核验断言 ：逐条对着源码检查，引用到 file:line 。

- 跑模型 ：状态机、协议、多机协作、数据模型先建成可执行模型，再交给引擎跑。- 审图 ：UML 图按模型读、按模型审，并与模型对照。- 画架构 ：Mermaid / PlantUML 源码直接出图，嵌套分组、折叠、深浅色； diagram review 量结构， diagram diff 比两版。- 对照重构 ：重构前后各建一份模型，两份报告摆一起比。- 留痕 ：结论固化成带哈希的报告，可复算、可比对、可导出。专精于中大型、中高复杂度项目的建模审查 这个工具专做一件事：把项目里关于行为、结构、数据的断言建成模型，跑一遍，拿回一条可复算的结论，而不是一段读起来像结论的散文。

它专精的尺度是中大型、中高复杂度的项目 ：几万行代码、上百个文件、跨模块的协议与状态机。在那个尺度上，一次判定替代的是几十次阅读，技能正文与工具定义那部分固定开销也随之摊开；我们测到的成本比在这一档回落到 0.93×–1.11×。它交回三样东西： - 一条 可复算 的结论：哈希、 verdict 、出处； - 一条 反例路径 ：哪几步、哪个事件序列让断言不成立； - 一份 可导出的模型 ：同一条结论能交给 UPPAAL、TLA+、PRISM、SPIN 复核。它专精的对象，是人已经抽象好的小模型 ：状态机、有限词自动机、数据模型与迁移、设计声明、依赖图。

模型大到枚举不动时，它报 truncated 并点名未决的检查；减模型（去掉性质不读的变量、合并对称状态