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

[Nikola Kasev <nikola...@xxxxxxxxx>]

Thank you for the explanation, Stephan.

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

Hello,

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.

Regards,

Stephan

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.