Cool, I haven’t heard much about Alloy in public use. It’s usually MiniZinc, TLA+, Coq, etc. I’ve done a little tinkering with Alloy, but I’m curious about other constraint systems or formal methods tools. Any lobsters have experience with Alloy or the others and can contrast/compare them?
Alloy isn’t comparable to MiniZinc because it’s not intended to be a constraint solver. While you can solve simple constraint problems, you don’t have any complex data structures (no matrices), it defaults to 4 bit integers, and it can’t express minimization or max criteria. For anything more than playing with proofs of concept you want to be using a dedicated tool. It also isn’t comparable to Coq, as its a specification language, not a theorem prover. It’s really best for high level specifications of complicated systems, which puts it in the same domain as TLA+ and SPIN. I don’t know SPIN, so will have to defer to Zave’s writing here, but I have experience in both TLA+ and Alloy so can compare them.
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 analyze, Lamport wanted maximal expressive power.
One consequence of this is that Alloy’s tooling and usability is light years ahead of TLA+. You can fit the entire syntax on a single sheet. Unlike TLA+, there’s no footguns in expressibility: it’s really hard to write a spec you can’t check with the tooling. 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. 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 unwieldy. 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? Still haven’t figured out how to do that.
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. I’m sorta working on a short primer to help address this.
I left it out because this is more akin to logic programming than formal methods in my mind. Maybe the distinction is artificial but formal methods in my opinion extends beyond just logic/relational programming because technically SQL would qualify as formal methods.
A while back I tried a similar thing, but instead of verification was trying synthesis. I wanted to see if I could get Alloy to generate a half-adder. You can see the solution I got, and the solution Daniel Jackson wrote, here.
Cool, I haven’t heard much about Alloy in public use. It’s usually MiniZinc, TLA+, Coq, etc. I’ve done a little tinkering with Alloy, but I’m curious about other constraint systems or formal methods tools. Any lobsters have experience with Alloy or the others and can contrast/compare them?
Alloy isn’t comparable to MiniZinc because it’s not intended to be a constraint solver. While you can solve simple constraint problems, you don’t have any complex data structures (no matrices), it defaults to 4 bit integers, and it can’t express minimization or max criteria. For anything more than playing with proofs of concept you want to be using a dedicated tool. It also isn’t comparable to Coq, as its a specification language, not a theorem prover. It’s really best for high level specifications of complicated systems, which puts it in the same domain as TLA+ and SPIN. I don’t know SPIN, so will have to defer to Zave’s writing here, but I have experience in both TLA+ and Alloy so can compare them.
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 analyze, Lamport wanted maximal expressive power.
One consequence of this is that Alloy’s tooling and usability is light years ahead of TLA+. You can fit the entire syntax on a single sheet. Unlike TLA+, there’s no footguns in expressibility: it’s really hard to write a spec you can’t check with the tooling. 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. 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 unwieldy. 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:
Is
N1connected toN2? Easy, just doN1 in N2^.edge. Through which nodes doesN1connect toN2? Still haven’t figured out how to do that.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. I’m sorta working on a short primer to help address this.
Thanks for taking the time to write such a detailed reply. I appreciate it!
There is also Picat but it’s more a programming language than a specification system.
Interesting that you omitted the formal methods tag. “If it works, it stops being AI.”
“If it enters common use, it stops being formal methods.”
I left it out because this is more akin to logic programming than formal methods in my mind. Maybe the distinction is artificial but formal methods in my opinion extends beyond just logic/relational programming because technically SQL would qualify as formal methods.
A while back I tried a similar thing, but instead of verification was trying synthesis. I wanted to see if I could get Alloy to generate a half-adder. You can see the solution I got, and the solution Daniel Jackson wrote, here.
This is cool. I didn’t think about synthesis at all but it makes sense. Synthesis is another constraint problem.