=> 和 <=> 之间的区别
Difference between => and <=>
我正在从 this great "Learn TLA+" page 学习 TLA+。
我无法理解 => 和 <=> 之间的 实用 区别。我以 "truth table" 的形式得到它，但我无法真正 掌握 它。
能否提供一个实用的 TLA+ 示例来突出显示这两者之间的区别？
相关：
=> ("if") 是一个蕴涵。这是一个例子：
如果门打开，则发出警报。
请注意，除了开门之外的其他因素（例如 window开场).
这是事实 table。假设您正在为客户编写报警系统。 x代表开门，y报警。
x | y | x => y | Explanation
0 | 0 | 1 | The door doesn't open, the alarm doesn't sound (You don't want the alarm to go off for nothing)
0 | 1 | 1 | The door doesn't open, but the alarm still sounds (e.g. because a window was opened)
1 | 0 | 0 | The door opens, but the alarm doesn't sound (That is not how you want to protect your house)
1 | 1 | 1 | The door opens and the alarm sounds (What else would you have an alarm for)
让我们转到方程式（<=> 或 "only if"）。仅当两个选项的值相同时才会出现这种情况。此示例保留警报但将其更改为仅当门打开时才发出警报。
注意：这次是开门window不应该触发警报，只有门应该。
x | y | x => y | Explanation
0 | 0 | 1 | The door doesn't open, the alarm doesn't sound
0 | 1 | 0 | The door doesn't open, the alarm sounds (That's a false positive, that window opening is not what your alarm should cover)
1 | 0 | 0 | The door opens, but the alarm doesn't sound (That is not how you want to protect your house)
1 | 1 | 1 | The door opens and the alarm sounds (What else would you have an alarm for)
这在规范中经常被混淆和写错（如果你知道的话，它也很方便地作为一种法律辩护）。
THEOREM TRUE = \A x: (x \in {1, 2}) => (x \in {1, 2, 3})
对比
THEOREM FALSE = \A x: (x \in {1, 2}) <=> (x \in {1, 2, 3})
不成立，因为\E x: (x \in {1, 2, 3}) /\ ~ (x \in {1, 2})（即x = 3）。
标识符x可以表示系统所在的房间。
表达式 A <=> B 的值是为 A \in BOOLEAN /\ B \in BOOLEAN 定义的。
对于 A 和 B 的非布尔值，TLA+ 未指定运算符 <=> 的含义。
适度解释布尔运算符，A <=> B对于非布尔值A、B可能是非布尔值。
根据自由解释，A <=> B 是布尔值，尽管对于非布尔值 A、B.
未指定该值
第 296--297 页的第 16.1.3 节 "Interpretations of Boolean Operators" 和 [1] 第 9--11 页（特别是第 9 页）的第 1.1 节 "Propositional Logic" 与什么最相关运算符 <=> 和 => 的意思是
[1] 莱斯利·兰波特，"Specifying systems"，艾迪生-韦斯利，2002
假设我们有一个最大大小为 MAX 的有界队列 q，一个从队列中弹出消息的 reader 进程，一个向其中添加消息的 writer 进程队列，以及 queue_maxed_flag 是真还是假。这里有四个可能的不变量：
(len(q) = MAX) => queue_maxed_flag 意味着（除了其他可能的事情，取决于规范）如果作者在 q 有 MAX-1 条消息时添加一条消息 还必须 设置 queue_maxed_flag，否则不变量被违反。但是，如果 reader 从最大队列中弹出，则不需要 unset queue_maxed_flag.queue_maxed_flag => (len(q) = MAX) 意味着（除了等等）如果 reader 在 q 有 MAX 条消息时弹出一条消息 它也必须 取消设置 queue_maxed_flag。但是，如果作者在 q 有 MAX-1 条消息时添加一条消息，则不需要 设置 queue_maxed_flag.(len(q) = MAX) <=> queue_maxed_flag 和 queue_maxed_flag <=> (len(q) = MAX) 意思相同：前两个不变量都成立。如果写入器将最后一条消息写入队列，则必须设置标志，如果 reader 从已满队列读取，则必须取消设置标志。
那么为什么是 A <=> B 而不是 A = B？ A <=> B 更严格，因为它期望 A 和 B 都是布尔值。 TLC 将 5 = 6 计算为 FALSE，但会在 5 <=> 6.
上引发错误
我正在从 this great "Learn TLA+" page 学习 TLA+。
我无法理解 => 和 <=> 之间的 实用 区别。我以 "truth table" 的形式得到它，但我无法真正 掌握 它。
能否提供一个实用的 TLA+ 示例来突出显示这两者之间的区别？
相关：
=> ("if") 是一个蕴涵。这是一个例子：
如果门打开，则发出警报。
请注意，除了开门之外的其他因素（例如 window开场).
这是事实 table。假设您正在为客户编写报警系统。 x代表开门，y报警。
x | y | x => y | Explanation
0 | 0 | 1 | The door doesn't open, the alarm doesn't sound (You don't want the alarm to go off for nothing)
0 | 1 | 1 | The door doesn't open, but the alarm still sounds (e.g. because a window was opened)
1 | 0 | 0 | The door opens, but the alarm doesn't sound (That is not how you want to protect your house)
1 | 1 | 1 | The door opens and the alarm sounds (What else would you have an alarm for)
让我们转到方程式（<=> 或 "only if"）。仅当两个选项的值相同时才会出现这种情况。此示例保留警报但将其更改为仅当门打开时才发出警报。
注意：这次是开门window不应该触发警报，只有门应该。
x | y | x => y | Explanation
0 | 0 | 1 | The door doesn't open, the alarm doesn't sound
0 | 1 | 0 | The door doesn't open, the alarm sounds (That's a false positive, that window opening is not what your alarm should cover)
1 | 0 | 0 | The door opens, but the alarm doesn't sound (That is not how you want to protect your house)
1 | 1 | 1 | The door opens and the alarm sounds (What else would you have an alarm for)
这在规范中经常被混淆和写错（如果你知道的话，它也很方便地作为一种法律辩护）。
THEOREM TRUE = \A x: (x \in {1, 2}) => (x \in {1, 2, 3})
对比
THEOREM FALSE = \A x: (x \in {1, 2}) <=> (x \in {1, 2, 3})
不成立，因为\E x: (x \in {1, 2, 3}) /\ ~ (x \in {1, 2})（即x = 3）。
标识符x可以表示系统所在的房间。
表达式 A <=> B 的值是为 A \in BOOLEAN /\ B \in BOOLEAN 定义的。
对于 A 和 B 的非布尔值，TLA+ 未指定运算符 <=> 的含义。
适度解释布尔运算符，A <=> B对于非布尔值A、B可能是非布尔值。
根据自由解释，A <=> B 是布尔值，尽管对于非布尔值 A、B.
第 296--297 页的第 16.1.3 节 "Interpretations of Boolean Operators" 和 [1] 第 9--11 页（特别是第 9 页）的第 1.1 节 "Propositional Logic" 与什么最相关运算符 <=> 和 => 的意思是
[1] 莱斯利·兰波特，"Specifying systems"，艾迪生-韦斯利，2002
假设我们有一个最大大小为 MAX 的有界队列 q，一个从队列中弹出消息的 reader 进程，一个向其中添加消息的 writer 进程队列，以及 queue_maxed_flag 是真还是假。这里有四个可能的不变量：
(len(q) = MAX) => queue_maxed_flag意味着（除了其他可能的事情，取决于规范）如果作者在q有MAX-1条消息时添加一条消息 还必须 设置queue_maxed_flag，否则不变量被违反。但是，如果 reader 从最大队列中弹出，则不需要 unsetqueue_maxed_flag.queue_maxed_flag => (len(q) = MAX)意味着（除了等等）如果 reader 在q有MAX条消息时弹出一条消息 它也必须 取消设置queue_maxed_flag。但是，如果作者在q有MAX-1条消息时添加一条消息，则不需要 设置queue_maxed_flag.(len(q) = MAX) <=> queue_maxed_flag和queue_maxed_flag <=> (len(q) = MAX)意思相同：前两个不变量都成立。如果写入器将最后一条消息写入队列，则必须设置标志，如果 reader 从已满队列读取，则必须取消设置标志。
那么为什么是 A <=> B 而不是 A = B？ A <=> B 更严格，因为它期望 A 和 B 都是布尔值。 TLC 将 5 = 6 计算为 FALSE，但会在 5 <=> 6.