| Hello,
TLAPS is an interactive proof system, that is, the user writes a proof that is then checked by machine. In order to use it, you need to install TLAPS as described on the Web pages [1] and then use it from the Toolbox. The Web pages have a minimal tutorial to get you started.
Best, Stephan
On 6 May 2019, at 13:15, Shiyao MA < i@xxxxxxxxx> wrote:
Hi Stephan,
How to invoke the tlaps tool to check theorems?
like, `java tlap.class.`?
Best, On Saturday, 7 July 2018 19:39:04 UTC+8, 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
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 tla...@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.
--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|