
Research
Abstracts  2007 
Alloy Analyzer 4: Efficient Model Finder for FirstOrder LogicFelix Chang, Emina Torlak & Daniel JacksonIntroductionThe Alloy Analyzer is a model finder for analyzing models written in Alloy, a simple structural modeling language based on firstorder logic. The tool can generate instances of invariants, simulate the execution of operations, and check userspecified 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 outofdate 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 domainspecific idioms using Alloy 3 because its type system and module import semantics are not very flexible and extensible. ApproachThe new Alloy language is more more coherent and expressive:
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 onthefly. 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.
ResultsThe 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 backends. There are currently over 500 members in the Alloy discussion mailing list [3], and many active users beyond that. At least 30 nonMIT research papers are based on Alloy, and several research tools are built on top of the Alloy Analyzer [1] [2]. 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. Research SupportThis work is supported in part by the National Science Foundation (ITR Programme, Award 0541183), and by Nokia/MIT Collaboration. References[1] M.F. Frias, J.P. Galeotti, C.G.L. Pombo, N.M. Aguirre. DynAlloy: Upgrading Alloy with Actions. In The Proceedings of the 27th International Conference on Software Engineering, 2005. [2] W. Heaven, A. Russo. Enhancing the Alloy Analyzer with Patterns of Analysis. In The Proceedings of the 15th Workshop on Logic Programming Environments, Spain, 2005 [3] Alloy Specification Language & Analyzer discussion group. http://tech.groups.yahoo.com/group/alloydiscuss/ [4] The Alloy Analyzer Quick Guide. http://alloy.mit.edu/alloy4/quickguide/ [5] Accessing Alloy4 using Java API. http://alloy.mit.edu/alloy4/api.html 

