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