12. 术语表

术语	白话
规格 spec	描述系统怎么一步步变化的小模型，不是上线代码
状态 state	某一刻所有变量的值
动作 action	带条件的一步变化，用 x’ 表示下一刻
行为 behavior	一串状态，从起点开始，可以无限长
TLC	TLA+ 的模型检查器，把所有可能顺序走一遍
不变式 invariant	每个状态都必须成立的规则（安全性）
活性 liveness	终究要发生的事，看整条路才能判断
反例 / 轨迹 trace	TLC 打印的、导致违反的那条路
Stuttering 原地踏步	什么都不变的一步；无限重复就是“停住了”
死锁 deadlock	到了一个没有任何动作可做的状态
WF 弱公平	一直能做的动作终究会做
SF 强公平	时不时能做的动作终究会做
SYMMETRY 对称	把只是换了名字的状态当成同一个
VIEW 视图	只按某个表达式判断状态是否相同