[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] What is the purpose of THEOREM in AsynchInterface?

Thank you for the explanation, Stephan.

On Saturday, July 7, 2018 at 1:39:04 PM UTC+2, Stephan Merz wrote:

TLC ignores THEOREMs in TLA+ modules: invariants and general temporal properties that you want to be model checked over the current specification have to be indicated via the respective fields of the TLC pane of the Toolbox. In that sense, consider THEOREMs to be formal comments for the reader of your specification. However, TLAPS (the TLA+ proof system) can be used to check proofs of theorems.


On 6 Jul 2018, at 23:36, Nikola Kasev <niko...@xxxxxxxxx> wrote:

I'm reading the "Specifying Systems" book and was wondering what is the purpose of the theorem definition on the last line in the AsynchInterface module (page 27)?

When configuring the model with Spec as the Temporal formula and TypeInvariant as an invariant to check, running the TLC model checker finds no errors. Removing the THEOREM definition seems to have no impact on the outcome of the checks. Is it for readability purposes only?

What am I missing?

Thank you for helping,
- Nikola  

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.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.