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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Fri, 18 Jan 2019 19:20:29 -0800 (PST)*References*: <b04580ad-cff7-4bc4-8de3-e7e81a7360d4@googlegroups.com>

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

On Friday, January 18, 2019 at 7:04:02 PM UTC-8, Lorin Hochstein wrote:

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

On Friday, January 18, 2019 at 7:04:02 PM UTC-8, Lorin Hochstein wrote:

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

**References**:**Can TLAPS check any termination proofs?***From:*Lorin Hochstein

- Prev by Date:
**Can TLAPS check any termination proofs?** - Next by Date:
**Help with running TLC in distributed mode (ad hoc)** - Previous by thread:
**Can TLAPS check any termination proofs?** - Next by thread:
**Help with running TLC in distributed mode (ad hoc)** - Index(es):