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

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

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