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

*From*: Smruti Padhy <smruti.padhy@xxxxxxxxx>*Date*: Mon, 12 Apr 2021 12:19:11 -0700 (PDT)*Ironport-hdrordr*: A9a23:sqk9DKl+rouzwqeT4WIg+Kno7EfpDfOiimdD5ilNYBxZY6Wkvuqpm+kW0gKxtSYJVBgb6Kq9EYSjYVeZz5565oENIayvNTON1VeAAYl+4eLZslndMgLk8Oo179YGT4FaCMfsSXBgh8f7/wXQKadV/PCj8Lq0wcbTym4Fd3AeV4hE7x1lTia3e3cGNTVuIJoiCd6k4NBbzgDQC0g/S8SgGz04WPLerMfAj5LsbXc9dmkawS2vqR/t17LgCRif2X4lIkhy6JMr8W3ElAK846W4rpiAu2Hh/kve9Y5fltek6tYrPr30tuEtMTnnhgulY45sMofywwwdm+2k5FY0nNSkmX5JVLUQ11rrcnixsV/R3WDboUoTwkXvzlKVmhLYzvDRfi4wCMZKmOtiA2Pkwncn1esMtp5j7iazu5ZRMBLNhyiV3amqazha0mSx5V4vi/QagXAaa5YXdbM5l+Ii1XIQPpEHEif3rK0EMM0rNsHT4/5KbUiXBkq0gkBfhPKrWHo3ElOpWU4fo4i03lFt7QNE5npd6soYkHINsKg4VoAB3eLZKa5l/YsucuYmKYRnBOkARsOzTlbARh/BKwupUCnaPZBCAH7Gp57p7Lhd3oHaHaAg/d8JgZzEFHlYuWQxd0+rKcrL8oZM7gmlehTMYQjQ

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.

----------------------- MODULE IncrementUpdatePattern ----------------------- (* This spec demonstrate an example of Increment and update pattern of two variables - Increment the first variable at a time and then update the second variable with the incremented value of the first variable. 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 time stamp associated with it. valX is incremented by 1 and valY is updated with new value of valX. This increment and update pattern is an abstraction that can be used during server/worker zero-downtime updates. We use TLAPS to prove the safety property of the spec. *) EXTENDS Naturals, TLAPS CONSTANTS MaxNum \* Maximum number X can take ASSUME SpecAssumption == /\ MaxNum \in (Nat \ {0}) \* MaxNum can not be zero --------------------------------------------------------------------------------------- VARIABLES valX, valY, clock, n vars == <<valX, valY, clock, n>> (* *********************************** Invariants and Temporal Properties *********************************** *) \* An invariant: ensures all the variables maintain the proper types. TypeInvariant == /\ valX \in [val:Nat, ts: Nat] /\ valY \in [val:Nat, ts: Nat] /\ clock \in Nat /\ n \in Nat (* If val of valX is greater than the val of valY, then the time of update of valX is greater than or equal to ValY *) SafetyProperty == (valX.val > valY.val) => valX.ts >= valY.ts ---------------------------------------------------------------------------------------- Init == /\ valX = [val|->1, ts|->0] /\ valY = [val|->0, ts|->0] /\ clock = 0 /\ n = 0 Inc == /\ n < MaxNum /\ valX.ts <= clock \*<-this is required only for proof /\ valY.ts <= clock \*<-this is required only for proof /\ n' = n+1 /\ clock' = clock + 1 /\ valX'=[val|->valX.val + 1, ts|->clock'] /\ UNCHANGED<<valY>> Update == /\ valY.val < valX.val /\ clock' = clock + 1 /\ valY'=[val|->valX.val, ts|->clock'] /\ UNCHANGED<<valX,n>> Next == Inc \/ Update Spec == Init /\ [][Next]_vars ------------------------------------------------------------------------------------------------------------ IInv == TypeInvariant THEOREM TypeCorrect == Spec => []IInv <1>1. Init => IInv BY SpecAssumption DEF Init, IInv, TypeInvariant <1>2. IInv /\ [Next]_vars => IInv' <2> SUFFICES ASSUME IInv, [Next]_vars PROVE IInv' OBVIOUS <2>. USE SpecAssumption DEF Init, IInv, TypeInvariant <2>1. CASE Inc BY <2>1 DEF Inc <2>2. CASE Update BY <2>2 DEF Update <2>3. CASE UNCHANGED vars BY SpecAssumption, <2>3 DEF vars <2>4. QED BY <2>1, <2>2, <2>3 DEF Next <1>. QED BY <1>1, <1>2, PTL DEF Spec --------------------------------------------------------------------------------------------------------- THEOREM Spec => []SafetyProperty <1>1. Init => SafetyProperty <2> SUFFICES ASSUME Init PROVE SafetyProperty OBVIOUS <2>. USE SpecAssumption DEF Init, IInv, TypeInvariant, SafetyProperty <2>1. CASE Inc BY <2>1 DEF Inc <2>2. CASE Update BY <2>2 DEF Update <2>3. CASE UNCHANGED vars BY SpecAssumption, <2>3 DEF vars <2>4. QED BY <2>1, <2>2, <2>3 DEF SafetyProperty <1>2. IInv /\ SafetyProperty /\ [Next]_vars => SafetyProperty' <2> SUFFICES ASSUME IInv, SafetyProperty, [Next]_vars PROVE SafetyProperty' OBVIOUS <2>. USE SpecAssumption DEF Init, IInv, TypeInvariant, SafetyProperty <2>1. CASE Inc BY <2>1 DEF Inc <2>2. CASE Update BY <2>2 DEF Update <2>3. CASE UNCHANGED vars BY <2>3 DEF vars <2>4. QED BY <2>1, <2>2, <2>3 DEF Next <1>. QED BY <1>1, <1>2, TypeCorrect, PTL DEF Spec ============================================================================= \* Modification History \* Last modified Mon Apr 12 12:32:29 CDT 2021 by spadhy \* Created Tue Mar 30 13:58:07 CDT 2021 by spadhy

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

**[tlaplus] Re: TLAPS proof of increment and update***From:*Ayush Pandey

- Prev by Date:
**Re: [tlaplus] Proving refinement for specs with fairness properties** - Next by Date:
**[tlaplus] Re: TLAPS proof of increment and update** - Previous by thread:
**Re: [tlaplus] Proving refinement for specs with fairness properties** - Next by thread:
**[tlaplus] Re: TLAPS proof of increment and update** - Index(es):