Re: Check that both branches are executed

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

On Sunday, December 10, 2017 at 5:39:24 PM UTC-8, Leslie Lamport wrote:

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

On Sunday, December 10, 2017 at 4:59:27 PM UTC-8, jakub.mikians 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)

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