Ramadge–Wonham：vibe-linter 的数学归宿

Parent: vibe-linter · Reference: ramadge-wonham-supervisory-control

RW 是 vibe-linter 精确的数学归宿（比 Petri 网更贴切）。"监督者只能禁用可控事件，永远无法强迫被控对象"——这正是 gatekeeper-not-driver 的数学定义。

映射关系：

• 测试结果就是 Σ_u——你只能允许测试运行，却控制不了它是红是绿。所以"测试必须通过"不是一个可控的 spec；可控的版本是"提交在观测到绿之前保持禁用。" RW 把这条"闸门而非命令"的直觉提升成了一条定理。
• supC(K) = 综合（synthesis）： 你只声明想要的性质，linter 计算出最小的锁集——即禁用最少一组提交/动作所需的、限制性最小的集合。
• 部分观测 = 观测面： 监督者只能看到投影（工具调用，而非内部推理）；任何依赖"agent 内心想了什么"的 spec 都无法执行。杠杆在于：Σ_o 是可以花代价买大的——强迫所有动作都经由工具调用（系统调用化，syscall-ization）就能扩大观测面。