3

假设我的模块中有一个与 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 。

4

2 回答 2

4

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

对于您的示例，也许这是正确的模型

sig B{}

one sig BA extends B {}

sig A {
  b: one BA
}

run { #A=2 }
于 2013-06-18T14:57:46.303 回答
1

首先，您说您描述的两个实例是等价的，尽管在表面上它们似乎具有不同的 A$1 和 A$2 值。然后你说“只有当......它们的字段[具有]相同的值时，2个原子才等效”。如果这是对等的定义，那么您的两个实例不等价；如果你的两个实例是等价的，那么你的定义没有捕捉到你想要的。

听起来好像您的意思是（1）B原子是（1a）总是等价的，或者（1b）在某些情况下是等价的，以及（2）如果A原子的字段都具有相同或等价的值，则它们是等价的. 好像你想禁止等效的 A 原子。如果是这样，那么你的工作是：

  • 定义一个对两个 B 元素为真的谓词当且仅当它们是等价的。
  • 为两个 A 元素定义一个谓词，当且仅当它们等价时为真。
  • 定义一个谓词（或事实），指定实例中没有两个 A 原子是等价的。

如果您的问题只是分析器正在向您显示模型的实例，这些实例彼此之间并没有有趣的区别，那么请参阅 Aleksandar Milicevic 的回复。

于 2013-06-18T16:12:06.323 回答