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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Tue, 20 Oct 2015 13:05:53 -0700 (PDT)*References*: <4a40f27f-5358-4339-84e1-1ceff5eecefa@googlegroups.com>

Your specifications are indeed nonsensical--apparently much more

nonsensical than you suspect. You seem to be under the mistaken

impression that a TLA+ specification is some kind of program and the

_expression_ x'=x+1 is an assignment statement that changes the value of

x when it is evaluated.

nonsensical than you suspect. You seem to be under the mistaken

impression that a TLA+ specification is some kind of program and the

_expression_ x'=x+1 is an assignment statement that changes the value of

x when it is evaluated.

A TLA+ specification is a formula, and evaluating a formula doesn't

change anything. Starting in the initial state, the possible next

states are specified by all possible values of a' and x' such that

your formula Next is true when x=1 and a=TRUE. To understand what is

going on, I suggest that for each of your definitions of Next, you

find 17 next states that it allows from the initial state. (This

isn't difficult, because there are so many next states that they don't

even form a set.)

change anything. Starting in the initial state, the possible next

states are specified by all possible values of a' and x' such that

your formula Next is true when x=1 and a=TRUE. To understand what is

going on, I suggest that for each of your definitions of Next, you

find 17 next states that it allows from the initial state. (This

isn't difficult, because there are so many next states that they don't

even form a set.)

When you understand what your specifications mean, you will appreciate

why TLC can't compute their possible behaviors. What particular error

messages TLC produces for them isn't of much interest.

why TLC can't compute their possible behaviors. What particular error

messages TLC produces for them isn't of much interest.

Leslie

**Follow-Ups**:**Re: Unclear TLC evaluation behavior***From:*Ron Pressler

**References**:**Unclear TLC evaluation behavior***From:*Ron Pressler

- Prev by Date:
**Unclear TLC evaluation behavior** - Next by Date:
**Re: Unclear TLC evaluation behavior** - Previous by thread:
**Unclear TLC evaluation behavior** - Next by thread:
**Re: Unclear TLC evaluation behavior** - Index(es):