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?