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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Tue, 23 May 2017 10:02:04 -0700 (PDT)*References*: <ac80049f-bdce-4141-b09b-929a63f649de@googlegroups.com>

There is a very simple explanation of why TLC is evaluating both

clauses of the disjunction even when the first is true. Consider the

spec with this initial predicate and next state relation:

clauses of the disjunction even when the first is true. Consider the

spec with this initial predicate and next state relation:

Init == x = 22

Next == \/ /\ x > 7

/\ x' = 42

\/ /\ x > 9

/\ x' = 24

/\ x' = 42

\/ /\ x > 9

/\ x' = 24

Would you expect TLC never to find the state with x = 24 because when

evaluating Next, it always finds the first disjunct true and therefore

never evaluates the second disjunct?

When evaluating the next-state action, TLC keeps evaluating any

disjunct that might evaluate to true in order to find all possible

next states. There are some cases in which TLC reports an error when,

if it were more clever, it would know that a subexpression it can't

evaluate does not have to be evaluated to determine the set of

possible next states--for example,

disjunct that might evaluate to true in order to find all possible

next states. There are some cases in which TLC reports an error when,

if it were more clever, it would know that a subexpression it can't

evaluate does not have to be evaluated to determine the set of

possible next states--for example,

Init == x = 0

Next == IF x = "abc" THEN x'= x+1 ELSE x'=x+1

Next == IF x = "abc" THEN x'= x+1 ELSE x'=x+1

This is not the case in your example, because the value of the first

conjunct of Tick is unspecified if record equals NoRecord, since that

subexpression is then of the form TRUE \/ e where the value of e is

not necessarily a Boolean. Hence, the set of possible next states in

that case is not specified by the semantics of TLA+.

conjunct of Tick is unspecified if record equals NoRecord, since that

subexpression is then of the form TRUE \/ e where the value of e is

not necessarily a Boolean. Hence, the set of possible next states in

that case is not specified by the semantics of TLA+.

Leslie

**References**:**TLC not handling disjunction correctly in special case?***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] TLC not handling disjunction correctly in special case?** - Next by Date:
**Re: [tlaplus] TLC not handling disjunction correctly in special case?** - Previous by thread:
**Re: [tlaplus] TLC not handling disjunction correctly in special case?** - Next by thread:
**TLA+ community meeting at FLOC 2018?** - Index(es):