The OntoUML2Alloy transformation of cardinality constraints is overrestrictive in specific cases.

This problem affects relationships where one of the domains is a 
RigidSortalClass or a MomentClass and the minimum cardinality constraint in the 
extremity connected to the other domain is greater than zero.

What steps will reproduce the problem?
1. Create an empty OntoUML model in the OntoUML editor;
2. Create a RigidSortalClass or a MomentClass (e.g., a «kind») "A";
3. Create a Classifier (e.g., a «kind») "B";
4. Create a Relationship "R" between "A" and "B";
5. Set the cardinalities of "R" in the extremity connected to "B" as "m..n", 
where both m and n are greater than zero;
6. Transform this model into Alloy by using our OntoUML2Alloy transformation.

What is the expected output? What do you see instead?

In the automatically generated Alloy specification, the expected output would 
be the generation of a cardinality constraint in the form:

abstract sig World {...}{
...
all x: A:>domain_of_quantification | (#R.x >= m) and (#R.x <= n)
}

However, the transformation generates the following one:

abstract sig World {...}{
...
all x: A | (#R.x >= m) and (#R.x <= n)
}

Firstly, remember that, from the Alloy specification of "R", if xRy in a world 
w, then both x and y must be in the domain of quantification of w. The problem 
with the code above is that, as m is greater then zero, it is demanding that 
all instances x of "A" must be in the domain of quantification of every world, 
so that the number of instances of "B" connected to x is greater than zero in 
all worlds.

The first formula corrects this issue, because it only demands that for every 
world w and every instance x of "A" that is in the domain of quantification of 
w, the number of instances of "B" connected to x is greater than zero in w. 
There is no cardinality constraint for the instances of "A" that are not in the 
domain of quantification of w. Therefore, it is possible to x to not be in the 
domain of quantification of w.

Please use labels and text to provide additional information.

Original issue reported on code.google.com by alessand...@gmail.com on 7 Jan 2011 at 1:02

nemo-ufes / ontouml-editor-eclipse

The OntoUML2Alloy transformation of cardinality constraints is overrestrictive in specific cases. #24