# Re: [tlaplus] Check that both branches are executed

Hello,

at the risk of stating the obvious: if all you want to check is if there exists an execution that may reach state LEFT (or RIGHT) at some point, you can check the invariant

state # LEFT    (or, state # RIGHT)

and let TLC produce a counter-example. Leslie's answer covers a much more general class of properties, such as the existence of a path that passes through both states at different points of time.

Stephan

> On 10 Dec 2017, at 22:18, jakub....@xxxxxxxxx wrote:
>
> 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)
>
>
> =============================================================================
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.