Can TLAPS check any termination proofs?

[Lorin Hochstein]

Is TLAPS capable (yet?) of checking a proof that an algorithm terminates?

In particular, consider the following simple algorithm:

----------------------------- MODULE CountDown -----------------------------

EXTENDS Naturals

CONSTANT N

ASSUME N \in Nat

(*

--fair algorithm CountDown {

variable i = N;

{

 loop:

   while (i>0) {

     i := i-1

   }

}}

*)

\* BEGIN TRANSLATION

VARIABLES i, pc

vars == << i, pc >>

Init == /\ i = N

        /\ pc = "loop"

loop == /\ pc = "loop"

        /\ IF i>0

              THEN /\ i' = i-1

                   /\ pc' = "loop"

              ELSE /\ pc' = "Done"

                   /\ i' = i

Next == loop \/ (pc = "Done" /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars /\ WF_vars(Next)

Termination == <>(pc = "Done")

\* END TRANSLATION

THEOREM AlwaysTerminates == Spec => Termination

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

Is it possible today to write a structured proof of the theorem AlwaysTerminates in a way that can be checked with TLAPS?

Lorin

[Leslie Lamport]

TLAPS cannot yet do any non-propositional temporal logic reasoning.
It also cannot reason about ENABLED.  We hope to have liveness reasoning
implemented within two years.

However, TLA is designed to do as little temporal logic reasoning as
possible.  What you could do is write a liveness proof in TLA,
omitting the proofs of steps that involve temporal reasoning.  For a
complicated system, most of the steps would require reasoning at the
action level, which TLAPS has always been able to do.  You'd essentially
have to apply the TLA proof rules by hand.  Whether that would be useful
will depend on what you're trying to do.

Leslie