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

Hello,
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

<1> SUFFICES ASSUME Init

PROVE  IInv

OBVIOUS

<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'

<1> SUFFICES ASSUME IInv,

[Next]_vars

PROVE  IInv'

OBVIOUS

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

Produce(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.

Best,

Smruti

--
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.