alloy - 表达几个实例之间的等价性

Question

假设我的模块中有一个与 sig B 相关的 sig A。

想象一下，现在我们有几个实例:

A$1 -> B$1   , A$2 -> B$2

和

A$1 -> B$2   , A$2 -> B$1

我想表达 B$1 和 B$2 是等价的(在某些条件下)，这样只会生成此实例 A$1 -> B , A$2 -> B.

其中一个解决方案可能是在声明 sig B 时使用关键字“one”，但在我的情况下它不起作用，因为 B 有多个字段，使得 B 原子不一定等价。简而言之，只有当它们具有相同值的场时，2 个原子才等价。

理想情况下，我想删除 B 的编号。但仍然可以有多个原子 B。

Answer 1

Alloy Analyzer 无法让您对后续实例的生成方式(或对称性破坏方式)进行太多控制，因此您通常必须在模型级别解决这些问题。

对于你的例子，也许这是正确的模型

sig B{}

one sig BA extends B {}

sig A {
  b: one BA
}

run { #A=2 }