RE: [tlaplus] Dedalus versus TLA+

Dear Ovidiu,

I don’t have time to read about Dedalus. However, there are three significant errors in your email.

1. TLA+ was designed as a finite model checker

TLA+ is a language not a model checker. That language was designed without any thought of there being a model checker for it.

2. it provides evidence of correctness (up to 𝑘 steps of execution)

There are two model checkers for TLA+. Apalache is a symbolic model checker that checks executions of up to k steps. (It was first used a few years ago.) TLC is an explicit-state model checker with no such limitation. (It was first used around 2000.) It can check a finite-state model of a spec.

3. but no proofs.

The TLAPS proof checker for TLA+ was written around 2007.

Cheers,

Leslie Lamport

From: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> On Behalf Of ovidiu...@xxxxxxxxx
Sent: Sunday, June 16, 2024 23:55
To: tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Dedalus versus TLA+

You don't often get email from ovidiu21marcu@xxxxxxxxx. Learn why this is important

Hello,

Can you help with a dedalus versus tla+ comparison and any comment on the following: (from this paper https://dl.acm.org/doi/pdf/10.1145/3639257):

Section 6.3

We chose the Dedalus temporal logic language because it was both amenable to our optimization goals and we knew we could compile it to high-performance machine code via Hydroflow. Temporal logics have also been used for verification of protocols—most notably Lamport’s TLA+ language [44], which has been adopted in applied settings [50]. TLA+ did not suit our needs for a number of reasons. Most notably, efficient code generation is not a goal of the TLA+ toolchain. Second, an optimizer needs lightweight checks for properties (FDs, monotonicity) in the inner loop of optimization; TLA+ is ill-suited to that case. Finally, TLA+ was designed as a finite model checker: it provides evidence of correctness (up to 𝑘 steps of execution) but no proofs. There are efforts to build symbolic checkers for TLA+ [42], but again these do not seem well-suited to our lightweight setting.

Many thanks.

Ovidiu

--
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/1166e069-9bd7-4ff3-906d-3962512e6d7dn%40googlegroups.com.