util/ordering 模块和有序子签名

考虑以下合金模型：

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 原子。（嗯，这并不完全正确。我明白that有序签名将始终具有范围允许的尽可能多的原子，因为 util/ordering 告诉我这一点。但这并不完全相同why.)

但为什么这个模型的实例没有任何签名 B 的原子呢？这是对 util/ordering 执行特殊处理的副作用吗？ （有意？无意？） util/ordering 是否仅适用于顶级签名？

或者还有什么我想念的事情吗？

在这个模型中，这是抽象的，我真的很想为 B 和 C 的并集起一个像 A 这样的名字，我真的很希望 C 是有序的，我真的很希望 B 是无序的，非空。目前，我似乎能够实现其中任何两个目标；有没有办法同时管理这三个？

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

简短的回答：所报告的现象是由默认和隐含范围的规则引起的；这些规则在 B.7.6 节中讨论语言参考.

更长的答案：

最终证明我应该更仔细地研究范围规范的语义，这一怀疑是有道理的。在此显示的示例中，规则完全按照记录执行：

• For run show for 7，签名A默认范围为7； B 和 C 也是如此。使用 util/ordering 模块强制 C 原子数为 7；这也耗尽了签名 A 的配额，从而使签名 B 的隐式范围为 0。

• For run show for 2 but 3 B，签名 A 的默认范围为 2，B 的显式范围为 3。这使得签名 C 的隐式签名为 2 减 3，或负 1。这似乎算作不一致；范围界限预计为自然数。

• For run show for 2 but 3 B, 3 C，签名 A 的隐式界限为 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

我将把这个问题留给其他答案，并希望它可以帮助其他一些用户。