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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 7 Jan 2016 10:28:17 -0800 (PST)*References*: <71319d03-6ab4-48a7-a6a2-53e7c9c48a51@googlegroups.com>

A TLA+ specification is a mathematical formula. "Evaluation' is not a

meaningful concept in mathematics. TLC is a program, one of its tasks

being to compute the set of possible next states of an action for a

given state. Since this involves trying to solve an unsolvable

problem, TLC uses certain heuristics. For example, it will do this

for the action formula (x' = 1) /\ (y' = x') but not for the

equivalent action formula (y' = x') /\ (x' = 1).

TLC's heuristics are insensitive to the use of definitions. In your

example, it handles Foo(x)' exactly the way it handles (x \cup y)',

which is exactly the way it handles (x' \cup y').

In almost all cases that arise in practice, it is easy to rewrite a

sensible action formula in a form that TLC can handle--for example by

rewriting (y' = x') /\ (x' = 1) as (x' = 1) /\ (y' = x'). Thus, if

you can't find such a rewriting, the odds are that your formula is not

sensible because it doesn't mean what you think it should. It may

therefore be instructive if you would post an action formula (that is

as simple as possible) that you would like TLC to evaluate but that

it doesn't.

Leslie

**Follow-Ups**:**Re: Tagged formulas***From:*Ron Pressler

**References**:**Tagged formulas***From:*Ron Pressler

- Prev by Date:
**Re: Tagged formulas** - Next by Date:
**Re: Tagged formulas** - Previous by thread:
**Re: Tagged formulas** - Next by thread:
**Re: Tagged formulas** - Index(es):