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.
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,
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...@xxxxxxxxxxxxxxxx
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