Our extensive industrial collaboration enables us to do research with immediate application to software development practices in realistic settings.
Solving Clafer Models with Choco
|Title||Solving Clafer Models with Choco|
|Year of Publication||2012|
|Series Title||Generative Software Development Laboratory|
|Document Number||GSDLab-TR 2012-12-30|
|Institution||University 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.