0

这可能是一个非常愚蠢的问题，但我还是会问。

我正在看 Leslie Lamport 关于 TLA+ 的视频。在名为“Die Hard”的视频四中，他给出了实施BigToSmall和SmallToBig公式的练习。长话短说：我们需要正确计算 3 加仑和 5 加仑的水壶从一个罐子倒到另一个罐子后的水量。

这是他的解决方案：

SmallToBig == IF big + small =< 5
               THEN /\ big'   = big + small
                    /\ small' = 0
               ELSE /\ big'   = 5
                    /\ small' = small - (5 - big)

BigToSmall == IF big + small =< 3
               THEN /\ big'   = 0 
                    /\ small' = big + small
               ELSE /\ big'   = small - (3 - big)
                    /\ small' = 3

我尝试使用这个和/或列出一些东西：

SmallToBig == \/ /\ big + small =< 5
                 /\ big'   = big + small
                 /\ small' = 0
              \/ /\ big'   = 5
                 /\ small' = small - (5 - big)

BigToSmall == \/ /\ big + small =< 3
                 /\ big'   = 0 
                 /\ small' = big + small
              \/ /\ big'   = small - (3 - big)
                 /\ small' = 3

但是当我运行它时，检查并没有终止，我不知道为什么。

4

2 回答 2

2

如果我将其重写为

\* Old
SmallToBig == 
   IF Condition
     THEN A
     ELSE B

\* New
SmallToBig == 
  \/ /\ Condition
     /\ A
  \/ B

在这两个版本中，我们都不能A没有Condition. 在旧版本中，我们不能拥有B with Condition。不过，在新版本中，我们可以使用Bwith Condition: 这是一个有效的操作。

于 2020-02-22T01:24:18.397 回答
1

让 TLC 检查不变量TypeOK。反例将向您展示发生了什么。

于 2020-02-22T01:01:21.527 回答