FAQ

 Why do you restrict your "theorem" to instances (of data models) such that all relevant attributes are defined? What is the problem with undefined attributes?

Consider the following very simple data model Persons:

entity Person isUser{
  Integer age
}

Consider also the following OCL boolean expression PersonsAge:

not(Person.allInstances()->exists(p|p.age = 40)) 
   and not(Person.allInstances()->forAll(p|p.age < 40 or p.age > 40))

The set of sentences ocl2fol_th(Persons) U ocl2fol_def(Persons, PersonsAge) U ocl2fol_sen(PersonsAge) that our mapping generates is clearly unsatisfactory, i.e., there does not exist any first-order model which can satisfy every sentence in this set.

Consider now an instance of Persons that only contains one object of type Person and suppose that this object has its attribute age  undefined. Notice that, for this instance of Personsdue to the OCL semantics for the undefined value,  the OCL boolean expression PersonsAge will evaluate to true!

Therefore, we need to restrict our "theorem" to instances (of data models) such that all relevant attributes are defined. This restriction was not explicitly stated in our original paper Clavel et al. 2009

We are currently working on a new mapping that will (try to) take into consideration the OCL semantics for the undefined value.