Principal Investigator Daniel Jackson
Project Website http://alloy.mit.edu/community/
The Alloy Analyzer is a model finder for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations, and check user-specified properties of a model. While the previous versions of the Alloy Analyzer have been used successfully in multiple domains, they have several deficiencies that are addressed by Alloy Analyzer 4.
First of all, Alloy 3 is a single monolithic application and cannot be easily extended to add new required features or be incorporated as part of a larger analysis framework.
Second of all, Alloy 3 uses out-of-date constraint generators and do not take advantage of new advances in effective use of SAT solver technology. It has a very limited implementation of sharing detection and symmetry breaking, and it does not take full advantage of partial instance knowledge in its formula generation.
Finally, it is awkward to model imperative constructs, object sequences, or other domain-specific idioms using Alloy 3 because its type system and module import semantics are not very flexible and extensible.
The new Alloy language is more coherent and expressive:
(1) it unifies treatment of relational expressions and function/predicate invocations;(2) it has built-in support for sequences;(3) it has better support for integers;(4) it has a more flexible type system which allows user-defined modeling idioms to simplify the task of writing the model.
Alloy 4 is modular and extensible. It has a core relational logic engine that incorporates new optimization techniques. The logic engine can be accessed in two ways: a compiler allows the model to be expressed in textual form, and a set of Java API methods that allow the model to be constructed, queried, and analyzed on-the-fly. If it is beneficial, additional interfaces can be easily written to integrate it into another analysis framework.
Finally, the Alloy Analyzer 4 has a clean separation between the Alloy relational logic and the underlying constraint solver Kodkod. Optimizations are performed first at the Alloy level, and the reduced problem is then given to Kodkod. This allows the developers of Kodkod to focus on developing a fast and efficient solver for general relational formulas without dealing with the complexity and semantics of Alloy. At the same time, the Alloy Analyzer 4 does not depend on Kodkod and can use other relational constraint solvers. This flexibility makes it possible for the Alloy Analyzer to make use of other solvers that may be better suited for specific problem domains.
The Alloy Analyzer 4 is written from scratch, and takes advantage of the new partial instance optimization capability in modern constraint solvers. It is currently based on the Kodkod model finder developed in MIT, but we are also exploring alternative translation back-ends.
There are currently over 500 members in the Alloy discussion mailing list, and many active users beyond that. At least 30 non-MIT research papers are based on Alloy, and several research tools are built on top of the Alloy Analyzer. The new Alloy Analyzer 4 is already used in at least 4 university courses on design modeling and discrete mathematics. Users at Airbus, AT&T, Telcordia, NASA Jet Propulsion Laboratory, Raytheon, World Wide Web Consortium, among others, are using the new Alloy Analyzer 4 for specific problems in their domain.