形式化方法可视化实验室

通过交互式可视化理解形式化方法的核心工具与思想：从时序逻辑的状态机到 SMT 约束求解，从归纳证明到混合系统的连续-离散耦合。每个模块均可播放、单步与重置，直观体会安全/活性、反例、迹等价与时钟演化的含义。

TLA+AlloySPIN / Promela CoqZ3 / SMTCSP / CCS Timed AutomataHybrid Automata
模块 01 · TLA+

时序逻辑与状态机

TLA+ 以数学方式描述系统行为：Init 初始条件、Next 次态关系，并用时序公式刻画 安全性（坏事永不发生）与 活性（好事终将发生）。

Next · 循环迁移 禁止 S0 S1 S2 S3 Bad
就绪
安全性 []~Bad 要求永远不进入 Bad 状态；活性 <>S3 要求最终到达 S3。虚线为被安全约束禁止的迁移，运行中永不被采纳。
当前状态S0
安全性 []~Bad✓ 满足
活性 <>S3… 等待
迁移数0
模块 02 · Alloy

关系约束与实例生成

Alloy 以关系代数声明签名与约束，通过 SAT 求解器枚举实例。若约束不可满足则给出 反例，辅助在早期发现设计缺陷。

生成实例…
签名 sig Person { friend: set Person }；约束 all p: Person | some p.friend。无朋友的节点即为反例（红色高亮）。
节点数4
关系边0
约束状态—
反例节点—
模块 03 · SPIN / Promela

模型检测与反例路径

SPIN 对 Promela 模型做穷尽状态空间搜索，验证 LTL 性质。若性质被违反，返回一条 反例路径 作为可执行的反证。

a b c d e f q N0 N1 N2 N3 N4 N5
就绪
LTL 性质 []!q（始终不发生 q）。红色路径 N0 → N1 → N4 即反例：它到达 q 状态，证伪该性质。
状态数6
迁移数7
LTL 属性[]!q
反例位置N0
模块 04 · Coq

归纳证明与 tactic 策略

Coq 基于归纳构造演算，通过 tactic 逐步将目标分解为子目标，直至全部闭合。证明树记录每一步策略的衍生关系。

∀ n, n + 0 = n induction 0 + 0 = 0 S m + 0 = S m simpl 0 = 0 reflexivity ✓ 闭合 simpl S (m + 0) = S m rewrite IH S m = S m reflexivity ✓ 闭合 按“单步”依次应用 tactic …
目标：1
证明 plus_n_O : forall n, n + 0 = n。先 induction n 分裂为基础与归纳步，再用 simpl 化简、rewrite IH 应用归纳假设、reflexivity 闭合。
剩余目标2
已闭合0
tactic 步0
进度0 / 6
模块 05 · Z3 求解器

SAT / SMT 约束求解

Z3 是 SMT 求解器，在实数/整数/布尔理论上判定约束可满足性。可视化展示约束裁出的可行域与求解点的搜索收敛过程。

x y 0 10 10 x+y=10 x=2 x=8 y=3 y=8
搜索中…
约束 x+y≥10, x≥2, y≥3, x≤8, y≤8。求解器在可行域（阴影）中搜索满足赋值，收敛到一个解即返回 sat。
约束数5
变量数2
求解状态搜索中
当前解(0,0)
模块 06 · 进程代数

CSP / CCS · 互模拟与迹

进程代数用标号迁移系统刻画并发行为。迹等价比较可观察动作序列，互模拟更强：要求每步迁移后仍能继续匹配。

P = a.(b.0 + c.0) Q = a.b.0 + a.c.0 a b c a a b c P0 P1 0 0 Q0 Q1 Q2 0 0
迹：—
两进程的迹集合相同 {a·b, a·c}，故 迹等价；但 P 在 a 之后可同时选择 b 或 c，而 Q 已被 a 提前锁定分支，故 不互模拟。
进程P / Q
迹匹配✓ 等价
互模拟✗ 不互模拟
当前迹—
模块 07 · 实时系统

时间自动机与 UPPAAL

时间自动机在迁移上添加 时钟约束（guard）与 不变式（invariant），刻画实时行为。UPPAAL 借此验证带时间的可达性与死锁性质。

x ≥ 3 / x:=0 x ≥ 2 / x:=0 L0 x≤5 L1 x≤4 时钟 x 0.00
L0 · x=0.00
L0 不变式 x≤5、迁移 guard x≥3 并重置 x:=0；L1 同理。时钟连续增长，guard 满足时发生离散迁移并复位时钟。
时钟 x0.00
当前位置L0
不变式x≤5
迁移数0
模块 08 · 混合系统

连续 / 离散混合自动机

混合自动机在离散迁移之外加入 连续流（ODE），刻画物理量演化与离散跳变的耦合。弹跳球是经典示例：自由下落与触地反弹。

h t 连续流：ṁ = v, v̇ = -g
静止
连续阶段遵循 ḣ=v, v̇=-g（抛物线轨迹）；触地 h=0 时触发离散跳变 v := -e·v（e 为恢复系数），能量逐次衰减。
高度 h0
速度 v0
弹跳次数0
当前模式静止