TLA+ model checking made symbolic

Re:TLA+ model checking made symbolic by RBerenguel on Friday November 29, 2019 @05:19AM (#21663449)

I've written some models for "personal use and validation", and I keep it in my toolbelt (with Alloy) in case my thinking is not clear about something

[ Parent | on HN ]

Re:TLA+ model checking made symbolic by kachnuv_ocasek on Friday November 29, 2019 @06:10AM (#21663640)

Could you briefly describe some of the models you played with? It seems cool that someone just specified models and verifies them in their spare time.

[ Parent | on HN ]

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 ]

Re:TLA+ model checking made symbolic by RBerenguel on Saturday November 30, 2019 @07:56AM (#21669760)

My spare time is kind of... weird. They were related to concurrency in an actor system, I validated a design and implementation (can’t share much more). I recommend checking Hillel’s blog as suggested, he has excellent examples (and his book is a good starting point for TLA+ and Pluscal as well)

[ Parent | on HN ]