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

[tlaplus] TLAPS proof of increment and update



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