Make sure the branches are complete

Question

The program can go from START to the LEFT or RIGHT branch. How can I check if there is an execution path for the LEFT branch and another execution path for the RIGHT branch?

------------------------------ 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

In a very general case, there is no way to verify that for each state at least one behavior ultimately achieves this. This is due to the fact that TLA + is based on linear time logic , which does not have a means of expressing a property that contains several different types of behavior.

Depending on the specific case, sometimes you can earn. For example, we could write

Left == 
  /\ state = START
  /\ state' = LEFT

Right ==
  /\ state = START
  /\ state' = RIGHT

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

Then you can check for two branches with

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