3 ms·
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 rea
by pron 8y ago
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 https://www.apress.com/gp/book/9781484238288
- gralx 8y agoFantastic, 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 8y 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 8y 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.