Solving Clafer Models with Choco

TitleSolving Clafer Models with Choco
Publication TypeReport
Year of Publication2012
AuthorsLiang, J.
Series TitleGenerative Software Development Laboratory
Document NumberGSDLab-TR 2012-12-30
Date Published12/2012
InstitutionUniversity of Waterloo

The Clafer modelling language relies on Alloy as its back-end solver. Although Alloy is a good target language for the Clafer compiler because of the strong similarities between the two languages, it suffers in the presence of large integers. This paper explains the implementation of a new Clafer solver based on the Java constraint programming library called Choco. The solver needs to capture the semantics of the language including the hierarchy structure, type inheritance, references, primitives, and constraints. Performance of the solvers is the main metric for comparison.

Refereed DesignationNon-Refereed
2012-liang-choco.pdf254.47 KB