检查分支是否执行

Question

程序可以从 START 分支到 LEFT 或 RIGHT 分支。如何检查是否存在 LEFT 分支的执行路径和 RIGHT 分支的其他执行路径？

------------------------------ 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+ 基于 线性时序逻辑 ，它无法表达属性在多个不同行为之间成立。

根据特定的情况，有时您可以进行替代。例如，我们可以写

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)

检查分支是否执行

Check that branches are executed

formal-verification

tla+