Re: [tlaplus] How should we fix a very minor TLC bug?

[Stephan Merz <stepha...@xxxxxxxxx>]

Hi Leslie,

TLAPS appears to treat the dummy module for the Reals just like those for Naturals and Integers, i.e. ignore it. The operators defined in module Reals appear to be recognized as built-in symbols, but no backend handles them yet.

The definitions in the dummy module are indeed not helpful. For example, they imply

  \A x,y : x/y = y/x
  \A x \in Real : x = 0    \* since Real = {}
  Infinity \in Nat /\ Infinity+1 > Infinity

One can discuss if it makes sense for TLC to handle real numbers (arguably, floats may make sense), but whatever decision is taken it doesn't look like it will impact the prover. For the moment, I believe that redefining the operators in the dummy module so that they raise errors is the most sensible thing to do.

Best,
Stephan


On Apr 23, 2013, at 8:17 PM, TLA Plus <tlapl...@xxxxxxxxx> wrote:

> 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?  
> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
>  
>