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

*From*: TLA Plus <tlapl...@xxxxxxxxx>*Date*: Tue, 23 Apr 2013 10:17:06 -0800

Chris Newcomb discovered that when a spec extends the Reals module,

TLC thinks that "a" / "b" equals {"a", "b"}. Since how this is fixed

could conceivably affect other users, I'm opening a discussion of it

here. Most people on the list other than the developers of TLAPS

will probably want to ignore this thread.

Here is the explanation of the bug. The official standard modules

Naturals, Integers, and Reals given in "Specifying Systems" define the

semantics of the arithmetic operators, but they are of no use to any

tool. So, to speed up parsing, dummy versions of those modules are

used by the parser. The dummy versions of Naturals and Integers are

ignored by TLC and TLAPS. However, the dummy version of Reals is used

by TLC and I presume by TLAPS. The body of that module is:

EXTENDS Integers

Real == { }

a / b == {a, b}

Infinity == 999999999

The question is, what should the definitions be. It's easy to make up

definitions that will cause errors when TLC tries to evaluate these

definitions. However, can we do anything that will make this module

usable by TLAPS? I don't see how, since I think we should maintain the

semantics that Int is a subset of Real and the arithemetic operators

like + and * on integers are the restrictions of the ones on reals.

But I'm open to suggestions.

We can make TLC produce appropriate error messages when the Reals

operators are used without the use of a suitable dummy Reals module:

we can write a Java Reals class for TLC that overrides these

definitions. I'm not going to do that myself, but I'll be happy to

consider adding such a module if someone else wants to write it.

(It should be easy to figure out how it's done by searching the

source code for the Naturals.java and Integers.java classes.)

Barring other suggestions, I will modify the dummy Reals module. I

welcome suggestions for what I should do. For example, should we keep

the current definition of Infinity? Should I change the definition of

Real so that TLC will always produce an error in evaluating exp \in

Real? Or should it evaluate -3 \in Real to TRUE?

**Follow-Ups**:**Re: [tlaplus] How should we fix a very minor TLC bug?***From:*Stephan Merz

- Prev by Date:
**Version 1.4.6: Open Source Release of TLA+ Tools** - Next by Date:
**Checking FIFO module** - Previous by thread:
**Re: Version 1.4.6: Open Source Release of TLA+ Tools** - Next by thread:
**Re: [tlaplus] How should we fix a very minor TLC bug?** - Index(es):