Hacker News Reader

Comment by lukego | Hacker News Reader

I'd love to find a "bottom up" description of a language like TLA+. Start from the appropriate primitive (SAT solver? SMT solver?), show how to encode an example model directly, add layers of syntax etc as necessary for more complex examples.

I've watched all of Lamport's lectures but it really leaves me wondering what's happening under the hood: what are the primitives and how are TLA+ models mapped onto them.

(Lamport likes to say that TLA+ is just mathematics and imply that the engine underneath is not relevant but c'mon.)

View on HN

TLA+ is just a mathematical language; it doesn't do anything other than help you formally express the behaviour of discrete dynamical systems and write formal proofs of propositions about them. It was designed to be used with pen and paper, and often the greatest benefit comes from using it that way. Various automated tools -- two model checkers employing completely different algorithms and a proof assistant that also uses different technique to talk to different backends (SMT solvers, Isabelle, tableaux provers) -- were added much later, and at different times, and they each cover different subsets of the language. So the multitude of algorithms employed by the tools are not the primitives.

I've written a series of posts that covers the TLA+ theory (but it isn't a tutorial): https://pron.github.io/tlaplus

SAT and SMT solvers deal with propositional logic only. TLA+ is based on propositional logic with added modalities (i.e. what a type theorist would call monads) for "time" (in the temporal logic sense) and non-determinism. It is essentially a somewhat bespoke modal logic. Modal logics in general have lower expressive power than FOL, but are conversely more computationally tractable.

Just found the TLAPS Tactics page: https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...

Sounds like the first thing TLAPS does is to translate the TLA+ program into SMT and try to prove it with Z3. If that times out then it translates it into a couple of other kinds of provers before giving up (...).

Maybe I should look at how TLA+ "hello world" is compiled into SMT as a first step.

Depending on the problem that you are trying to solve with TLA+, you may prefer one encoding or another. For instance, here is one encoding for the proof system: https://hal.archives-ouvertes.fr/hal-01768750/. And here is another encoding for model checking: https://dl.acm.org/doi/10.1145/3360549

Direct link to the Apalache model checker: https://apalache.informal.systems/

I think you'd be better off starting with a simpler formalism for this, like Linear Temporal Logic. That's a good pick because there's a straightforward mapping to Büchi automata. This will give you some more intuition on model checking in general, but TLA+ is much more complex than LTL.

(The most popular model checker for TLA+, TLC, is a brute forcer that represents the state space as a directed graph. Lamport talks about it a bit in Specifying Systems.)

Reply on news.ycombinator.com