Choco output should reflect the IR for group cardinality inheritance

[mantkiew]

In the Alloy output, the generation of group cardinality constraints is pushed down to the application site, that is, to the concrete clafers. However, doing the same for Choco looses the important information about where the group cardinality was declared.

abstract xor A       // xor declared but no constraint generated
   b
a1 : A                   // constraint generated because a1 is concrete
   c                        // the constraint applies to all children b, c, and d
   d
abstract G : A      // xor is inherited but no constraint generated
g1 : G
   e                       // the constraint applies to all children b and e

[JLiangWaterloo]

In my opinion, in the generated Choco IR, A should be the only clafer with group cardinality information. Here is my reasoning.

1. If I programmatically create a new clafer inheriting from A, then I need to also inherit the group cardinality. Hence A must have the group cardinality information.
2. G/a1/g1 should not have any group cardinality information attached directly. If I were to programmatically change the group cardinality of A, then the group cardinalities of G/a1/g1 will not be updated if they have their own copy of attached group cardinality.

[mantkiew]

How about a design in which all of them have group cardinality but with a flag whether it was declared (like for A), refined or inherited (for G, a1, and a2) for the given clafer?

abstract or H           // declared
    e
abstract I : H          // inherited
    f
xor J : I                   // refined
    g

The benefits are 1) you don't have to redo the analysis, 2) you can choose and change how you use this information in the backend, 3) decouple backend from frontend.

[JLiangWaterloo]

I would prefer not to do it that way. The reason is that the model may not necessarily come from the frontend (for example it could be handwritten using the Java API like I do in my unit tests). So I will have to do the analysis anyways, which is almost trivial.

[mantkiew]

It turns out that the inheritance resolver propagates group card. information to all clafers and it does not record whether it was declared, inherited, or refined. The only way for me to recover that information is to trace back to AST.

For Alloy, we simply generate nothing for abstract clafers but only for concrete ones, which gives us the right behavior.

Also, I checked how abstract and concrete clafers were generated over the releases. See genAbstractClafer and genConcreteClafer:

0.3.6
0.3.7
0.3.8
0.3.9
0.3.10
0.4.0
0.4.1

both functions remained virtually unchanged wrt. group card generation.

So, it's trivial for me to do generation of group card for all clafers (just like in IR), which would represent the philosophy that all information is already resolved and fully explicit. When creating clafers programmatically, one should specify the correct group cardinality anyway (copy from super, refine, or declare. Note that declaring group cardinality is only possible at the top of inheritance hierarchy otherwise it is default 0..* and lower in the inheritance hierarchy it's only refinement).

[JLiangWaterloo]

I fixed the bug in the Choco backend.

As long as either the abstract Clafer AND/OR the concrete Clafer has the group cardinality, then it will work.

[mantkiew]

Ok, then I'll generate group card for all clafers, except the ones which have the default one.