What operators are defined in TLA+ BUILTINS?

[Andrew Helwer]

The operator TRUE, for example, is not part of the language spec. However if you try to define it:

TRUE == 5

You get a parser error saying it is already defined in module --TLA+ BUILTINS--. What other operators are defined in this module?

[Martin]

Hello Andrew,

The book "Specifying Systems"[1] has a description and the semantics of the
built-in operators of TLA+ in chapter 16 (p.291). The error message might be a
bit confusing because built-in operators do not need to live in their own
module, that's just how TLC handles it.

cheers,
Martin

[1] https://lamport.azurewebsites.net/tla/book.html

> --
> 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...@googlegroups.com
> <mailto:tlaplus+u...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tlaplus/e66c183c-d270-4807-9d2a-fab593539cbbn%40googlegroups.com
> <https://groups.google.com/d/msgid/tlaplus/e66c183c-d270-4807-9d2a-fab593539cbbn%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Paulo Feodrippe]

Besides the book and if you wanna check some TLC code, you can also see https://github.com/tlaplus/tlaplus/blob/d977051118f63b9c97d7d4c4d6af27183971ada3/tlatools/org.lamport.tlatools/src/tla2tex/BuiltInSymbols.java#L221. 

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/83f97890-d829-2d7b-c16a-c0568cd86d75%40gmail.com.

[Martin]

Hello Paolo,

The list you referenced contains all operator names that have some special
treatment (e.g. also all infix operators are included in the table or lexemes
neccessary for writing proofs). If you just need a new operator name that table
is perfect for checking collisions. But it's not a problem to write

EXTENDS Naturals

a \sim b == (a-b) % 2 == 0 \* a ~ b are congruent modulo two

even though \sim is listed.

cheers,
Martin

On 4/21/21 6:14 PM, Paulo Feodrippe wrote:
> Besides the book and if you wanna check some TLC code, you can also
> see https://github.com/tlaplus/tlaplus/blob/d977051118f63b9c97d7d4c4d6af27183971ada3/tlatools/org.lamport.tlatools/src/tla2tex/BuiltInSymbols.java#L221

> <https://github.com/tlaplus/tlaplus/blob/d977051118f63b9c97d7d4c4d6af27183971ada3/tlatools/org.lamport.tlatools/src/tla2tex/BuiltInSymbols.java#L221>. 

> <mailto:tlaplus%2Bunsu...@googlegroups.com>
> > <mailto:tlaplus+u...@googlegroups.com
> <mailto:tlaplus%2Bunsu...@googlegroups.com>>.

> > To view this discussion on the web visit
> >
> https://groups.google.com/d/msgid/tlaplus/e66c183c-d270-4807-9d2a-fab593539cbbn%40googlegroups.com
> <https://groups.google.com/d/msgid/tlaplus/e66c183c-d270-4807-9d2a-fab593539cbbn%40googlegroups.com>
> >

> <https://groups.google.com/d/msgid/tlaplus/e66c183c-d270-4807-9d2a-fab593539cbbn%40googlegroups.com?utm_medium=email&utm_source=footer

> <https://groups.google.com/d/msgid/tlaplus/e66c183c-d270-4807-9d2a-fab593539cbbn%40googlegroups.com?utm_medium=email&utm_source=footer>>.
>
> --
> 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...@googlegroups.com

> <mailto:tlaplus%2Bunsu...@googlegroups.com>.

> To view this discussion on the web visit

> https://groups.google.com/d/msgid/tlaplus/83f97890-d829-2d7b-c16a-c0568cd86d75%40gmail.com
> <https://groups.google.com/d/msgid/tlaplus/83f97890-d829-2d7b-c16a-c0568cd86d75%40gmail.com>.

>
> --
> 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...@googlegroups.com
> <mailto:tlaplus+u...@googlegroups.com>.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/tlaplus/CANDKcwDHORK-jrnEMRoPoeon5Pn3Tg2LW64ovn3TQ-hmXGbUHA%40mail.gmail.com
> <https://groups.google.com/d/msgid/tlaplus/CANDKcwDHORK-jrnEMRoPoeon5Pn3Tg2LW64ovn3TQ-hmXGbUHA%40mail.gmail.com?utm_medium=email&utm_source=footer>.

[Leslie Lamport]

There is no actual TLA+ Builtins module; that was apparently an easy way to report that TRUE is a TLA+ primitive.  I'm not sure what you mean by "the language spec".  TRUE does appear in Table 1 of "Specifying Systems".  It's not part of the syntax specification because, syntactically, it's just an operator that takes no argument.  The only other such built-in operators in that table are FALSE, BOOLEAN, and STRING.  I can't think of any others, but perhaps someone can think of another one that isn't listed in that table that I have forgotten.  I expect searching SANY's code for BOOLEAN would reveal it if it exists.

Leslie

[Andrew Helwer]

Oh yes I meant the BNF grammar specifically, not the entirety of the language spec. Makes sense they are captured by the identifier token instead of having their own rule.

I looked through the codebase and can't find where these builtins get special treatment, but wherever I find BOOLEAN I also find TRUE, FALSE, and STRING, so Leslie you're probably right that is all of them.

Andrew