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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 19 Nov 2020 18:35:42 +0100*References*: <09339bc6-eea4-4480-a6ee-75567f92bb4an@googlegroups.com> <58556ffe-17ae-81f0-6c06-9261d4a85225@lemmster.de> <7039e237-bf47-4c72-9941-6edd25188ee8n@googlegroups.com> <a9b78c6b-b5ae-a8af-f281-d95cfd586c1f@lemmster.de> <14047959-eaa6-4691-995d-4d6aa27cbec5n@googlegroups.com> <9BDED377-1BA4-4A2F-944B-E58D3D2D1A26@gmail.com> <13d52375-2f27-4120-831e-867de5fae8a1n@googlegroups.com> <3E5BF84F-15DC-4087-B7D6-AC914F980EBC@gmail.com> <2c130114-1919-4a45-abf9-4690252a34e6n@googlegroups.com>

When you write "BY DEF IInv", the prover replaces the predicate IInv by the conjunction "TypeInvariant /\ SafetyProperty". If you need to expand these predicates as well (and you do in your proof), write "BY DEF IInv, TypeInvariant, SafetyProperty". You can easily test this by launching the prover with only IInv expanded. When the proof fails, the window with the failed proof obligation displays exactly the TLA+ formula that is sent to the back-end provers. In the future, we may enable some expansions of definitions to happen automatically to avoid the tedium of having to indicate exactly which definitions should be used. But for now, the prover will only expand definitions of the operators that you indicate explicitly, except for built-in operators such as logical connectives and elementary arithmetic. (You can write "USE DEF ..." so that certain operators are always expanded from the USE step up to the end of the scope in which the USE directive occurs.) 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/4A8D7376-BC4E-470D-9D3B-B11E5136268F%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Smruti Padhy

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Markus Kuppe

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Smruti Padhy

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Markus Kuppe

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Smruti Padhy

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Stephan Merz

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Smruti Padhy

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Stephan Merz

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Smruti Padhy

- Prev by Date:
**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS** - Next by Date:
**Re: [tlaplus] Is this a (hidden) variable that tells me the state the model checker is in?** - Previous by thread:
**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS** - Next by thread:
**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS** - Index(es):