Experimental: Attributes

There is a set of version numbers:

Version : int *
[Version + 2 > 0]

What is the value of Version in the constraint? Is the constraint satisfied? Is the meaning of plus purely arithmetic or it also handles sets? Semantic variants:

Sum

The same semantics as in Alloy: the value of a set is arithmetic sum of all its elements. The constraint becomes:

[sum(Version) + 2 > 0]

where sum(Version) is arithmetic sum of values of Version’s instances.

Implications

• Version is missing.

Reasonable default. If there is no Version instance, then the sum of empty set is 0. CDL uses the same semantics:

[(Version ? Version else 0) + 2 > 0]

• Version has cardinality 1

Everything is OK, because sum of Version will be equal to the scalar value.

• Version has cardinality > 1

There might be some problems. Let’s say Version has cardinality 2: Version = {a0, a1}, val(a0) = 2, val(a1) = -2. Then sum(Version) = 2 – 2 = 0, so the constraint is satisfied because [0 + 2 > 0]. For a0, we’ve got [2 + 2 > 0], which is ok. For a1, we’ve got [-2 + 2 > 0], which is unsatisfied. That seems counterintuitive. Even in the Clafer paper, we’ve got the constraint [comp.version = 1]. If we use the sum semantics there, not all components have to be in the version 1.

Advantages

• Reasonable value for empty sets: 0. The same value is used in CDL and the Excel spreadsheet.
• No guarding (to check empty sets) is necessary because we get 0 in the worst case.

Disadvantages

• Confusing for higher cardinalities.

Universal Quantification

Use universal quantification over all instances of Version. The constraint becomes:

[all a : Version | a + 2 > 0]

Implications

• Version is missing.

Then the constraint is completely ignored. It does not seem reasonable to ignore constraint just because the element is missing.

• Version has cardinality 1

Everything is OK.

• Version has cardinality > 1

Everything is OK. Apply the constraint for each instance of Version separately.

Advantages

• works well for non-empty clafers.

Disadvantages

• ignores constraints for empty Clafers.
• complex semantics

Enforced Presence

Enforces that all clafers used in constraints must be present. The constraint becomes:

[ some Version && Version + 2 > 0 ]

Implications

• Version is missing.

For this case, if there is no Version, then the whole constraint is unsatisfied. It is similar to undefined in OCL, because it signals an abnormal situation.

• Version has cardinality 1

Everything is OK.

• Version has cardinality > 1

It is unclear what happens in that case. Should it take the sum of all elements or do universal quantification?

Advantages

• It seems intuitive that the element should be present if we want the constraint to hold.

Disadvantages

• Stretching this idea shows unexpected behavior. First, what is the negation of Version + 2 > 0? Should it negate the presence of Version? [ ! (some Version && Version + 2 > 0) ] vs [some Version && !(Version + 2 > 0)] . Also [!(Version > 2)] is not necessarily the same as [Version <= 10] as one might expect.

Enforced Presence with Universal Quantification

This one specializes enforces presence by doing universal quantification. The constraint becomes:

[ some Version && all v : Version | v + 2 > 0 ]

Implications

• Version is missing.

As with enforced presence.

• Version has cardinality 1

Everything is OK.

• Version has cardinality > 1

Everything is Ok.

Advantages

• As for enforced presence.

Disadvantages

• As for enforced presence.
• complex semantics

Guards

All the constraints must be guarded and checked for emptiness. The constraint becomes:

[(Version ? Version : 0) + 2 > 0]

Implications

• Version is missing.

Reasonable default value: 0.

• Version has cardinality 1

Everything is Ok.

• Version has cardinality > 1

Unclear semantics for higher cardinalities.

Advantages

• Works fine for optional Clafers

Disadvantages

• Problems with higher cardinalities.
• If a clafer is used multiple times, it has to be guarded each time. Rather inconvenient.

Vector Operations

Sets are treated as vectors. Arithmetic operations act on vectors. For example is V = [1,2], then V + 2 = [3,4]. Syntactically the constraint does not change:

[Version + 2 > 0]

It is unclear what happens with non-arithmetic operators.

Implications

• Version is missing.

After performing addition, the relational expression works on an empty set. So we either compare empty set with 0 and return empty set as a result (and the whole constraint becomes false), or perform the comparison on all elements of empty set (and the whole constraint is satisfied).

• Version has cardinality 1

Everything is Ok.

• Version has cardinality > 1

In Clafer we do not have vectors of Boolean values, so relational operators cannot return vectors of Boolean values. Some kind of quantification would have to be used.

Advantages

• well-defined rules for arithmetic operations

Disadvantages

• complex semantics
• counterintuitive

Conclusion

None of the solutions is perfect. Deciding on a particular variant is a trade-off. Proposed solution:

• use the sum semantics for optional clafers. If something absent, then its value is 0.
• for clafers with higher cardinalities use quantifiers. The translator will do syntactic checks and will issue warnings if there is no quantification. The problem is that this semantics is rather complex, but might be intuitive.
• we need more examples to evaluate possible design decisions