[tlaplus] Proving temporal property in TLAPS

• From: "Grundmann, Matthias (KASTEL)" <matthias.grundmann@xxxxxxx>
• Date: Fri, 31 May 2024 13:03:00 +0200
• User-agent: Mozilla Thunderbird

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.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature