[ohpauleez]

Adding to what tel said:

Alloy will tell you where things are over or under-specified. You can ask the system to generate you scenarios in the "world" so you can see a graphical representation of states. You can test/check your assumptions or operating criteria against the structures/rules of the of the "world" and it'll find and show you counter-examples where things fail. I especially like working in Alloy because it's incremental and interactive, like a REPL for you design work, providing some of the benefits of property-based testing in the design portions of creating your system. Simply put: It helps you think through and explore your design!