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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 15 Apr 2021 09:00:20 +0200*Ironport-hdrordr*: A9a23:BqjL4K1jeJOFr0ScuVKT6wqjBLokLtp033Aq2lEZdDV5etGV/vrAoN01zhnx4Qx+ZFgFlcqbMKeNBVPQnKQY3aArMb2vXBbrtQKTRekI0aLZ3zbiFyfin9Qx6Y5cdcFFYuHNMQ==*References*: <90b306a3-c413-4b09-810e-98aedb44d91fn@googlegroups.com> <BA49039D-022B-486C-B57A-D7DFC676F265@gmail.com> <d9af2d7a-f150-422f-956a-98b6b69f7843n@googlegroups.com>

Hello again, my initial message was perhaps a little cryptic, so let me explain the rationale behind it. You were effectively trying to prove the implication TypeInvariant /\ SafetyProperty /\ Inc => SafetyProperty' but this implication doesn't hold. As a concrete counter-example, consider the state valX = [ val |-> 42, ts |-> 23 ] valY = [ val |-> 42, ts |-> 70 ] clock = 27 (I'm omitting the variable n because it is unimportant for this discussion.) Observe that this state satisfies both TypeInvariant and SafetyProperty. In particular, the latter holds trivially because the left-hand side of the implication is false. Now, Inc will lead you to the state valX = [ val |-> 43, ts |-> 28 ] valY = [ val |-> 42, ts |-> 70 ] clock = 28 and SafetyProperty is false for that state. This shows that SafetyProperty is not inductive (relative to TypeInvariant). However, the first state is actually not reachable in your specification, and one way to rule it out is to observe that time stamps cannot exceed the clock value. This observation leads to asserting the invariant ClockInv, which makes the proof go through. Now, in general there is no guarantee that the additional predicate is an inductive invariant: you may have to iterate the process and successively add more information about reachable states in order to obtain an inductive invariant that you can prove with a proof assistant such as TLAPS. As for model checking, you are completely right that you need to bound the state space that TLC will explore. One standard way to do this is to add a state constraint where you bound the value of clock. 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/A085D874-3F90-4D91-B89C-28C06ED3AB4D%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] TLAPS proof of increment and update***From:*Smruti Padhy

**References**:**[tlaplus] TLAPS proof of increment and update***From:*Smruti Padhy

**Re: [tlaplus] TLAPS proof of increment and update***From:*Stephan Merz

**Re: [tlaplus] TLAPS proof of increment and update***From:*Smruti Padhy

- Prev by Date:
**Re: [tlaplus] Re: Overriding operator which is used in a temporal property** - Next by Date:
**[tlaplus] How to check properties on models with huge numbers of behaviours** - Previous by thread:
**Re: [tlaplus] TLAPS proof of increment and update** - Next by thread:
**Re: [tlaplus] TLAPS proof of increment and update** - Index(es):