5 ms·

Does anyone know how this compares to TLA+? Pros, cons, differences?

mcguire 7y ago
They're both model checkers. Alloy had a better "programming language", to me. TLA+ is more aggressive about being untyped, IIRC.
RockmanX 7y ago
the point I like Alloy is that it allows you to express something like "forall function f such that f is well-define ...", very cool. I barely know anything about TLA+ though.
hcs 7y ago
Perhaps best answered by: http://alloytools.org/faq/how_does_the_alloy_analyzer_differ_from_model_checkers.html http://alloytools.org/faq/how_does_the_alloy_analyzer_differ... It's more about data structures and testing every variation up to a fixed maximum size.
- hwayne 7y ago
  It's worth pointing out that Jackson wasn't specifically thinking of TLA+ when he wrote that. In _Software Abstractions_ he compares Alloy to B, OCL, VDM, and Z. TLA+ is very different from all of those, just as Alloy is. At some point in the future I'm supposed to write an in-depth comparison, though documentation work is higher priority right now.
  - hcs 7y ago
    Thanks! I've only really been through the tutorials of each, I'm glad to read about your experience upthread.
hwayne 7y ago
Alloy comes from the Z line of “systems are basically giant relational algebra problems”, while TLA+ comes from the LTL line of “systems are basically giant temporal logic problems”, which leads to a lot of fundamental differences between them. They also had different design philosophies: Jackson wanted a language that was easy to build tooling for, Lamport wanted a language that was easy to express complex logic in. One consequence of this is that Alloy is a much smaller language: you can fit the entire syntax on a single sheet. It's also much easier in TLA+ to write a spec that you can't model-check, while with Alloy you have to be actively trying. It’s also impossible to write an unbound model in Alloy, so you’re guaranteed that every spec is over a finite state space. Which gets rid of the common TLA+ runtime problem of “is this taking a long time because it’s a big state space or because it’s an infinite state space". Re tooling: Alloy converts to SAT, which makes model checking much, much faster. Specs that would take minutes to check in TLA+ take less than a second in Alloy. Being able to model-find as well as model-check is really nice, as is the ability to generate multiple counter/examples. The visualizer is really useful, too, especially for showing counterexamples to nontech folk. But the thing I honestly miss most when working in TLA+ is the REPL. It’s not the best REPL, but it’s a hell of a lot better than no REPL. Okay, so drawbacks: Alloy doesn’t have an inbuilt notion of time. You have to add it in as a sequence sig. This means you can’t study liveness properties or deadlocks or anything like that. It also makes simulating concurrency awkward. This isn’t a huge problem if you have simple interactions or only one structure that’s changing, but the more “timelike” the problem gets, the worse Alloy becomes at handling it. Less fundamental but still a big problem I keep having: no good iteration or recursion. Transitive closure is pretty nice but it’s not powerful enough. For example: sig node {edge: set Node} Is N1 connected to N2? Easy, just do `N1 in N2^.edge`. Through which nodes does N1 connect to N2? That's much harder. The biggest problem with Alloy adoption, though, is social: there’s no comprehensive online documentation. If you want to learn it you have to buy _Software Abstractions_. Fantastic book but not something that’s especially convenient, and it doesn't cover newer features. We're working on changing this, but it will be a while before we have comprehensive online documentation available. Which one is more appropriate to use really depends on your problem. As a very, very, VERY rough rule of thumb: TLA+ is best you're most interested in the dynamics of a system: the algorithms, the concurrency, etc. Alloy is best when you're most interested in the statics of a system: the requirements, the data relationships, the ontology, etc. My standard demos for showcasing TLA+ are concurrent transfers and trading platforms, while my standard demos for Alloy are access policies and itemized billing. You can use each in the other's niche, too (see Zave's work on Chord), so it's not a stark division.
- all2 7y ago
  This is fascinating to me. Do you have demos in a public place so I can take a look?
- ohpauleez 7y ago
  This largely sums up my experience with Alloy and TLA+, as well as when I favor using one tool over the other. My formal education included classes in Z, so the spirit of Alloy always made sense to me and it's usually the tool I start with (I tend to see systems problems as relations, the tooling is fantastic, the REPL is very useful, counter-examples help illuminate the problem space, etc.) When my problem is strictly algorithmic or it's all about the evolution of state spaces over time (especially concurrent states over time), I lean towards TLA+. When my problem is strictly a state machine, I usually write out some combination of a Parnas table and a statechart, and then encode the table into Alloy. I have a little tutorial I use to teach teammates the basics of TLA+ and Alloy, which takes about two hours to get through. I find that within a week of using Alloy, folks are dangerous enough to get value out of it.
  - jplane 7y ago
    Is the "little tutorial" available somewhere? I'd be interested in working through it.

