检查分支执行

Question

程序可以从启动到左或右分支分支。我如何检查左分支有执行路径和右分支的另一个执行路径？

------------------------------ MODULE WFBranch ------------------------------
VARIABLE state
START == "start"
LEFT == "left"
RIGHT == "right"
Init == state = START
Next ==
    /  / state = START
        /  / state' = LEFT
            / state' = RIGHT
    /  / state in {LEFT, RIGHT}
        / state' = START
Spec ==
    / Init
    / [][Next]_<<state>>
    / WF_<<state>>(Next) * Avoid stuttering at start
(*
This passes, but it does not ensure that there exist different paths covering both
branches - e.g. state might never be LEFT.
*)
CheckEventualStates == / (state = START) ~> (state = RIGHT)
                       / (state = START) ~> (state = LEFT)
=============================================================================

Answer 1

在"完全一般案例中"中，无法检查每个状态，至少一种行为最终达到了这一点。这是因为TLA 基于线性时间逻辑，它没有表达在多种不同行为之间存在的属性的方法。

根据特定的情况，有时您可以制作subsitutes。例如，我们可以写

Left == 
  / state = START
  / state' = LEFT
Right ==
  / state = START
  / state' = RIGHT
Next ==
    /  / state = START
        /  / Left
            / Right
    /  / state in {LEFT, RIGHT}
        / state' = START

然后您可以检查有两个分支

CheckEventualStates ==
    / <>(ENABLED Left)
    / <>(ENABLED Right)