Can TLAPS check any termination proofs?

[Lorin Hochstein <lor...@xxxxxxxxx>]

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