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
-------------------------------------------
In evaluation, the identifier buffer is either undefined or not an operator.
line 64, col 19 to line 64, col 24 of module BlockingQueue
-------------------------------------------
I am not sure what I am missing here.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.
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.
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_produced
SafetyProperty == 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?
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)-1
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 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.)
The overall module with the full proof is attached.
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. -s
------------------------- 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
On 16 Nov 2020, at 20:38, Smruti Padhy <smruti...@gmail.com> 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?
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.
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?
--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/13d52375-2f27-4120-831e-867de5fae8a1n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2c130114-1919-4a45-abf9-4690252a34e6n%40googlegroups.com.