7 ms·

We use TLA+. There's nothing particularly magical about TLA+. There are a variety of modeling languages and model checking toolkits out there. I've yet to encou

We use TLA+. There's nothing particularly magical about TLA+. There are a variety of modeling languages and model checking toolkits out there. I've yet to encounter someone in industries that have commonly adopted model definition & checking who uses TLA+. It's popularity seems highest among folks in newer SaaS/IT arenas than elsewhere. More often I run into folks using SCADE's model checker. Tied for a distant 2nd, I'd say I've run into more folks who work with NuSMV, CADP, and mCRL2 than TLA+. This could also be mostly sample bias, and it's worth noting that the folks who use any of these things are in the very extreme minority of architects & developers that I speak to in automotive, med. tech., industrial automation, etc. Though, like I said, we use TLA+. Not for any particularly good reason than it was a sufficient tool among the variety of comparable tools for what we needed to do, but I expect that if we had to go back and do it all over again we'd have selected something else. The specification language has some annoying warts, the checking performance isn't comparatively very good, and the provided IDE works in almost exactly the opposite way any of us wish it would work. To the point that one of our engineers figured out how to wire it all up through Emacs so we could stop monkeying around with TLA Toolbox for 90% of the work. Of course, everything has problems, so TLA+ isn't notoriously different here. We've just used it in anger more than other things. For whatever it's worth, I also used to be an Erlang developer and used to play around a bit with McErlang, which I think might be a dead project now. However, there's an active project called Concuerror (https://concuerror.com/ https://concuerror.com/) which kind of covers the same domain. I don't know how well it works or what its level of maturity is, but it is very interesting in this one very important regard... it's model checking against your actual program implementation. That's an enormous and fantastic difference. Model conformance of concrete implementation to your design (and checked) model is an enormous problem, and tools which can close or remove that gap can be enormously valuable. What I don't know is the level of sophistication of Concuerror, nor if it is able to check for the kinds of properties you care about in your systems.

QuinnWilton 7y ago
Concuerror is a very cool tool! I've been very impressed with some of the bugs I've seen it detect. It's definitely a tool I'd like to make more use of. Thanks for the insightful comment, it's given me a lot of things to research!
spenuke 7y ago
Did you all ever open source your emacs tooling? I’d like to see that.
- im_down_w_otp 7y ago
  We didn't. It's on our list of things to open source and write about though, so we will when time permits. Probably won't be until after the new year, as we're focused on preparing for CES.
pron 7y ago
TLA+'s secret power is refinement; the entire logic is built around the abstraction/refinement relation. One of the best ways to use TLA+ is to specify you system in two or three levels of detail and check that they are, indeed, refinements. If you just use TLA+ for model-checking and don't use refinement mappings that are possible due to the language's elegance, you're giving up on most of its power, and if that's the case, you might as well use weaker specification languages like Promella and NuSMV. But I think it's worthwhile to learn how to use refinements and enjoy the full power of TLA+ rather than just as a language for model-checking. Unlike Promella and NuSMV, TLA+ is not designed as a frontend language for a model-checker. It's a language primarily designed to allow you to think about and understand your system in interesting ways, and it also has a model checker. It's designed to be read and discussed (hence the emphasis on pretty-printing) much more than written and edited. If you're using it anyway, make the full use of it.
- deleted 7y ago
  [deleted]
- hwayne 7y ago
  I'm now _really_ curious as to how many people who use and value TLA+ have actually used refinement. I've used it, you've used it, Lamport and (probs) Merz and Markus have used it, most other people I've talked to haven't. Probably time for a community poll or something.
  - pron 7y ago
    Technically it's impossible to use TLA+ without using refinement, as the entire TLA logic is based on it. Checking Machine ⇒ □P is checking that Machine refines □P. But, of course, the real power -- and what you and I both meant -- comes from writing machine formulas on both sides of the implication sign. I don't think many of those who use TLA+ use refinement between two machine formulas, but I think that's partly because they still consider TLA+ as a frontend language for TLC, which is unfortunate, because if all you want (or, rather, think you want) is a model-checker, there are probably better ones. In fact, the little use of refinement is just a symptom of this bigger issue. I don't think refinement is always useful, but I do think that everyone who uses TLA+ should use its power for analysis rather than just mundane model-checking. I admit, TLC is so enticing, that once you use it, TLA+ can feel secondary to it. Of course, I'd be happy if people used model-checkers more, whether TLC, Spin, NuSMV, Simulink or others, but I'd be even happier if people used TLA+ for its primary purpose, perhaps after being enticed by TLC: thinking about system design. I guess the problem is exactly what Lamport pointed out: programmers (including myself) don't like to think, especially when we can use automation. To be honest, I don't think I would have come to TLA+ if it weren't for TLC. So, in a sense, TLC both pulls people to TLA+ and obscures its main purpose. In the TLA+ workshop I imagine one day giving to my colleagues, I start with refinement. I would also start without TLC at all; just showing how TLA+ helps you think -- its main purpose and advantage. When writing specifications, I now always start with refinement, first writing how the system would behave at a very high-level, and only then refining a specific algorithm. (If anyone reads this without having read the article, and doesn't know what TLC is, it's a model-checker for TLA+ that's included in the TLA+ Toolbox)
