8 ms·
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 sy
by gralx 7y ago
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 agoYo, 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 https://lamport.azurewebsites.net/tla/book.html [2]: https://lamport.azurewebsites.net/tla/hyperbook.html 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 agoThanks, 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.