1

考虑以下合金模型：

open util/ordering[C]

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

pred show {}
run show for 7

我理解为什么，当 I 时run show for 7，该模型的所有实例都有 7 个签名 C 原子。（嗯，这不太正确。我知道有序签名将始终具有范围允许的尽可能多的原子，因为 util/ordering 告诉我是这样。但这与为什么不完全相同。）

但是为什么这个模型的实例没有任何签名 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根本不产生任何实例。也许我需要更好地理解范围规范的语义。]

4

2 回答 2

2

简短的回答：报告的现象来自默认和隐式范围的规则；这些规则在Language Reference的 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，签名 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

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

于 2013-06-26T00:09:55.210 回答
1

我知道有序签名将始终具有范围允许的尽可能多的原子，因为 util/ordering 告诉我。但这与为什么不完全相同。

原因是，当强制一个有序 sig 包含尽可能多的原子时，翻译器可以生成一个有效的对称破坏谓词，在大多数有序 sig 示例中，这会导致更好的求解时间。所以这只是一个权衡，设计决定是强制执行这个额外的约束以获得性能。

于 2013-06-26T16:51:50.507 回答