3 ms·

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 t

by chrsig 4y ago

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.

mdaniel 4y ago
Did you already watch the linked video (https://news.ycombinator.com/item?id=35512991 https://news.ycombinator.com/item?id=35512991) and go through Alloy's tutorial? https://alloytools.org/tutorials/online/ 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?