Hacker News Reader

Does anyone know of a good hands on guide through learning how to use a model checker like alloy or tla+?

I see lots of value in adopting them, but the dsl's that they use are inscrutable to me. I'm sure that after some hands-on time I'd understand them well enough, but having a hard time figuring out how to get that ball rolling.

View on HN

Did you already watch the linked video (https://news.ycombinator.com/item?id=35512991) and go through Alloy's tutorial? https://alloytools.org/tutorials/online/

Based on the approach taken by the presenter from the video, I'd guess the "hands on" you're looking for is to take some API that you serve to others, internally or externally, and start writing down things you believe are invariant about it. Inputs must have a length greater than 1? Well, do all downstream systems also honor that invariant?

Reply on news.ycombinator.com