What kind of analysis does the Alloy Analyzer do?
The Alloy Analyzer is, technically speaking, a ‘model finder’. Given a logical formula (in Alloy), it attempts to find a model — a binding of the variables to values — that makes the formula true. For simulation, the formula will be some part of the system description. If it’s a state invariant INV, for example, models of INV will be states that satisfy the invariant. If it’s an operation OP, with variables representing the before and after states, models of OP will be legal state transitions. For checking, the formula is a negation, usually of an implication. To check that the system described by the property SYS has a property PROP, you would assert (SYS implies PROP); the Alloy Analyzer negates the assertion, and looks for a model of (SYS and not PROP), which, if found, will be a counterexample to the claim. Version 4.0 uses a new model finder engine called Kodkod and has a revised visualizer. Read more about it here. Version 3.0 improves on version 2.0 in a number of ways. Read m
