How does the Alloy Analyzer differ from model checkers?
The motivation for the Alloy project was to bring to Z-style specification the kind of automation offered by model checkers. The Alloy Analyzer is designed for analyzing state machines with operations over complex states. Model checkers are designed for analyzing state machines that are composed of several state machines running in parallel, each with relatively simple state. Alloy allows structural constraints on the state to be described very directly (with sets and relations), whereas most model checking languages provide only relatively low-level data types (such as arrays and records). The input languages of model checkers do not usually allow you to describe the state with the kinds of data structure easily handled by Alloy (tables, trees, etc); most require even simple data structures to be encoded using low-level primitives such as arrays and enumerations. Model checkers do a temporal analysis that compares a state machine to another machine or a temporal logic formula. The ter
