OCLsolve — a Constraint Solver for UML/OCL

OCLsolve is a Java library for solving constraints expressed in UML/OCL. OCL (Object Constraint Language) is a textual language extending UML.

OCLsolve aims to solve constraints as efficiently as possible, and to provide support for a comprehensive set of UML/OCL language features. See the API for a description of the supported language features. Support for some features like Tuple types would have been feasible, but were not implemented due to lack of resources.

OCLsolve is not bound to a particular representation of the UML/OCL model.

This library has not been tested systematically, and is therefore likely to still contain major bugs. It is intended to demonstrate the feasibility of solving constraints expressed in UML/OCL.

Architecture and System Requirements

OCLsolve works by expressing the UML/OCL constraint as a Boolean satisfiability (SAT) problem, and solving the resulting SAT problem with an off-the-shelf SAT solver. The library can use the Java SAT4J solver and also ships with a Linux x86 binary of the MiniSat solver which allows improved performance on systems that can execute this binary. Note that supporting the SAT4J solver makes OCLsolve executable on any Java virtual machine. OCLsolve reuses some code from the Kodkod solver for interfacing with the SAT solvers.


oclsolve.jarPlain JAR containing OCLsolve
oclsolve-2013-01-28.zipZip of the JAR, the SAT4J solver library, the Javadoc and the example below


Some documentation can be found in the Javadoc.


Below is a simple example of calling OCLsolve for solving the OCL constraint set->includesAll(subset) and subset->sum() <= n. Here set and subset are variables holding a value of OCL type Set, while n holds an integer. Furthermore, we specify that the solver should maximize the value of the expression subset->sum(). For testing, we assign the value {1,2,8} to set and 4 to n.

import krieger.oclsolve.*; public class Example { public static void main(String[] args) { // We do not define any classes in this example. // (We stick to the primitive types and the OCL standard library types.) ClassTranslatorBase<Class<?>, String> classTranslator = new ClassTranslatorBase<Class<?>, String>(); // We use 32 bits for integers // (the "String" type parameter denotes a type used for identifying classes). ClassifierFactory<String> classifierFactory = classTranslator.createClassifierFactory(32); // We obtain an object representing the type of plain integers. // The multiplicity passed indicates that null values are allowed. Classifier<?> intType = classifierFactory.getIntegerType(new Multiplicity(0,1,false,false)); // We obtain an object representing the type of integer sets. // The multiplicity passed describes an unordered collection // of unbounded size containing unique elements. Classifier<?> intSet = classifierFactory.getIntegerType(new Multiplicity(0,-1,false,true)); // We define variables for holding the set, the subset, // and the value of the subset sum. Constant<?> set = intSet.newConstant(); Variable<?> subset = intSet.newVariable(); Constant<?> n = intType.newConstant(); // We start defining the constraint satisfaction problem. Problem problem = new Problem(); SetExpression setExpr = (SetExpression) set.getExpression(); SetExpression subsetExpr = (SetExpression) subset.getExpression(); IntegerExpression nExpr = (IntegerExpression) n.getExpression(); // The set must include all elements of the subset. // In OCL: set->includesAll(subset) problem.addConstraint(setExpr.includesAll(subsetExpr)); // The subset sum must not be larger than prescribed. // In OCL: subset->sum() <= n problem.addConstraint(subsetExpr.sum().leq(nExpr)); // Replace "leq" by "oclIsEqualTo" to force equality // We choose to maximize the sum of the subset as objective function. problem.maximize(subsetExpr.sum()); // We assign values to the constants defined. set.assignValue(new int[] {1, 2, 8}); n.assignValue(4); // Finally we solve the constraint satisfaction problem. classifierFactory.addToProblem(problem); set.addToProblem(problem); subset.addToProblem(problem); n.addToProblem(problem); boolean solved = problem.solve(); System.out.println("Solution found: " + solved); System.out.println("Satisfying subset: " + subsetExpr.evaluate()); } }

Further code samples can be found in the source code of OCLexec, an animator/simulator for UML/OCL specifications that is based on OCLsolve and the Eclipse MDT libraries.


These are some similar projects carried out by others: