Re: [tlaplus] TLAPS proof of increment and update

Hello,

the problem is that your safety property is not an inductive invariant (even with respect to the typing invariant). However, it is easy to see that the time stamps of your variables can never exceed the clock value, and so the extra guard that you added to the Inc action is actually an invariant of your specification. It even happens to be an inductive invariant.

The attached TLA+ module contains a proof of the safety property. Please see the TLAPS tutorial or other examples in the distribution for the concept and the importance of inductive invariants.

Hope this helps,

Stephan

P.S.: The constant MaxNum is (obviously) unnecessary for the prover – better add a state constraint to the model that you use for TLC instead of adding a spurious precondition in your specification. -s

--
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/BA49039D-022B-486C-B57A-D7DFC676F265%40gmail.com.

Attachment: inc_spec.tla
Description: Binary data

On 12 Apr 2021, at 21:19, Smruti Padhy <smruti.padhy@xxxxxxxxx> wrote:

Hi,
I have been trying different proofs with TLAPS. In the spec attached in this conversation, I tried a simple example of increment and update of two variables. That is, Increment the first variable at a given time and then update the second variable with the incremented value of the first variable at a different time.
This spec has two variables - valX and valY. valX and valY are represented as a record with two fields: val that can take Natural numbers and ts as timestamp associated with it. We use a global clock for time.
valX is incremented by 1 and valY is updated with the new value of valX. This increment and update pattern is an abstraction that can be used during server/worker zero-downtime updates.
I was able to use TLAPS to prove the safety property of the spec. But it required two extra enabling conditions in the Inc action for the proof to work:
/\ valX.ts <= clock \*<-this is required only for proof
   /\ valY.ts <= clock \*<-this is required only for proof
I am not clear as to why we would need these two conditions. It should follow from the induction hypothesis.

I would appreciate it if someone can provide me some more insights into the workings of the TLAPS proof.
I have attached the spec with this conversation.
Best,
Smruti
ps: I am unable to post any attached TLA+ spec to this group in my conversation. so renamed the file with .txt.

--
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/90b306a3-c413-4b09-810e-98aedb44d91fn%40googlegroups.com.
<inc_spec.tla.txt>