util/序模和有序子签名

Question

考虑以下合金模型：

open util/ordering[C]

abstract sig A {}
sig B extends A {}
sig C extends A {}

pred show {}
run show for 7

我理解为什么当我run show for 7时，这个模型的所有实例都有7个签名C原子(嗯，这不是完全正确的)。我知道有序签名总是有尽可能多的原子，因为util/ ordered告诉我是这样的。但这与原因并不完全相同。)

但是为什么这个模型的实例中没有任何特征B的原子呢？这是为util/ordering执行的特殊处理的副作用吗？(意欲？意料之外？)使用/排序是否只适用于顶级签名？

还是我错过了别的什么事？

在这个模型中，这是抽象的，我真的很想有一个名字，比如A来表示B和C的结合，我非常希望C是有序的，我真的希望B是无序的和非空的。目前，我似乎能够实现其中的任何两个目标；是否有办法同时管理这三个目标？

增编:我注意到指定run show for 3 but 3 B, 3 C确实实现了我的三个目标。相反，run show for 2 but 3 B根本不产生任何实例。也许我需要更好地理解范围规范的语义。

Answer 1

简短的回答:报告的现象是默认和隐式范围规则的结果；这些规则将在语言参考的B.7.6节中讨论。

较长的答覆：

最终的怀疑是，我应该更仔细地研究范围规范的语义，这是有道理的。在这里所示的示例中，规则的工作原理与文档完全相同：

• 对于run show for 7，签名A的默认范围为7；B和C也是如此。使用util/ordering模块强制C原子数为7；这也耗尽了签名A的配额，从而使签名B的隐式范围为0。
• 对于run show for 2 but 3 B，签名A的默认范围为2，而B的显式范围为3。这使得签名C的隐式签名为2减3，或负1。这似乎是不一致的；范围界应该是自然数。
• 对于run show for 2 but 3 B, 3 C，signature的隐界为6(子签名界之和)。

为了更好地理解范围规则，执行以下所有命令对此用户非常有用：

run show for 3
run show for 3 but 2 C
run show for 3 but 2 B
run show for 3 but 2 B,  2 C
run show for 3 but 2 A
run show for 3 but 2 A, 2 C
run show for 3 but 2 A, 2 B
run show for 3 but 2 A, 2 B, 2 C

我将把这个问题留待其他人回答，并希望它能帮助其他用户。

Answer 2

我知道有序签名总是有尽可能多的原子，因为util/ ordered告诉我是这样的。但这和原因不完全一样。

其原因是，当强制一个有序的sig包含尽可能多的原子时，翻译器就有可能生成一个高效的对称破缺谓词，在大多数有有序sig的例子中，这会带来更好的求解时间。因此，这是一个简单的权衡，而设计决定是执行这个额外的约束，以获得性能。