[tlaplus] Re: PlusCal resources?

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

For TLA+ itself:

• Appropriately, TLA+ has a spec of its own grammar written in TLA+; this had some bugs I fixed and can be found here: https://github.com/tlaplus-community/tlaplus-standard/tree/main/grammar
• Alternatively you might prefer the presentation of the grammar in https://github.com/tlaplus-community/tree-sitter-tlaplus
• Specifying Systems has a chapter on the TLA+ 1 grammar & semantics
  
• Changes introduced in TLA+ 2 are summarized on this page: http://lamport.azurewebsites.net/tla/tla2.html

For PlusCal:

• P syntax & semantics: https://lamport.azurewebsites.net/tla/p-manual.pdf
• C syntax & semantics: https://lamport.azurewebsites.net/tla/c-manual.pdf

Are you looking to write a parser or interpreter, or just looking to understand which operators TLC defines?

Andrew Helwer

On Thursday, August 17, 2023 at 9:16:10 AM UTC-4 Gal Vardi wrote:

Popping again the same repeating question, once every two years :) Have anyone found (or wrote?) or knows a formal definition document of the TLA+ syntax, semantics, grammar ?
I am looking for something which is ASCII-text-searchable e.g. I want to know what is the meaning and usage of '\subseteq' operator?

Gal.

ב-יום שלישי, 14 בספטמבר 2021 בשעה 20:56:40 UTC+3, Andrew Helwer כתב/ה:

Where can I find language standard documents and other things relating to PlusCal? I don't mean tutorials, I mean something like a BNF grammar and semantics similar to chapters 15-17 of Specifying Systems or stuff found on this site: http://lamport.azurewebsites.net/tla/tla2.html

Andrew

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/79dbd4b2-69d2-4d2a-aba4-f084a979a3f7n%40googlegroups.com.