logic - => 和 <=> 之间的区别

Question

我正在从 this great "Learn TLA+" page 学习 TLA+ .

我无法理解 => 之间的实际差异和 <=> .我从“真值表”的角度理解它，但我无法真正掌握它。

能否提供一个实用的 TLA+ 示例来强调这两者之间的区别？

有关的:

https://math.stackexchange.com/questions/68293/what-is-the-difference-between-only-if-and-iff

Answer 1

假设我们有一个有界队列 q最大尺寸 MAX , reader从队列中弹出消息的进程，一个 writer将消息添加到队列的进程，以及 queue_maxed_flag这是真的还是假的。这里有四个可能的不变量:

(len(q) = MAX) => queue_maxed_flag意味着(除了其他可能的事情，取决于规范)如果作者在 q 时添加消息有 MAX-1消息它也必须集 queue_maxed_flag ，否则违反不变量。但是，如果读取器从已达到最大值的队列中弹出，则不需要 未设置 queue_maxed_flag .

queue_maxed_flag => (len(q) = MAX)意味着(除了等)如果阅读器在 q 时弹出消息有 MAX消息它也必须未设置 queue_maxed_flag .但是，如果作者在 q 时添加了一条消息有 MAX-1消息，它不需要集 queue_maxed_flag .

(len(q) = MAX) <=> queue_maxed_flag和 queue_maxed_flag <=> (len(q) = MAX)意思是一样的:前两个不变量都成立。如果写入器将最后一条消息写入队列，则必须设置该标志，如果读取器从已满队列中读取，则必须取消设置该标志。

那么为什么 A <=> B而不是 A = B ? A <=> B更严格，因为它期望 A 和 B 都是 bool 值。 TLC 评估 5 = 6如 FALSE ，但它会在 5 <=> 6 上引发错误.