I also looked into the proof of HeadTailProperties. I am not sure if I understand it correctly, the proof looks like it is stating the property of a sequence with its operators as the last step of the proof is OBVIOUS.
Thank you again for the time and the detailed explanation and proof. It helped me a lot.
Thanks for the clarification.
------------------------- MODULE producer_consumer -------------------------
EXTENDS Naturals, Sequences, SequenceTheorems, TLAPS
CONSTANTS MaxTotalNumberOfItemsProduced, (* max number of items that can be produced by a producer *)
MaxBufferLen (* max buffer capacity for produced items *)
ASSUME Assumption ==
/\ MaxTotalNumberOfItemsProduced \in Nat
/\ 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"}]
-----------------------------------------------------------------------------
(* Temporarl 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_produced = num_of_items_consumed + Len(buffer)
------------------------------------------------------------------------------
(* 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)
-------------------------------------------------------------------------------
(* Proof *)
(* ---- Proof structure ---- *)
(* ----
Correct = ... \* The invariant you really want to prove
IInv = ... /\ Correct \* the inductive invariant
THEOREM Spec=>[]Correct
<1>1. Init => IInv
<1>2. IInv /\ [Next]_vars => IInv'
<1>3. IInv => Correct
<1>4. QED
BY <1>1, <1>2, <1>3
------------------------ *)
(*---- Inductive Invariant -------*)
IInv == /\ TypeInvariant
/\ SafetyProperty
(* While checking for the inductive invariant in TLC , Seq operator needs to be redefine as MySeq. *)
MySeq(P) == UNION {[1..n -> P] : n \in 0..MaxBufferLen}
(* ---- Dr.Stephen's proof decomposition 1 ------- *)
THEOREM Spec => []IInv
<1>1. Init => IInv
BY Assumption DEF Init, IInv, TypeInvariant, SafetyProperty
<1>2. IInv /\ [Next]_vars => IInv'
<2> SUFFICES ASSUME IInv,
[Next]_vars
PROVE IInv'
OBVIOUS
<2>. USE Assumption DEF IInv, TypeInvariant, SafetyProperty
<2>1. ASSUME NEW item \in Item,
Produce(item)
PROVE IInv'
BY <2>1, Assumption DEF Produce
<2>2. CASE Consume
<3>. Len(buffer') = Len(buffer)-1
BY <2>2, HeadTailProperties DEF Consume
<3>. QED BY <2>2 DEF Consume
<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, PTL DEF Spec
(*------ Decomposition 1' ------ *)
(* Removed HeadTailProperties from the proof step <3>. in decomposition 1. TLAPS still able o prove it *)
THEOREM Spec => []IInv
<1>1. Init => IInv
BY Assumption DEF Init, IInv, TypeInvariant, SafetyProperty
<1>2. IInv /\ [Next]_vars => IInv'
<2> SUFFICES ASSUME IInv,
[Next]_vars
PROVE IInv'
OBVIOUS
<2>. USE Assumption DEF IInv, TypeInvariant, SafetyProperty
<2>1. ASSUME NEW item \in Item,
Produce(item)
PROVE IInv'
BY <2>1, Assumption DEF Produce
<2>2. CASE Consume
<3>. Len(buffer') = Len(buffer)-1
BY <2>2 DEF Consume
<3>. QED BY <2>2 DEF Consume
<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, PTL DEF Spec
(* ----- Proof Decomposition 2 ------- *)
(* Separately proved step 1 and step 2 of the proof as LEMMA. Then proved the fonal THEOREM. *)
LEMMA TypeCorrect == Init => IInv
<1> SUFFICES ASSUME Init
PROVE IInv
OBVIOUS
<1>1. TypeInvariant
BY Assumption DEF Init, IInv, TypeInvariant
<1>2. SafetyProperty
BY DEF Init, IInv, SafetyProperty
<1>3. QED
BY <1>1, <1>2 DEF IInv
(* Decompose proof into CASE Next, UNCHANGED vars. CASE Next is further decomposed into Produce, Consume, UNCHANGED *)
LEMMA SecondStep== IInv /\[Next]_vars => IInv'
<1> SUFFICES ASSUME IInv,
[Next]_vars
PROVE IInv'
OBVIOUS
<1>1. CASE Next
<2>. USE Assumption DEF IInv, TypeInvariant, SafetyProperty
<2>1. ASSUME NEW item \in Item,
Produce(item)
PROVE IInv'
BY <2>1, Assumption DEF Produce
<2>2. CASE Consume
<3>. Len(buffer') = Len(buffer)-1
BY <2>2 DEF Consume
<3>. QED BY <2>2 DEF Consume
<2>3. QED
BY <1>1, <2>1, <2>2 DEF Next
<1>2. CASE UNCHANGED vars
BY Assumption, <1>2 DEF vars, IInv, TypeInvariant, SafetyProperty
<1>3. QED
BY <1>1, <1>2
THEOREM Spec =>[]IInv
BY TypeCorrect, SecondStep, PTL DEF Spec
(* ----- Proof decomposition 3 ------- *)
(* Decomposed proof of <1>2 into individual conjunct of IInv', that is TypeInvariant' and SafetyProperty' *)
(* TypeInvariant' and SafetyInvariant' further decomposed into CASE Produce, CASE Consume, CASE UNCHANGED vars respectively.*)
(* It is interesting to see step <2>1.<3>2 does not require assert Len(buffer') = Len(buffer)-1 to prove TypeInvariant' *)
(* while step <2>2.<3><2> requires it to prove SafetyProperty'*)
THEOREM Spec => []IInv
<1>1. Init => IInv
BY Assumption DEF Init, IInv, TypeInvariant, SafetyProperty
<1>2. IInv /\ [Next]_vars => IInv'
<2> SUFFICES ASSUME IInv, [Next]_vars
PROVE IInv'
OBVIOUS
<2>1. TypeInvariant'
<3>1. ASSUME NEW item \in Item,
Produce(item)
PROVE TypeInvariant'
BY <3>1, Assumption DEF Produce, IInv, TypeInvariant, SafetyProperty
<3>2. CASE Consume
BY <3>2, Assumption DEF Consume, IInv, TypeInvariant, SafetyProperty
<3>3. CASE UNCHANGED vars
BY Assumption, <3>3 DEF vars, IInv, TypeInvariant, SafetyProperty
<3>4. QED
BY <3>1, <3>2, <3>3 DEF Next
<2>2. SafetyProperty'
<3>1. ASSUME NEW item \in Item,
Produce(item)
PROVE SafetyProperty'
BY <3>1, Assumption DEF Produce, IInv, TypeInvariant, SafetyProperty
<3>2. CASE Consume
<4>. Len(buffer') = Len(buffer)-1
BY <3>2 DEF Consume, IInv, TypeInvariant, SafetyProperty
<4>. QED BY <3>2 DEF Consume, IInv, TypeInvariant, SafetyProperty
<3>3. CASE UNCHANGED vars
BY Assumption, <3>3 DEF vars, IInv, TypeInvariant, SafetyProperty
<3>4. QED
BY <3>1, <3>2, <3>3 DEF Next
<2>3. QED
BY <2>1, <2>2 DEF IInv
<1>. QED BY <1>1, <1>2, PTL DEF Spec
(* ---- Proof Decomposition 3' --- Modification to the above proof decomposition 3 *)
(* When tried to decompose proof for the step <2>2.<3><2>, i.e CASE Consume to proof SafetyProperty', it decompose it to further to CASE Produce, Consume, UNCHANGED vars*)
THEOREM Spec => []IInv
<1>1. Init => IInv
BY Assumption DEF Init, IInv, TypeInvariant, SafetyProperty
<1>2. IInv /\ [Next]_vars => IInv'
<2> SUFFICES ASSUME IInv, [Next]_vars
PROVE IInv'
OBVIOUS
<2>1. TypeInvariant'
<3>1. ASSUME NEW item \in Item,
Produce(item)
PROVE TypeInvariant'
BY <3>1, Assumption DEF Produce, IInv, TypeInvariant, SafetyProperty
<3>2. CASE Consume
BY <3>2, Assumption DEF Consume, IInv, TypeInvariant, SafetyProperty
<3>3. CASE UNCHANGED vars
BY Assumption, <3>3 DEF vars, IInv, TypeInvariant, SafetyProperty
<3>4. QED
BY <3>1, <3>2, <3>3 DEF Next
<2>2. SafetyProperty'
<3>1. ASSUME NEW item \in Item,
Produce(item)
PROVE SafetyProperty'
BY <3>1, Assumption DEF Produce, IInv, TypeInvariant, SafetyProperty
<3>2. CASE Consume
<4>1. ASSUME NEW item \in Item,
Produce(item)
PROVE SafetyProperty'
BY <4>1, Assumption DEF Produce, IInv, TypeInvariant, SafetyProperty
<4>2. CASE Consume
<5>. Len(buffer') = Len(buffer)-1
BY <3>2, Assumption DEF Consume, IInv, TypeInvariant, SafetyProperty
<5>. QED BY <4>2 DEF Consume, IInv, TypeInvariant, SafetyProperty
<4>3. CASE UNCHANGED vars
BY <4>3 DEF vars, IInv, TypeInvariant, SafetyProperty
<4>4. QED
BY <4>1, <4>2, <4>3 DEF Next
<3>3. CASE UNCHANGED vars
BY Assumption, <3>3 DEF vars, IInv, TypeInvariant, SafetyProperty
<3>4. QED
BY <3>1, <3>2, <3>3 DEF Next
<2>3. QED
BY <2>1, <2>2 DEF IInv
<1>. QED BY <1>1, <1>2, PTL DEF Spec
=============================================================================
\* Modification History
\* Last modified Mon Nov 16 12:21:06 CST 2020 by spadhy
\* Created Mon Oct 26 10:27:47 CDT 2020 by spadhy