扩展签名和原子实例化

我使用的是Alloy 4.2，我使用继承有一个复杂性问题 . 显然，签名之间的继承不像我以前在面向对象编程中那样（或者至少像我期望的那样） .

显然，当在run命令中没有设置exact关键字时，即使根抽象类是抽象的，原子也会实例化为根抽象签名的原子 . 当exact关键字用于指定命令时，原子会在指定时被实例化：叶子具体类 .

我希望能够搜索具有从另一个抽象继承的集合的可变性的解决方案 . 它允许我在抽象签名中指定然后存在于叶签名中的关系 .

示例（详细程度需要设置为高）：

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

当我在这里运行2谓词时有以下痕迹：

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.

在这个执行跟踪中，我们可以看到，尽管A是抽象的，但所有B和C都被实例化为A原子 . 我们可以看到B和C在A元素集中挑选了6个不相交的元素 .

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.

在此跟踪中，我们可以看到A集仅由B和C元素组成，而不是由A元素组成 . 我们还可以看到，由于组合爆炸，求解时间非常不同，即使第二个命令解决的问题比第一个命令更简单 .

为了最大限度地缩短求解时间，是否可以通过在签名上使用事实或设置约束来获得看起来像这样的跟踪？

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]]