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

*From*: Nikola Kasev <nikola...@xxxxxxxxx>*Date*: Fri, 6 Jul 2018 14:36:11 -0700 (PDT)

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

**Follow-Ups**:**Re: [tlaplus] What is the purpose of THEOREM in AsynchInterface?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Invariant valid in all states but one** - Next by Date:
**Re: [tlaplus] What is the purpose of THEOREM in AsynchInterface?** - Previous by thread:
**Re: [tlaplus] Invariant valid in all states but one** - Next by thread:
**Re: [tlaplus] What is the purpose of THEOREM in AsynchInterface?** - Index(es):