extending signatures and atoms instantiation

Question

I am using Alloy 4.2 and I have a complexity problem using inheritance. Apparently the inheritance between signatures does not behave as I used to face in object oriented programming (or at least as I expect).

Apparently when the exactly keyword is not set in the run command, the atoms are instantiates as the atoms of the root abstract signature even if the root abstract class is abstract. When the exactly keyword is used to specify a command the atoms are instantiated as they are specified: leaf concrete classes.

I would like to be able to search solutions with a variability of sets that inherits from another abstract one. It allow me to specify relations in the abstract signature which then exists in the leaf signatures.

example (verbosity needs to be set to high):

abstract sig A {}

sig B extends A {}

sig C extends A {}

pred show {}

run show for 6 B, 6 C
run show for exactly 6 B, exactly  6 C

When I run the 2 predicate here are the following traces :

Executing "Run show1 for 6 B, 6 C"
   Sig this/B scope <= 6
   Sig this/C scope <= 6
   Sig this/A scope <= 12
   Sig this/A in [[A$0], [A$1], [A$2], [A$3], [A$4], [A$5], [A$6], [A$7], [A$8], [A$9], [A$10], [A$11]]
   Sig this/B in [[A$0], [A$1], [A$2], [A$3], [A$4], [A$5], [A$6], [A$7], [A$8], [A$9], [A$10], [A$11]] with size<=6
   Sig this/C in [[A$0], [A$1], [A$2], [A$3], [A$4], [A$5], [A$6], [A$7], [A$8], [A$9], [A$10], [A$11]] with size<=6
   Solver=minisatprover(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=4 Symmetry=20
   15152 vars. 24 primary vars. 55808 clauses. 55164ms.
   Instance found. Predicate is consistent. 225ms.

In this execution trace we can see that all B and C are instantiated as A atoms despite A is abstract. And we can see that B and C have pick 6 disjoint elements in the A element set.

Executing "Run show2 for exactly 6 B, exactly 6 C"
   Sig this/B scope <= 6
   Sig this/C scope <= 6
   Sig this/A scope <= 12
   Sig this/A in [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5], [C$0], [C$1], [C$2], [C$3], [C$4], [C$5]]
   Sig this/B == [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5]]
   Sig this/C == [[C$0], [C$1], [C$2], [C$3], [C$4], [C$5]]
   Solver=minisatprover(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=4 Symmetry=20
   0 vars. 0 primary vars. 0 clauses. 2ms.
   Instance found. Predicate is consistent. 14ms.

In this trace, we can see that the A set is composed only of B and C elements, not A elements. We also can see that the solving time is very different due to combinatorial explosion, even if the problem solved by the second command is simpler than the first one.

To minimise solving time, is it possible to have trace that would look like this by using fact or setting constraints on signatures?

Executing "Run show2 for 6 B, 6 C"
   Sig this/B scope <= 6
   Sig this/C scope <= 6
   Sig this/A scope <= 12
   Sig this/A in [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5], [C$0], [C$1], [C$2], [C$3], [C$4], [C$5]]
   Sig this/B == [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5]]
   Sig this/C == [[C$0], [C$1], [C$2], [C$3], [C$4], [C$5]]

Answer 1

When the "exactly" keyword is not used, then it is not possible to know the actual type of each atom before solving the model. In other words, scope

run show for 6 B, 6 C

specifies only upper bounds, meaning that a valid instance is allowed to contain, for example, 2 atoms of B and 1 atom of C (depending on the actual constraints in the model). That's why Alloy can only allocate enough atoms to start with (giving them some generic names, in this case names derived from the name of the base type), and after an instance is found, each atom will be renamed (in the visualizer) to reflect its actual type.

Only when you specify exact scopes Alloy can minimize the bounds (as you noticed) in order to potentially reduce the solving time.