Check that both branches are executed

[jakub....@gmail.com]

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)


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

[Leslie Lamport]

What you want to check of your spec is that there is a behavior satisfying Spec in which the formula 

   Q == /\ (state = START) ~> (state = RIGHT) 
        /\ (state = START) ~> (state = LEFT).  

is true.  Let's call that condition Possibly(Spec, Q).  A condition of the form Possibly(Spec, Q) is not expressible in a linear-time temporal logic like TLA.  However, given a TLA+ spec Spec such as the one you wrote and a formula Q, it is possible to find a formula F such that Possibly(Spec, Q) is true if and only if the formula Spec /\ F satisfies Q.    The formula F is the conjunction of conditions of the form WF_vars(A) and/or SF_vars(A) where A is a subaction of the next-state action, meaning that A implies Next.  For your example, you can let

   F == SF_state(state=START /\ state'=LEFT) /\ SF_state(state=START /\ state'=RIGHT)

To understand what's going on, you should read the paper called "Proving Possibility Properties"; here's a link to the paper:

        http://lamport.azurewebsites.net/pubs/pubs.html#lamport-possibility 

The paper is quite mathematical and not easy reading, but it's only 8 pages long (excluding the proof in the appendix that you needn't read).

Leslie

[Leslie Lamport]

I wrote my message in haste.  What I said is true for certain formulas Q, including the formula in jacob.mikian's example.  The paper I referenced considers a different class of formulas Q, and specs without liveness conditions.  But the ideas easily apply to the example.  It would be interesting to try to characterize the class of formulas Q to which it applies.  I suspect that there is a theorem to the effect that for any Spec and Q, where Spec = Init /\ [][Next]_vars /\ G and (Init /\ [][Next]_vars, G) is machine closed (defined in the paper), there is a TLA+ specification FSpec such that Possibly(Spec, Q) is true iff  FSpec => Q  is a valid TLA+ formula.

Leslie

[Stephan Merz]

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

> --
> 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...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.