首页 文章

util / ordering模块和有序子签名

提问于
浏览 次
1

考虑以下Alloy模型：

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 / ordering告诉我 . 但那与原因不完全相同 . ）

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

或者还有其他事情发生在我身上吗？

在这个模型中，这是抽象的，我真的希望有一个类似A的名字来表示B和C的结合，我真的很喜欢C被命令，我真的很喜欢B无序和非空 . 目前，我似乎能够实现任何两个目标;有没有办法同时管理这三个？

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

alloy

2 回答

  • 1

    简短回答：报告的现象来自违约和隐含范围的规则;这些规则在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

    我会留下这个问题以获得其他答案，并希望它可以帮助其他一些用户 .

    回复于
  • 1

    我理解有序签名将始终具有与示波器允许的原子数一样多的原子，因为util / ordering告诉我 . 但这与原因并不完全相同 .

    原因在于，当强制有序sig包含与范围允许的原子数量时，转换器可以生成有效的对称破坏谓词，在大多数示例中，有序sig可以产生更好的求解时间 . 因此，这仅仅是一种权衡，而设计决策是为了获得性能而强制实施这种额外约束 .

    回复于

相关问题