Re: [tlaplus] Check that both branches are executed

[Stephan Merz <stepha...@xxxxxxxxx>]

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.