Linking Alloy with SMT-based Finite Model Finding

Abstract

Alloy is a well-known declarative language for modelling systems early in the development process. Currently, it uses the Kodkod library as its back-end for finite model finding (finding instances of the model by determining satisfiability for finite sets). Alloy's tool, the Alloy Analyzer, converts the Alloy model to an equivalent Kodkod problem, which is translated to boolean logic and analyzed using an off-the-shelf SAT solver by Kodkod. However, this method can often handle only problems of fairly small size sets.

We present Portus, a tool for translating Alloy into an equisatisfiable many-sorted finite model finding (MSFMF) problem of first-order logic. The MSFMF problem is evaluated by an SMT-based finite model finding method implemented in the Fortress solver, creating an alternative back-end to the Alloy Analyzer. Fortress converts the MSFMF problem into (mostly) the logic of equality with uninterpreted functions (EUF), a decidable fragment of first-order logic that is well-supported in many SMT solvers.

Portus is presented as a two-fold approach. First, we discuss the basic translation of all Alloy constructs in detail. Second, we suggest optimizations applicable to some Alloy models to improve the performance of Portus. We evaluate the effect of each optimization on Portus.

Finally, we compare the performance of Portus with Kodkod, the current solver of the Alloy Analyzer, on a corpus of Alloy models over various scopes. We classify these Alloy models based on certain characteristics and provide a hypothesis regarding the class of Alloy models Portus performs better on.