You do not have permission to delete messages in this group
Copy link
Report message
Sign in to report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tlaplus
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
unread,
Apr 21, 2021, 12:09:05 PM4/21/21
Reply to author
Sign in to reply to author
Forward
Sign in to forward
Delete
You do not have permission to delete messages in this group
Copy link
Report message
Sign in to report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tla...@googlegroups.com, Andrew Helwer
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.
You do not have permission to delete messages in this group
Copy link
Report message
Sign in to report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tla...@googlegroups.com, Paulo Feodrippe, Andrew Helwer
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
>
> --
> 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
You do not have permission to delete messages in this group
Copy link
Report message
Sign in to report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tlaplus
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
unread,
Apr 22, 2021, 9:44:15 AM4/22/21
Reply to author
Sign in to reply to author
Forward
Sign in to forward
Delete
You do not have permission to delete messages in this group
Copy link
Report message
Sign in to report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tlaplus
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.