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:
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)
=============================================================================