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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 4 Mar 2020 08:41:39 +0100*References*: <b23791fe-5aa0-48b4-ae13-151105e94d3f@googlegroups.com> <BE5C1A4C-BD12-4F3C-892A-EF1E902EA102@gmail.com> <17e8cb76-2256-4f80-8b89-982187e33eda@googlegroups.com>

The formula Spec (and its sub-formulas Init, Next etc.) express the algorithm as a TLA+ specification, and we then want to verify properties such as Spec => []MutualExclusion Therefore, Spec does not need to be checked, it can be assumed to hold (the implication is trivially true of state sequences that do not satisfy Spec). Concretely, TLC interprets Init and Next in order to construct the initial state(s) and the successor states of any states it has already constructed. For the latter, it considers the different disjuncts in the definition of Next: any successor state allowed by some of these formulas is allowed by Next. For details on how TLC interprets these formulas, please see Specifying Systems, and if you have not yet done so, watch the video lectures on TLA+. Regards, Stephan
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7AA48EF6-EC08-45F8-A8AA-EFAD96963737%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Spec formula for Peterson algorithm***From:*Mursel Musabasic

**References**:**[tlaplus] Spec formula for Peterson algorithm***From:*Mursel Musabasic

**Re: [tlaplus] Spec formula for Peterson algorithm***From:*Stephan Merz

**Re: [tlaplus] Spec formula for Peterson algorithm***From:*Mursel Musabasic

- Prev by Date:
**Re: [tlaplus] Spec formula for Peterson algorithm** - Next by Date:
**Re: [tlaplus] TCP/IP client/server communication protocol** - Previous by thread:
**Re: [tlaplus] Spec formula for Peterson algorithm** - Next by thread:
**Re: [tlaplus] Spec formula for Peterson algorithm** - Index(es):