Proving temporal property in TLAPS

[Grundmann, Matthias (KASTEL)]

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

[Stephan Merz]

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

=============================================================================

> --
> 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/7336ff89-595a-43ba-ba71-f373898da9e8%40kit.edu.

[Grundmann, Matthias (KASTEL)]

Hi Stephan,

Thank you for the explanation which helped me to better comprehend how the prover approaches the proof.
The workaround to make the bound of the quantifier explicitly constant is quite clever!

Matthias