8. 公平：WF 和 SF

“公平”（fairness）是你对运行环境的承诺：调度器不会永远冷落某个动作。没有公平，系统可以随时永远停住，活性几乎都证不出来。

写法	名字	白话
WF_vars(A)	弱公平	如果 A 从某一刻起一直能做，它终究会被做
SF_vars(A)	强公平	如果 A 时不时能做（无数次出现机会，哪怕中间断开），它终究会被做

例子：失败就自动重试。Succeed 只在 pending 时能做，回到 idle 时又不能做，它的机会是“断断续续”的。

---- MODULE Retry ----
\* 请求失败就自动重试。我们希望“最终一定成功”。
VARIABLE status

Init == status = "idle"
Send    == status = "idle"    /\ status' = "pending"
Fail    == status = "pending" /\ status' = "idle"
Succeed == status = "pending" /\ status' = "done"

Next == Send \/ Fail \/ Succeed

\* 弱公平：一直能做的事，终究要做
SpecWF == Init /\ [][Next]_status /\ WF_status(Next)

\* 再加强公平：反复有机会成功，终究会成功一次
SpecSF == SpecWF /\ SF_status(Succeed)

EventuallyDone == <>(status = "done")
====

RetryWF.cfg

SPECIFICATION SpecWF
PROPERTY EventuallyDone
CHECK_DEADLOCK FALSE

# RetrySF.cfg（只有第一行不同）
SPECIFICATION SpecSF
PROPERTY EventuallyDone
CHECK_DEADLOCK FALSE

stateDiagram-v2
  [*] --> idle
  idle --> pending: Send
  pending --> idle: Fail(自动重试)
  pending --> done: Succeed

只有弱公平：

java -cp tla2tools.jar tlc2.TLC -config RetryWF.cfg Retry.tla

Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
status = "idle"

State 2: <Send line 6, col 12 to line 6, col 52 of module Retry>
status = "pending"

Back to state 1: <Fail line 7, col 12 to line 7, col 49 of module Retry>

“Back to state 1” 表示一个循环：idle → pending → idle → pending……永远在转。这条路满足弱公平，因为系统一直在走 Next 里的步骤（Send、Fail），没有停住；Succeed 也不是“一直能做”（每次回到 idle 就不能做了），弱公平管不到它。

加上强公平 SF_status(Succeed)：

java -cp tla2tools.jar tlc2.TLC -config RetrySF.cfg Retry.tla

Model checking completed. No error has been found.
4 states generated, 3 distinct states found, 0 states left on queue.

强公平说：Succeed 有无数次机会，所以它终究会发生一次。对应到前端：只有当你真的相信“网络不会每次都恰好失败”时，才可以写 SF。这是一个假设，要写进文档，而不是 TLC 帮你证明的事实。

练习

练习 8.1：在 Retry 里只写 WF_status(Succeed)，能通过吗？

答案：不能。Succeed 在循环里时有时无，不是“一直能做”，弱公平对它没有约束。（按定义推出，未单独运行。）

练习 8.2：现实中怎样不靠强公平也能保证结束？

答案：给重试设上限，比如最多 3 次，失败到上限就进入 error 终点。这样“最终会结束（成功或放弃）”只靠弱公平就够了。