[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sun, 10 Dec 2017 17:39:23 -0800 (PST)*References*: <6eeeba09-d478-40b8-9345-85cdab38e1f2@googlegroups.com>

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).

/\ (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)

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

**Follow-Ups**:**Re: Check that both branches are executed***From:*Leslie Lamport

**References**:**Check that both branches are executed***From:*jakub . . . .

- Prev by Date:
**Check that both branches are executed** - Next by Date:
**Re: Check that both branches are executed** - Previous by thread:
**Check that both branches are executed** - Next by thread:
**Re: Check that both branches are executed** - Index(es):