News for hackers. Stuff that matters.

A comment on TLA+ model checking made symbolic. Parent comment

Re:TLA+ model checking made symbolic by QuinnWilton on Friday November 29, 2019 @03:31PM (#21666659)
You may have seen this blog already, but the author of "Practical TLA+" has a really fascinating blog with some fun toy examples. I'm a fan of this article where they model A Link to the Past with Alloy, to prove that dungeons are "winnable" [0].

The rest of the blog is really interesting too.

[0] https://www.hillelwayne.com/post/alloy-randomizer/

[ Parent | on HN ]
Re:TLA+ model checking made symbolic by hwayne on Friday November 29, 2019 @04:53PM (#21667035)
Feel free to throw an email my way (it's on the website) if you want to chat a bit more about potential use cases.
[ Parent | on HN ]