3 ms·

It would not be very difficult to get a working understanding of TLA+. You can separate the language into two parts - specifying safety, and specifying liveness

by ahelwer 12y ago

It would not be very difficult to get a working understanding of TLA+. You can separate the language into two parts - specifying safety, and specifying liveness. Safety is the easy one, and with knowledge of basic predicate logic and set operations you can have a logic puzzle spec written within hours. Specifying liveness is more difficult, since it involves temporal logic and other things I didn't cover in my degree. However, Lamport says (and I've found) 95% of specs will only need boilerplate temporal logic, so don't worry about it. I taught myself through the book Specifying Systems, although Lamport now recommends the TLA+ Hyperbook. Teaching yourself TLA+ then applying it to a work project to demonstrate its value to management is a good strategy. That is the approach I took, and having a concrete project to motivate study of TLA+ is very effective.

Jtsummers 12y ago
Thanks for the feedback. I'll read/work through the tutorials and Hyperbook, I've also downloaded Specifying Systems. Hopefully I have as much time as I think I do coming up. Another question, it seems they have a strong push to use the software tools (makes sense). A lot of the time that I'll have for this will be away from home, but not particularly busy (I tend to show up to places early so I often spend up to an hour at a bar/restaurant reading a book before friends arrive). In your opinion, would it be best for me to drag my laptop with me, or could I do a fair amount with paper and pencil and put it into the computer later?
- ahelwer 12y ago
  Paper and pencil should be enough. The syntactic analyzer is nice to have but Lamport really pushes the value of writing down your thoughts in formal logic, as an act. Model checking isn't something you do iteratively - by the time you have a spec amenable to model checking, you'll pretty convinced it's correct. Mostly, model checking will catch errors where you didn't accurately translate your thoughts to TLA+.

by ahelwer 12y ago

Jtsummers 12y ago

Thanks for the feedback. I'll read/work through the tutorials and Hyperbook, I've also downloaded Specifying Systems. Hopefully I have as much time as I think I do coming up. Another question, it seems they have a strong push to use the software tools (makes sense). A lot of the time that I'll have for this will be away from home, but not particularly busy (I tend to show up to places early so I often spend up to an hour at a bar/restaurant reading a book before friends arrive). In your opinion, would it be best for me to drag my laptop with me, or could I do a fair amount with paper and pencil and put it into the computer later?

ahelwer 12y ago
Paper and pencil should be enough. The syntactic analyzer is nice to have but Lamport really pushes the value of writing down your thoughts in formal logic, as an act. Model checking isn't something you do iteratively - by the time you have a spec amenable to model checking, you'll pretty convinced it's correct. Mostly, model checking will catch errors where you didn't accurately translate your thoughts to TLA+.