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

[tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS

I am new to using TLAPS. I have been trying to understand the steps to prove the safety property of a specification using TLAPS. I am trying out a simple producer-consumer example spec where an item is produced and placed in a buffer, and then it is consumed from the buffer. Effectively we have one producer producing an item and one consumer consuming it.  It is a simplified version of BlockingQueue Spec: https://github.com/lemmy/BlockingQueue/blob/master/BlockingQueue.tla.

Here is the spec:

------------------------- MODULE producer_consumer -------------------------

EXTENDS Naturals, Sequences, TLAPS

CONSTANTS MaxTotalNumberOfItemsProduced, (* max number of items that can be produced by a producer *)

         MaxBufferLen                   (* max buffer capacity for produced items *)

ASSUME Assumption == 

         /\ MaxBufferLen \in (Nat \ {0}) (* MaxbufferLen should be atleast 1 *)


VARIABLES buffer, num_of_items_produced, num_of_items_consumed 

vars == <<buffer, num_of_items_produced, num_of_items_consumed>>  

Item == [type: {"item"}]


(* Temporal property: Any item that is produced gets eventually consumed *)

AllItemsConsumed == <>[](Len(buffer) = 0 /\ num_of_items_produced = num_of_items_consumed) 

(* Type Correctness *)

TypeInvariant == /\ buffer \in Seq(Item)

                 /\ Len(buffer) \in 0..MaxBufferLen 

                 /\ num_of_items_produced \in 0..MaxTotalNumberOfItemsProduced

                 /\ num_of_items_consumed  \in 0..MaxTotalNumberOfItemsProduced

(* An Invariant: num of items consumed is always less than or equal to the total number of items produced *)

SafetyProperty == num_of_items_consumed <= num_of_items_produced    


(* Specification *)

Init == /\ buffer = <<>>

        /\ num_of_items_produced = 0 

        /\ num_of_items_consumed = 0              

Produce(item) == /\ Len(buffer) < MaxBufferLen

                 /\ num_of_items_produced < MaxTotalNumberOfItemsProduced

                 /\ buffer'= Append(buffer, item)

                 /\ num_of_items_produced' = num_of_items_produced + 1

                 /\ UNCHANGED<<num_of_items_consumed >>

Consume == /\ Len(buffer) > 0

           /\ buffer'= Tail(buffer)

           /\ num_of_items_consumed' = num_of_items_consumed + 1 

           /\ UNCHANGED<<num_of_items_produced>>          

Next == 

       \/ \E item \in Item: Produce(item)

       \/ Consume

Spec == Init /\ [][Next]_vars

FairSpec == Spec 

           /\ WF_vars(\E item \in Item: Produce(item))

           /\ WF_vars(Consume)


I used TLC to check if properties TypeInvariant and SafetyProperty of the spec are invariants. These properties hold for models with different values of MaxTotalOfItemsProduced and MaxBufferLen. 

I formed a possible inductive invariant :   

  IInv == /\ TypeInvariant

               /\ SafetyProperty

My goal is to prove THEOREM Spec => []IInv 

I read the paper "Proving Safety Properties" by Leslie Lamport. As suggested in the paper, before trying to prove it, I used TLC to check if IInv is an invariant of Spec. It is true that it is an invariant of the Spec. 

Next step is to check IInv /\ [Next]_vars => IInv'

As suggested in the paper, I created a TLC model with behavioral specification with IInv as initial predicate and Next as next-state relation. Then checked if IInv is an invariant. I -am getting the following error in TLC: 


In computing initial states, the right side of \IN is not enumerable.

line 26, col 21 to line 26, col 40 of module producer_consumer

The error occurred when TLC was evaluating the nested

expressions at the following positions:

0. Line 74, column 11 to line 75, column 27 in producer_consumer

1. Line 74, column 14 to line 74, column 26 in producer_consumer

2. Line 26, column 18 to line 29, column 79 in producer_consumer

3. Line 26, column 21 to line 26, column 40 in producer_consumer 


I also checked the BlockingQueue spec for TypeInv. The same error is shown in the TLC.

So, I couldn't check IInv is an invariant for IInv /\ [Next]_vars using TLC.

I tried TLAPS to prove the THEOREM Spec => []IInv .

I am able to prove Step one: 


THEOREM TypeCorrect == Init => IInv


               PROVE  IInv


  <1>1. TypeInvariant

     BY DEF Init, IInv, TypeInvariant 

  <1>2. SafetyProperty

     BY DEF Init, IInv, SafetyProperty 

  <1>3. QED

    BY <1>1, <1>2 DEF IInv


Next, I tried proving 

THEOREM IInv /\[Next]_vars => IInv'

But couldn't succeed.

Here is my attempt to decompose the proof (using TLAPS in TLC) and to prove it:


THEOREM IInv /\[Next]_vars => IInv'



               PROVE  IInv'


  <1>1. ASSUME NEW item \in Item,


        PROVE  IInv'

    <2>1. TypeInvariant'

    <2>2. SafetyProperty'

      <3>1. CASE Next

      <3>2. CASE UNCHANGED vars

      <3>3. QED

        BY <3>1, <3>2

    <2>3. QED

      BY <2>1, <2>2 DEF IInv


  <1>2. CASE Consume

    <2>1. TypeInvariant'

      <3>1. (buffer \in Seq(Item))'

      <3>2. (Len(buffer) \in 0..MaxBufferLen)'

      <3>3. (num_of_items_produced \in 0..MaxTotalNumberOfItemsProduced)'

      <3>4. (num_of_items_consumed  \in 0..MaxTotalNumberOfItemsProduced)'

      <3>5. QED

        BY <3>1, <3>2, <3>3, <3>4 DEF TypeInvariant

    <2>2. SafetyProperty'

    <2>3. QED

      BY <2>1, <2>2 DEF IInv

  <1>3. CASE UNCHANGED vars

  <1>4. QED

    BY <1>1, <1>2, <1>3 DEF Next


I am confused as to what is the best way to decompose proof.  I tried to follow the step by instructions in the Proving Safety Properties paper. In the paper, the example of the decompose proof was for the SimpleMutex algorithm. I am trying to use the same structure of proof here. Also, looked into BlockingQueue proof. It used SMT in its proof. I saw some other examples which used zenon, SMT both. I am new to using the proving system so do not understand when to use SMT or Zenon in the proof.

I have also gone through the TLAPS tutorial example of GCD spec. Also, read about some of the limitations and unsupported features in TLAPS. Not sure if I have one of those in my proof.

I will appreciate it if someone could provide any insight or clarification that will help me with the proof.  



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/09339bc6-eea4-4480-a6ee-75567f92bb4an%40googlegroups.com.