TLC 模型检查器不会在公式的 and/or 列表版本上终止

TLC model checker doesn't terminate on an and/or list version of formula

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

我正在观看 Leslie Lamport 的有关 TLA+ 的视频。在 video number four 中,称为 "Die Hard",他给出了实现 BigToSmallSmallToBig 公式的练习。长话短说:我们需要正确计算将 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

我尝试使用这个 and/or 列表:

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

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

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

如果我将其重写为

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

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

在这两个版本中,我们不能没有 Condition 就没有 A。在旧版本中,我们不能有B Condition。不过,在新版本中,我们可以使用 BCondition:这是一个有效的操作。