lemmster 7y ago
Did you also wire up trace expression evaluation in Emacs?

QuinnWilton 7y ago

Concuerror is a very cool tool! I've been very impressed with some of the bugs I've seen it detect. It's definitely a tool I'd like to make more use of. Thanks for the insightful comment, it's given me a lot of things to research!

spenuke 7y ago

Did you all ever open source your emacs tooling? I’d like to see that.

im_down_w_otp 7y ago
We didn't. It's on our list of things to open source and write about though, so we will when time permits. Probably won't be until after the new year, as we're focused on preparing for CES.

pron 7y ago

TLA+'s secret power is refinement; the entire logic is built around the abstraction/refinement relation. One of the best ways to use TLA+ is to specify you system in two or three levels of detail and check that they are, indeed, refinements. If you just use TLA+ for model-checking and don't use refinement mappings that are possible due to the language's elegance, you're giving up on most of its power, and if that's the case, you might as well use weaker specification languages like Promella and NuSMV. But I think it's worthwhile to learn how to use refinements and enjoy the full power of TLA+ rather than just as a language for model-checking. Unlike Promella and NuSMV, TLA+ is not designed as a frontend language for a model-checker. It's a language primarily designed to allow you to think about and understand your system in interesting ways, and it also has a model checker. It's designed to be read and discussed (hence the emphasis on pretty-printing) much more than written and edited. If you're using it anyway, make the full use of it.

deleted 7y ago
[deleted]
hwayne 7y ago
I'm now _really_ curious as to how many people who use and value TLA+ have actually used refinement. I've used it, you've used it, Lamport and (probs) Merz and Markus have used it, most other people I've talked to haven't. Probably time for a community poll or something.
- pron 7y ago
  Technically it's impossible to use TLA+ without using refinement, as the entire TLA logic is based on it. Checking Machine ⇒ □P is checking that Machine refines □P. But, of course, the real power -- and what you and I both meant -- comes from writing machine formulas on both sides of the implication sign. I don't think many of those who use TLA+ use refinement between two machine formulas, but I think that's partly because they still consider TLA+ as a frontend language for TLC, which is unfortunate, because if all you want (or, rather, think you want) is a model-checker, there are probably better ones. In fact, the little use of refinement is just a symptom of this bigger issue. I don't think refinement is always useful, but I do think that everyone who uses TLA+ should use its power for analysis rather than just mundane model-checking. I admit, TLC is so enticing, that once you use it, TLA+ can feel secondary to it. Of course, I'd be happy if people used model-checkers more, whether TLC, Spin, NuSMV, Simulink or others, but I'd be even happier if people used TLA+ for its primary purpose, perhaps after being enticed by TLC: thinking about system design. I guess the problem is exactly what Lamport pointed out: programmers (including myself) don't like to think, especially when we can use automation. To be honest, I don't think I would have come to TLA+ if it weren't for TLC. So, in a sense, TLC both pulls people to TLA+ and obscures its main purpose. In the TLA+ workshop I imagine one day giving to my colleagues, I start with refinement. I would also start without TLC at all; just showing how TLA+ helps you think -- its main purpose and advantage. When writing specifications, I now always start with refinement, first writing how the system would behave at a very high-level, and only then refining a specific algorithm. (If anyone reads this without having read the article, and doesn't know what TLC is, it's a model-checker for TLA+ that's included in the TLA+ Toolbox)

lemmster 7y ago

Did you also wire up trace expression evaluation in Emacs?