5 ms·

> I think TLA+ is a great fit for what you want to do. I'm very happy to hear that. > What problems are you facing? Generally, the problem of formally specif

• pron 7y 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 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 ago
      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 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 ago
        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.
• sethwm 7y ago
  Have you looked at PlusCal [1][2]? It's more natural for many software developers and compiles down to TLA+. [1] https://en.wikipedia.org/wiki/PlusCal https://en.wikipedia.org/wiki/PlusCal [2] https://lamport.azurewebsites.net/tla/p-manual.pdf https://lamport.azurewebsites.net/tla/p-manual.pdf
  • gralx 7y ago
    Yes, I did. I prefer math/logic syntax, and I often like to work with pen and paper, and those are my main reasons for preferring TLA+ syntax over PlusCal. The author of Practical TLA+ says PlusCal is innately less expressive. Even so, pron elsewhere recommends reading Practical TLA+ for other reasons, so I think I'll learn PlusCal anyway. I appreciate the suggestion.
    • pron 7y ago
      I have mixed feelings about PlusCal. I, too, prefer TLA+ (except for low-level concurrent algorithms, or maybe algorithms best specified with long series of sequential steps), but for many programmers PlusCal can feel more familiar (which may be misleading; specification is not programming, and when you specify in TLA+ it also looks different from programming, but PlusCal looks a lot like programming, but it isn't). I think that those who are not threatened by mathematical notation should start with TLA+, and those who are should start with PlusCal. But there is value in the examples of specifications of the book regardless of the notation used. The central principles of specification are always the same.
      • hwayne 7y ago
        One of these days I gotta write an in-depth discussion of my teaching logic. The reasons I have for starting with PlusCal are fairly complex, and there are also disadvantages to it, too. But I still think that for many engineers, it's easier to learn PlusCal and then TLA+ than to go straight to TLA+.
        • tonyarkles 7y ago
• raister 7y ago
  Have you tried considering UPPAAL?
  • gralx 7y ago
    No - first I've heard of it. Just looked at its Wikipedia page. Color me intrigued.... Thank you!