5 ms·

How does Alloy compare to TLA+?

by teeray 4y ago

rsrsrs86 4y ago
Both can deal with time, but Alloy is a high level language to describe structures, their relationships, constraints and feels like writing SQL schemas and property tests. It is easy to use. With Alloy, you can very quickly iterate over software designs. TLA is more heavy weight and geared toward verifying concurrent systems, including algorithms and such. It is much harder to learn. With TLA, you can verify concurrent systems and algorithms.
hwayne 4y ago
Every time this comes up I promise myself I'll write a full post, and then I try to write a full post and give up 3000 words later. Here's my usual, now-about-two-years-out-of-date-spiel: ------- 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: Alloy6 added a notion of "time". This expands the space that Alloy can do, but the syntax is really footgun-heavy. If you forget to update a variable in TLA+, you get an error, if you forget to update in Alloy, it'll just assign whatever value it wants to that variable. I asked one of the developers and apparently it's not something they can easily address in the current semantics. Other problems are it can only check up to a given time-bound, which makes complex properties like liveness hard to check. The more “timelike” the problem gets, the worse Alloy becomes at handling it. Alloy also doesn't have composable collection types. You can model "a queue of messages", but you can't easily model "a queue of messages for each server". It's possible but you have to be clever, whereas in TLA+ it's straightforward. 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`. How many nodes is the shortest path? That’s much harder. 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 a strict division.
- deleted 4y ago
  [deleted]
- dgan 4y ago
  Thanks it's really hard to navigate among different available tools as a n00b; so that clears it out!
slaymaker1907 4y ago
Allow is very different in that it approaches things by converting whatever you are trying to verify into first order logical formulae then trying to find some model which violates the formula. This is undecidable in the general case, but Alloy works around this by limiting the domain to some finite size (so considering all possible sets below some size) in which case the problem is merely NP-complete and easily translated into SAT. Because Alloy works off of first order logic, it's a lot more general than TLA+ but doesn't have temporal logic concepts like liveness as first class primitives. You can still model most of this stuff in Alloy, but I think Alloy is really best for when you want to verify something which doesn't have a good model checker available or in problem spaces which easily reduce to first order logic.
- hwayne 4y ago
  > Because Alloy works off of first order logic, it's a lot more general than TLA+ but doesn't have temporal logic concepts like liveness as first class primitives. This is incorrect: TLA+ is also based off first-order logic constructs and can generally represent a much wider range of systems than Alloy can. The difference is that Alloy is more tractable: what it can represent it can model check much, much faster than TLA+.

How does Alloy compare to TLA+?

by teeray 4y ago

How does Alloy compare to TLA+?

Both can deal with time, but Alloy is a high level language to describe structures, their relationships, constraints and feels like writing SQL schemas and property tests. It is easy to use. With Alloy, you can very quickly iterate over software designs. TLA is more heavy weight and geared toward verifying concurrent systems, including algorithms and such. It is much harder to learn. With TLA, you can verify concurrent systems and algorithms.

hwayne 4y ago

Every time this comes up I promise myself I'll write a full post, and then I try to write a full post and give up 3000 words later. Here's my usual, now-about-two-years-out-of-date-spiel: ------- 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: Alloy6 added a notion of "time". This expands the space that Alloy can do, but the syntax is really footgun-heavy. If you forget to update a variable in TLA+, you get an error, if you forget to update in Alloy, it'll just assign whatever value it wants to that variable. I asked one of the developers and apparently it's not something they can easily address in the current semantics. Other problems are it can only check up to a given time-bound, which makes complex properties like liveness hard to check. The more “timelike” the problem gets, the worse Alloy becomes at handling it. Alloy also doesn't have composable collection types. You can model "a queue of messages", but you can't easily model "a queue of messages for each server". It's possible but you have to be clever, whereas in TLA+ it's straightforward. 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`. How many nodes is the shortest path? That’s much harder. 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 a strict division.

deleted 4y ago
[deleted]
dgan 4y ago
Thanks it's really hard to navigate among different available tools as a n00b; so that clears it out!

slaymaker1907 4y ago

Allow is very different in that it approaches things by converting whatever you are trying to verify into first order logical formulae then trying to find some model which violates the formula. This is undecidable in the general case, but Alloy works around this by limiting the domain to some finite size (so considering all possible sets below some size) in which case the problem is merely NP-complete and easily translated into SAT. Because Alloy works off of first order logic, it's a lot more general than TLA+ but doesn't have temporal logic concepts like liveness as first class primitives. You can still model most of this stuff in Alloy, but I think Alloy is really best for when you want to verify something which doesn't have a good model checker available or in problem spaces which easily reduce to first order logic.

hwayne 4y ago
> Because Alloy works off of first order logic, it's a lot more general than TLA+ but doesn't have temporal logic concepts like liveness as first class primitives. This is incorrect: TLA+ is also based off first-order logic constructs and can generally represent a much wider range of systems than Alloy can. The difference is that Alloy is more tractable: what it can represent it can model check much, much faster than TLA+.