Hi Smruti,glad that you found my answer helpful. My replies are below.On 16 Nov 2020, at 20:38, Smruti Padhy <smruti...@xxxxxxxxx> wrote:Hi Stephan,Thank you so much for the detailed reply. It actually helped me a lot with the understanding of the proof. I have some follow up questions as well. I have added me comments and questions in-line with your reply message below:On Saturday, November 14, 2020 at 5:32:39 AM UTC-6 Stephan Merz wrote:Hello,apologies for the late reply – I tried to reconstruct your spec from what you pasted in the message but it may be a bit out of sync with the spec you are actually working on.Yes, I have attached the latest spec with the proofs.The first issue that I noticed was that your invariant mentions both constants MaxBufferLen and MaxTotalNumberOfItemsProduced but you only have an assumption for the first constant. So I added the conjunct/\ MaxTotalNumberOfItemsProduced \in Nat
to your constant assumption. Also, that assumption must of course be used in the proof but this is not shown in the proof that you reported being able to finish. Note that TLC will not help find you problems involving missing assumptions about constants because constants have fixed values in your model.Thanks for pointing that out. I completely missed that point. I have added that now.The second issue concerns the Consume action: it increments the variable num_of_items_consumed while leaving num_of_items_produced unchanged. Therefore you will not be able to conclude that the inequalitynum_of_items_consumed <= num_of_items_produced(which is your SafetyProperty) is preserved. This should have been discovered when you used TLC to check if your invariant was inductive. A minute of reflection indicates that the invariant that you really need isnum_of_items_consumed + Len(buffer) <= num_of_items_producedYes, while checking my previous SafetyProperty, TLC gave me an invariant violation error with a counter example. After some thought, I corrected my inductive invariant toSafetyProperty == num_of_items_produced = num_of_items_consumed + Len(buffer)
Is there a specific reason to use '<=' instead '=' ?
TLAPS is able to prove the inductive invariant with '='. Also as a system property, it seems num_of_items_consumed + Len(buffer) should always be equal to num_of_items_produced. Am I missing any counterexample?
Just after posting my reply, it occurred to me that I could have written '=' instead of '<=', and of course the version with equality is a stronger and more precise invariant, so it should be preferred. Both imply the original property that you stated.Now we can start the formal proof of the invariant, based on the general schema for invariant proofs. The only non-obvious step is the one that shows that [Next]_vars preserves the invariant, so I used the "decompose proof" command to split it into individual proof steps corresponding to the sub-actions of [Next]_vars. The cases corresponding to Produce and UNCHANGED vars are again simple, leaving us with the Consume action, which unfortunately isn't proved automatically. I now guessed that the prover needed to know that the length of the buffer decreases in this step and therefore asserted<3>. Len(buffer') = Len(buffer)-1Thank you so much. This was the key. I was stuck at trying to proof Consume action. This also clarifies some of the doubts I had.With this knowledge, the prover indeed managed to prove the step corresponding to the Consume action. (I could have split the conclusion IInv' into its individual conjuncts to find out which ones go through and which ones don't, further narrowing down the source of the problem.)For understanding how the TLAPS decompose proof works, I have decomposed the steps of the proof into several ways that TLAPS provides. In the updated spec attached, one can find the different decomposition and its proofs. As you have mentioned, I tried the proof decomposition by splitting IInv' to TypeInvariant' and SafetyProperty' (Proof Decomposition 3 in the spec). It is interesting to observe that TypeInvariant' and SafetyInvariant' could further be decomposed into CASE Produce, CASE Consume, CASE UNCHANGED vars. The step <2>1.<3>2 (CASE Consume) does not require the assert Len(buffer') = Len(buffer)-1 to prove TypeInvariant' while step <2>2.<3><2> requires it to prove SafetyProperty'.In Proof Decomposition 3', I tried to decompose proof for step <2>2.<3><2>, i.e CASE Consume, to proof SafetyProperty' without directly using Len(buffer') = Len(buffer)-1. The TLAPS decomposes it to further to CASE Produce, Consume, UNCHANGED vars. The same proof follows. It was like a cycle if we try to decompose Case Consume, it keeps decomposing it. I am not sure if that is the intended behaviour of TLAPS or some bug that I am seeing.When you use "decompose proof", the interface usually (depending on the shape of the formulas) offers you to work on either the hypotheses or the consequence of an assertion. I believe the reason for the behavior that you observed is that the assumption [Next]_vars is still present among the hypotheses, and since it is a disjunction, it can be decomposed. In contrast, the Consume action is a conjunction, and it doesn't make sense to decompose a conjunction in a hypothesis.For proving the auxiliary level-3 step, I use the lemma HeadTailProperties from the library module SequenceTheorems. (These modules are by default installed in /usr/local/lib/tlaps/, just like TLAPS.tla, it is worth looking at the theorems they provide if you are doing any non-trivial proof. You may also look at the proofs of these lemmas in SequenceTheorems_proofs.tla if you are stuck in some proof about sequences.)Thank you for letting me know about the Library modules. I tried the proof you had in the spec. TLAPS is able to proof auxiliary level-3 step with or without HeadTailProperties. Decomposition 1 in my updated spec (attached) is the exact proof that you had with HeadTailProperties and Decomposition 1' in the updated proof in the latest spec that is exactly the same proof as yours without HeadTailProperties. Am I missing something here?Indeed, the SMT backend knows enough about sequences to understand that the length of the tail is one less than the length of the original sequence, so appealing to lemma HeadTailProperties was not necessary here. Unfortunately, although the backend can prove that assertion when it is presented with it, it is not clever enough to replace Len(buffer') with Len(buffer)-1 on its own, and so the intermediate assertion has to be stated ...Happy proving,StephanI 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.----------------------------------------
THEOREM HeadTailProperties ==
ASSUME NEW S,
NEW s \in Seq(S), s # << >>
PROVE /\ Head(s) \in S
/\ Tail(s) \in Seq(S)
/\ Len(Tail(s)) = Len(s)-1
/\ \A i \in 1 .. Len(Tail(s)) : Tail(s)[i] = s[i+1]
OBVIOUS-----------------The overall module with the full proof is attached.Thank you again for the time and the detailed explanation and proof. It helped me a lot.Hope this helps,StephanP.S.: In a first approximation, you should not have to care about which backend (SMT, Zenon or Isabelle) proves any given step since TLAPS will call all of them. Adding "BY SMT" etc. to a step simply documents which backend succeeds in proving a step and avoids unnecessary calls to the other backends. -sThanks for the clarification.Best,Smrutips: When I attached the spec, I was getting error in posting. Also copying pasting here:. You can find the spec in our github repo: https://github.com/tapis-project/specifications/blob/master/generic-patterns/producer_consumer.tla------------------------- 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
--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/13d52375-2f27-4120-831e-867de5fae8a1n%40googlegroups.com.