TLC模型检查器不会终止于公式的和/或列表版本

Question

这也许是个很愚蠢的问题，但我还是会问的。

我正在看莱斯利·兰波特关于TLA+的视频。在四号录影带中，他给出了一个实现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

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

Answer 1

如果我把它重写为

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

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

在这两个版本中，我们都不能没有A而没有Condition。在旧版本中，我们不能使用B和Condition。但是，在新版本中，我们可以使用B和Condition：这是一个有效的操作。

Answer 2

让TLC检查一下TypeOK。反例会告诉你发生了什么。