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.
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+.
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.
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
then the program outputs "true", and otherwise the program outputs "false". Because both outputs are allowed, 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.