They're both model checkers. Alloy had a better "programming language", to me. TLA+ is more aggressive about being untyped, IIRC.

RockmanX 7y ago

the point I like Alloy is that it allows you to express something like "forall function f such that f is well-define ...", very cool. I barely know anything about TLA+ though.

hcs 7y ago

Perhaps best answered by: http://alloytools.org/faq/how_does_the_alloy_analyzer_differ_from_model_checkers.html http://alloytools.org/faq/how_does_the_alloy_analyzer_differ... It's more about data structures and testing every variation up to a fixed maximum size.

hwayne 7y ago
It's worth pointing out that Jackson wasn't specifically thinking of TLA+ when he wrote that. In _Software Abstractions_ he compares Alloy to B, OCL, VDM, and Z. TLA+ is very different from all of those, just as Alloy is. At some point in the future I'm supposed to write an in-depth comparison, though documentation work is higher priority right now.
- hcs 7y ago
  Thanks! I've only really been through the tutorials of each, I'm glad to read about your experience upthread.

hwayne 7y ago

Alloy comes from the Z line of “systems are basically giant relational algebra problems”, while TLA+ comes from the LTL line of “systems are basically giant temporal logic problems”, which leads to a lot of fundamental differences between them. They also had different design philosophies: Jackson wanted a language that was easy to build tooling for, Lamport wanted a language that was easy to express complex logic in. One consequence of this is that Alloy is a much smaller language: you can fit the entire syntax on a single sheet. It's also much easier in TLA+ to write a spec that you can't model-check, while with Alloy you have to be actively trying. It’s also impossible to write an unbound model in Alloy, so you’re guaranteed that every spec is over a finite state space. Which gets rid of the common TLA+ runtime problem of “is this taking a long time because it’s a big state space or because it’s an infinite state space". Re tooling: Alloy converts to SAT, which makes model checking much, much faster. Specs that would take minutes to check in TLA+ take less than a second in Alloy. Being able to model-find as well as model-check is really nice, as is the ability to generate multiple counter/examples. The visualizer is really useful, too, especially for showing counterexamples to nontech folk. But the thing I honestly miss most when working in TLA+ is the REPL. It’s not the best REPL, but it’s a hell of a lot better than no REPL. Okay, so drawbacks: Alloy doesn’t have an inbuilt notion of time. You have to add it in as a sequence sig. This means you can’t study liveness properties or deadlocks or anything like that. It also makes simulating concurrency awkward. This isn’t a huge problem if you have simple interactions or only one structure that’s changing, but the more “timelike” the problem gets, the worse Alloy becomes at handling it. Less fundamental but still a big problem I keep having: no good iteration or recursion. Transitive closure is pretty nice but it’s not powerful enough. For example: sig node {edge: set Node} Is N1 connected to N2? Easy, just do `N1 in N2^.edge`. Through which nodes does N1 connect to N2? That's much harder. The biggest problem with Alloy adoption, though, is social: there’s no comprehensive online documentation. If you want to learn it you have to buy _Software Abstractions_. Fantastic book but not something that’s especially convenient, and it doesn't cover newer features. We're working on changing this, but it will be a while before we have comprehensive online documentation available. Which one is more appropriate to use really depends on your problem. As a very, very, VERY rough rule of thumb: TLA+ is best you're most interested in the dynamics of a system: the algorithms, the concurrency, etc. Alloy is best when you're most interested in the statics of a system: the requirements, the data relationships, the ontology, etc. My standard demos for showcasing TLA+ are concurrent transfers and trading platforms, while my standard demos for Alloy are access policies and itemized billing. You can use each in the other's niche, too (see Zave's work on Chord), so it's not a stark division.

all2 7y ago
This is fascinating to me. Do you have demos in a public place so I can take a look?
ohpauleez 7y ago
This largely sums up my experience with Alloy and TLA+, as well as when I favor using one tool over the other. My formal education included classes in Z, so the spirit of Alloy always made sense to me and it's usually the tool I start with (I tend to see systems problems as relations, the tooling is fantastic, the REPL is very useful, counter-examples help illuminate the problem space, etc.) When my problem is strictly algorithmic or it's all about the evolution of state spaces over time (especially concurrent states over time), I lean towards TLA+. When my problem is strictly a state machine, I usually write out some combination of a Parnas table and a statechart, and then encode the table into Alloy. I have a little tutorial I use to teach teammates the basics of TLA+ and Alloy, which takes about two hours to get through. I find that within a week of using Alloy, folks are dangerous enough to get value out of it.
- jplane 7y ago
  Is the "little tutorial" available somewhere? I'd be interested in working through it.