[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 31 May 2024 14:05:00 +0200*References*: <7336ff89-595a-43ba-ba71-f373898da9e8@kit.edu>

Hi Matthias, that’s an interesting problem in that you’ve hit what appears to be a limitation of the "coalescing" technique that underlies the interplay of predicate logic and temporal logic reasoning in TLAPS. The problem is that you mix quantifier reasoning and temporal logic reasoning, and the bound of the quantifier is a state function, not a constant. Your theorem is correct because the domain of the sequence is in fact unchanged along the execution, but the prover doesn’t "see" this, and even if you add "UNCHANGED (DOMAIN States)" as a conjunct to the right-hand side of step <1>1 of your proof, the coalescing procedure is not smart enough to exploit this when pushing the quantifier over []. The workaround I suggest is to make the domain of the "States" function explicit, as in the module below. In the proof, step <1>2 introduces a constant for the bound variable and uses PTL to establish the property for that fixed constant i. Step <1>3 then introduces the quantifier, and coalescing knows that it may push the quantifier across [] as long as the domain of the quantifier is a constant. Best regards, Stephan -------------------------- MODULE TerminationSpec -------------------------- EXTENDS TLAPS CONSTANT Proc VARIABLE States Init == States \in [Proc -> {"INIT", "DONE"}] Terminate(i) == States' = [States EXCEPT ![i] = "DONE"] Next == \E i \in Proc : Terminate(i) Spec == Init /\ [][Next]_States HasTerminated(i) == States[i] = "DONE" THEOREM Spec => [](\A i \in Proc : HasTerminated(i) => [] HasTerminated(i)) \* Init is an invariant <1>1 Init /\ [Next]_States => Init' BY DEF Init, Next, Terminate \* Each step leaves terminated states unchanged <1>2 ASSUME NEW i \in Proc PROVE Spec => [](HasTerminated(i) => []HasTerminated(i)) <2>1 Init /\ [Next]_States /\ HasTerminated(i) => HasTerminated(i)' BY DEF Init, Next, Terminate, HasTerminated <2> QED BY <1>1, <2>1, PTL DEF Spec <1> QED BY <1>1, <1>2 ============================================================================= > On 31 May 2024, at 13:03, Grundmann, Matthias (KASTEL) <matthias.grundmann@xxxxxxx> wrote: > > Can the theorem in the following exemplary specification be proven in TLAPS? > > -------------------------- MODULE TerminationSpec -------------------------- > > EXTENDS Sequences, TLAPS > > VARIABLE States > Init == States \in Seq({"INIT", "DONE"}) > Terminate(i) == > States' = [States EXCEPT ![i] = "DONE"] > Next == \E i \in DOMAIN States : Terminate(i) > Spec == Init /\ [][Next]_States > > HasTerminated(i) == > States[i] = "DONE" > THEOREM Spec => [](\A i \in DOMAIN States : HasTerminated(i) => [] HasTerminated(i)) > > ============================================================================= > > The theorem should state that once a state has been set to "DONE", the state will always equal "DONE" (and never be reverted to "INIT"). Have I formalized this correctly? > > My attempt to prove the theorem follows. TLAPS successfully checks the steps <1>1 and <1>2 but not the QED step. > > THEOREM Spec => [](\A i \in DOMAIN States : HasTerminated(i) => [] HasTerminated(i)) > \* Init is an invariant > <1>1 Init /\ [Next]_States => Init' > BY DEF Init, Next, Terminate > \* Each step leaves terminated states unchanged > <1>2 Init /\ [Next]_States => \A i \in DOMAIN States : HasTerminated(i) => HasTerminated(i)' > BY DEF Init, Next, Terminate, HasTerminated > <1>3 QED > BY <1>1, <1>2, PTL DEF Spec, HasTerminated > > -- > 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. > To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7336ff89-595a-43ba-ba71-f373898da9e8%40kit.edu. -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/66A37E6A-7864-4EAF-AF7A-E31EE4D7C399%40gmail.com.

**Follow-Ups**:**Re: [tlaplus] Proving temporal property in TLAPS***From:*Grundmann, Matthias (KASTEL)

**References**:**[tlaplus] Proving temporal property in TLAPS***From:*Grundmann, Matthias (KASTEL)

- Prev by Date:
**[tlaplus] Proving temporal property in TLAPS** - Next by Date:
**Re: [tlaplus] Proving temporal property in TLAPS** - Previous by thread:
**[tlaplus] Proving temporal property in TLAPS** - Next by thread:
**Re: [tlaplus] Proving temporal property in TLAPS** - Index(es):