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

[tlaplus] Proving temporal property in TLAPS

Can the theorem in the following exemplary specification be proven in TLAPS?

-------------------------- MODULE TerminationSpec --------------------------


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