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

[tlaplus] Re: TLAPS proof of increment and update

Thank you, Ayush for your reply. 

On Monday, April 12, 2021 at 3:05:18 PM UTC-5 ayushpand...@xxxxxxxxx wrote:
I am not an expert not even intermediate with TLAPS so I might be completely wrong but I found 2 interesting things in this proof. 
  1. You do not need the condition /\ valX.ts <= clock \*<-this is required only for proof  for TLAPS to prove your theorems.
  2. Clock is the main culprit of the proof not working properly.
I don't know if I can explain this very well but the obligation that fails in the proof is <2>1. If we perform a symbolic execution of the states, we know that Init => SafetyProperty. This is obvious. Now, in any state other than init, we start with an assumption that safety property holds so, (valX.val > valY.val) => valX.ts >= valY.ts  is true. Now if you apply the operations of the Inc state, clock becomes clock+1 and valX becomes [valX.val+1, clock+1].  Now replace these changes in the safety property which should hold true. We get:

(valX.val+1 > valY.val) => clock+1 >= valY.ts 

With any of the assumptions you started with, it is not possible to prove this. This problem goes away when you add valY.ts <= clock because suddenly the proof assistant has another assumption it can use with the Inc state.

On Monday, April 12, 2021 at 9:19:11 PM UTC+2 smruti...@xxxxxxxxx wrote:


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.  



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/e6b41e9a-c035-4e18-858b-19d09338b547n%40googlegroups.com.