Check that both branches are executed

[jakub....@xxxxxxxxx]

I have a specification that can branch from START to LEFT or to RIGHT state. Is that possible to check that there exist different execution paths covering both branches?

The check CheckEventualStates passes, but it does not ensure that LEFT (nor RIGHT) is ever reached by any execution path.

------------------------------ 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 paths covering both
branches - state might never be LEFT.
*)
CheckEventualStates == \/ (state = START) ~> (state = RIGHT)
                       \/ (state = START) ~> (state = LEFT)


=============================================================================