OCL2MSFOL is a pure Java application that generates a Many-Sorted First-Order Logic (MSFOL) theory from an Object Constraint Language (OCL) constraint with an underlying contextual model. The mapping is strictly based on the work of Carolina Dania et. al. at IMDEA Research Institute, Madrid, Spain. The detail of the mapping definition can be reviewed here.
OCL works with a four-value logic: true, false, null and invalid. While the first two values are understood universally, the last two represent undefinedness: null represents unknown or undefined value whereas invalid represents an error or exception. Given an OCL constraint (represented as a string) and its contextual model (represented as a JSON file), OCL2MSFOL generates a complete FOL theory in SMT-LIB2 language as a text file.
There are four modes that can be chosen from: TRUE, FALSE, NULL and INVALID. Each model corresponds to a different theory which can be interpreted differently. For example, given an OCL expression e, using the application with mode TRUE generates a MSFOL theory that defines scenarios in which evaluating e returns true.
Please be aware that neither the mapping definition nor the implementation is complete. The following items highlight the supported subset of OCL:
- literal: Boolean, Integer, String.
- Boolean:
true
,false
. - Integer: ...,
-1
,0
,1
, ... - String:
"a string"
, ...
- Boolean:
- predefined variables of permitted types.
caller
,self
,user
, ...
- datamodel's attributes and association-ends.
user.age
,user.accounts
, ...
- datamodel classes's
allInstances()
.class.allInstances()
- logical operations:
not
,and
,or
,implies
. - comparison operations
=
,<
,<=
,>
,>=
,<>
. - collection's operations:
isEmpty()
,notEmpty()
,isUnique()
,forAll()
,exists()
,collect()
,select()
. - undefinedness opeartions:
oclIsUndefined()
,oclIsInvalid()
.
- (required)
Maven 3
andJava 1.8
(or higher). - (submodule)
datamodel
- branch:OCL2MSFOL
. - (submodule)
JavaOCL
submodule - branch:master
.
The submodules will be automatically updates using Git
commands as in the guideline.
git clone https://github.com/npbhoang/OCL2MSFOL.git
git submodule update --init --recursive
Have a quick look at the Runner.java
class for a quick guideline.
Below provides a few OCL expression as examples:
// Case 1: true
String inv = "true";
// Case 2: caller.students->isEmpty
OCL2MSFOL.putAdhocContextualSet("caller", "Lecturer");
String inv = "caller.students->isEmpty()";
// Case 3: self.age >= 18
OCL2MSFOL.putAdhocContextualSet("self", "Student");
String inv = "self.age >= 18";
// Case 4: Student.allInstances()->forAll(s|s.lecturers->forAll(l|l.age > s.age))
String inv = "Student.allInstances()->forAll(s|s.lecturers->forAll(l|l.age > s.age))";
// Case 5: caller.age = self.age
OCL2MSFOL.putAdhocContextualSet("self", "Student");
OCL2MSFOL.putAdhocContextualSet("caller", "Lecturer");
String inv = "caller.age = self.age";
// Case 6: self.name = user
OCL2MSFOL.putAdhocContextualSet("self", "Student");
OCL2MSFOL.putAdhocContextualSet("user", "String");
String inv = "self.name = user";