pron on TLA+: design, model, document, and verify concurrent systems

Comment on TLA+: design, model, document, and verify concurrent systems parent

First, just to be precise, system dynamics are specified in TLA+ with TLA, which is a linear-time temporal logic (albeit one that seeks to minimize temporal reasoning); set theory is used "only" for the data part.

Second, the whole point of a high-level specification is that it is not dependent on a programming language, and allows you to choose the level of detail that suits you. One of the things that set TLA+ apart is that it allows for very convenient refinements, i.e. you can specify the same system multiple times, at different levels of detail, and show that a more detailed specification indeed implements a more abstract one.

Perhaps looking at examples (which you can find on the subreddit I linked and in the sidebar) will give you a better feel for how TLA+ is used for precisely the goal you have in mind. The Practical TLA+ book[1] (which uses PlusCal) also has good examples.

[1]: https://www.apress.com/gp/book/9781484238288

gralx 7y

Fantastic, pron - thanks for the helpful replies.

I had a look at Practical TLA+ a few weeks back, but because its first example also specifies a concurrent system, and because most of it is written in PlusCal syntax, not in TLA+, I decided to put it off. I'll give it another look on your recommendation. I'll also check out the subreddit you linked to.

The idea of starting with a general high-level specification before adding detail makes a lot of sense.

As for specific problems, I have in mind a program that should be simple to specify. At its heart, it tests whether each numeric value in an input tuple X lies between values at the same index in tuples A and B, so that if

    ∀x ∈ X : a_i ∈ A ≤ x_i ≤ b_i ∈ B

then the program outputs "true", and otherwise the program outputs "false". Because both outputs are allowed,

    True ≜  ∧ ∀x ∈ X : ∧ x_i ≥ a_i ∈ A
                       ∧ x_i ≤ b_i ∈ B
            ∧ Output′ = true

    False ≜ ∧ ∃x ∈ X : ∨ x_i < a_i ∈ A
                       ∨ x_i > b_i ∈ B
            ∧ Output′ = false

covers all states. Some of my syntax is not TLA+, as you can see, so that's the specific problem I'm up against right now.

hwayne 7y

Yo, author of PT here. I'd say that given your use case, the book _probably_ won't be that useful to you. Among other things, I intentionally avoided teaching refinements. You'd probably be happier starting with either _Specifying Systems_[1] or the _Hyperbook_[2], particularly the latter's proof track.

If you still have access to a copy of PT, I'd recommend reading chapter 7 (specifying and implementing algorithms) to see if that helps at all. The code is in PlusCal, but the general approach transfers to pure TLA+.

[1]: https://lamport.azurewebsites.net/tla/book.html [2]: https://lamport.azurewebsites.net/tla/hyperbook.html

EDIT: in terms of writing it as TLA+, you probably want something like

    EXTENDS Sequences
    IndicesBetween(X, A, B) ==
      \A i \in 1..Len(X):
        /\ A[i] <= X[i]
        /\ B[i] >= X[i]

Assuming `Len(X) <= Min(Len(A), Len(B))`.

gralx 7y

Thanks, Hillel! The TLA+ formulation looks good. I was so happy to get your advice that I bought a copy of Practical TlA+ from Apress. Even if it doesn't help with this particular project, I'm sure it will be useful down the line.

Specifying Systems has been my go-to reference alongside Lamport's video tutorial. Thanks for suggesting Chapter 7 of the Hyperbook - I never thought to look there.

EDIT: I misread: Chapter 7 refers to the chapter in Practical TLA+, not to the Hyperbook's proof track.

Comments