Interesting! We did something similar to this some years ago using answer-set programming (specifically Potassco) as the modeling language for checking properties of games like winnability instead. Kind of related but in a different direction, also to generate game levels meeting those properties rather than checking.
Seems like there are some similarities, e.g. ASP also compiles down to a finite SAT-like representation for solving (though it isn’t precisely SAT). But comes from a different historical background, out of logic programming rather than model-checking, and the modeling languages are as a result pretty different. Would be interesting to compare the strengths/weaknesses of Alloy vs. ASP for different kinds of game-modeling tasks.
edit: I vaguely remembered a Twitter discussion about Alloy/ASP relationship from my coauthor on that work, and dug it up but it’s pretty inconclusive.
The GDQ Link to the Past Randomizer (open world, swordless) race was my first exposure to the randomizer, and it blew me away. Hoping to learn it casually.
Alloy looks really cool, and much more approachable than other snippets and blog posts I’ve seen. Is it a good tool to start working with formal methods?
Short answer: probably, if you’re specifically interested in verifying specifications.
Long answer: it depends. There’s a lot of different fields in formal methods. You have verifying code matches a spec, you have refining specs into code, you have verifying the specs themselves, etc. Alloy is a tool in the latter category, and the other big players in that field are Z, Spin, and TLA+. Z is mostly out of favor and I thin Spin is too. In my opinion, TLA+ is orders of magnitude more powerful than Alloy but also much, much less user-friendly. Not necessarily harder to learn. Just, like, the tooling and UX actively hate you. That’s fixable in the long run, but in the short run, it puts up a lot of barriers that Alloy doesn’t have.
If you do decide to start with Alloy, Daniel Jackson’s Software abstractions is the best resource to learn.
Try to make notes about tooling problems you encountered. I want them in case I run into people wanting to do some work in formal methods that requires less specialist skill. UX and docs are often low-hanging fruit which your learntla.com illustrated on latter. I also saw it was on Java (right?) with a port to safe, portable, native code potentially being useful. I try to ditch anything with high TCB or close to Oracle’s lawyers.
Interesting! We did something similar to this some years ago using answer-set programming (specifically Potassco) as the modeling language for checking properties of games like winnability instead. Kind of related but in a different direction, also to generate game levels meeting those properties rather than checking.
Seems like there are some similarities, e.g. ASP also compiles down to a finite SAT-like representation for solving (though it isn’t precisely SAT). But comes from a different historical background, out of logic programming rather than model-checking, and the modeling languages are as a result pretty different. Would be interesting to compare the strengths/weaknesses of Alloy vs. ASP for different kinds of game-modeling tasks.
edit: I vaguely remembered a Twitter discussion about Alloy/ASP relationship from my coauthor on that work, and dug it up but it’s pretty inconclusive.
Good post, very clear explanations!
The GDQ Link to the Past Randomizer (open world, swordless) race was my first exposure to the randomizer, and it blew me away. Hoping to learn it casually.
Alloy looks really cool, and much more approachable than other snippets and blog posts I’ve seen. Is it a good tool to start working with formal methods?
Short answer: probably, if you’re specifically interested in verifying specifications.
Long answer: it depends. There’s a lot of different fields in formal methods. You have verifying code matches a spec, you have refining specs into code, you have verifying the specs themselves, etc. Alloy is a tool in the latter category, and the other big players in that field are Z, Spin, and TLA+. Z is mostly out of favor and I thin Spin is too. In my opinion, TLA+ is orders of magnitude more powerful than Alloy but also much, much less user-friendly. Not necessarily harder to learn. Just, like, the tooling and UX actively hate you. That’s fixable in the long run, but in the short run, it puts up a lot of barriers that Alloy doesn’t have.
If you do decide to start with Alloy, Daniel Jackson’s Software abstractions is the best resource to learn.
Try to make notes about tooling problems you encountered. I want them in case I run into people wanting to do some work in formal methods that requires less specialist skill. UX and docs are often low-hanging fruit which your learntla.com illustrated on latter. I also saw it was on Java (right?) with a port to safe, portable, native code potentially being useful. I try to ditch anything with high TCB or close to Oracle’s lawyers.