3

我正在从这个很棒的“学习 TLA+”页面学习 TLA+。

我无法得到和之间的实际区别。我从“真值表”的角度得到它，但我无法真正掌握它。=><=>

有人可以提供一个实用的 TLA+ 示例来突出这两者之间的区别吗？

有关的：

4

3 回答 3

4

想象一下，我们有一个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 都是布尔值。TLC 评估5 = 6为FALSE，但在 上引发错误5 <=> 6。

于 2017-11-13T18:16:20.287 回答
4

=>("if") 是一个暗示。举个例子： 如果门打开了，就拉响警报。
请注意，警报仍然可能因门打开以外的其他原因（例如窗户打开）而触发。

这是它的真值表。假设您正在为客户编写警报系统。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)

让我们看看方程式（<=>或“仅当”）。仅当两个选项的值相同时才适用。此示例保留警报，但将其更改为仅当门打开时才发出警报。
注意：这次打开的窗户不应该触发警报，只有门会触发。

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)

这是在规范中经常混淆和写错的东西（如果你知道的话，它也很方便地作为法律辩护）。

于 2017-11-11T22:29:42.097 回答
3 
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对于and的非布尔值，TLA+ 未指定B运算符的含义。<=>对布尔运算符的适度解释，A <=> B对于非布尔值，可能是非布尔A值B。对于自由解释，A <=> B是布尔值，尽管该值未指定为非布尔值A, B。

[1] 中第 296--297 页的第 16.1.3 节“布尔运算符的解释”和第 9--11 页（特别是第 9 页）的第 1.1 节“命题逻辑”与运算符<=>和=>含义最相关。

[1] Leslie Lamport，“指定系统”，Addison-Wesley，2002

于 2017-11-11T23:57:47.820 回答