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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 12 Mar 2020 08:55:51 +0100*References*: <a0c81c85-cf49-424d-9e7a-0c8876db6cec@googlegroups.com> <CAFEV_-j4ns-VAFFHq8-BQOoQ4UK2QR0sCTducteQKpvUBLZHOw@mail.gmail.com> <156ed98e-9c77-4dbf-911e-7ddedb2b3b7c@googlegroups.com> <CAFEV_-geq22WxpXF49yRZ7UQys9KDU68RFhCsOeR8HCXAm+iMw@mail.gmail.com>

In this discussion, it is important to make a distinction between a specification and an instance of a specification. A CONSTANT parameter in a specification represents an arbitrary value (possibly constrained by an assumption that delimits values for which the module is intended to be meaningful). By assigning different values to the constant parameters, we obtain different instances of the specification. The value is fixed for every instance, in particular it never changes during or across behaviors considered for that particular instance of the specification. TLC checks the correctness of instances of TLA+ specifications, and that's why you fix the values of constants when you launch TLC.A TLA+ specification is correct (cf. section 17.6 of Specifying Systems) if the assumptions imply the theorems, and this means that any instance has to be correct (observe that the non-meaningful instances are trivially correct). Because there are infinitely many values, you cannot use TLC to check the correctness of a specification, but you can reason symbolically about TLA+ specifications, as with TLAPS.Hope this helps, 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/792666D4-051B-4057-95C7-368A0C7379BE%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] meaning of CONSTANT***From:*ss . nedunuri

**References**:**[tlaplus] meaning of CONSTANT***From:*ns

**Re: [tlaplus] meaning of CONSTANT***From:*Apostolis Xekoukoulotakis

**Re: [tlaplus] meaning of CONSTANT***From:*ns

**Re: [tlaplus] meaning of CONSTANT***From:*Apostolis Xekoukoulotakis

- Prev by Date:
**Re: [tlaplus] meaning of CONSTANT** - Next by Date:
**[tlaplus] Re: Error Producing PDF Version** - Previous by thread:
**Re: [tlaplus] meaning of CONSTANT** - Next by thread:
**Re: [tlaplus] meaning of CONSTANT** - Index(es):