检查合金中的 Sig 相等性

问题描述

在以下 Alloy 模型中，我想检查具有 Bool 字段类型的 sig 的两个实例的相等性：

module test

open util/boolean as bool


sig Info {
    active: Bool
}

assert assertion {
    all x1,x2: Info |
        x1.active = True && x2.active = True implies x1 = x2
}

check assertion for 10

如果 x_1 和 x_2 都将 True 作为其 active 字段，此模型会检查它们是否相等。 Alloy 给出了一个反例，然而，在反例中，x_1 和 x_2 在结构上是相等的，但出于某种原因，Alloy 认为它们不相等。

编辑：

一个建议是使用子类型如下：

sig Info {}

sig ActiveInfo in Info {}

-- i is inactive if i in (Info - ActiveInfo)

但是，这不适合我的模型。

引自《软件抽象》一书：

" 相等是结构相等还是引用相等？

关系没有与其值不同的身份，所以这种区别，基于编程概念，这里没有意义。如果两个关系具有相同的元组集，则它们不是两个关系：它们只是一个和相同的关系。一个原子不过是它的身份；当两个原子是同一个原子时，它们是相等的。如果你有一组原子表示复合对象（使用一些关系将原子映射到它们的内容），您可以定义任何结构相等的概念你想要明确地，通过引入一个新的关系。（对于那些 C++ 那里的程序员：不，你不能在 Alloy 中重新定义等号。）”

我不太明白这一段。我很欣赏关于合金中平等如何运作的解释。特别是如何检查具有不同身份但相同值的原子的相等性？

解决方法

我知道 Alloy 中的平等是基于价值观的。

这不是真的。 x1 和 x2 具有相同的 active 值，但在签名中是不同的原子。这类似于在很多 OOP 语言中，两个对象可以具有相同的结构值但具有不同的身份。

顺便说一下，我建议使用子类型来表示布尔值。你可以这样做

sig Info {}

sig ActiveInfo in Info {}

-- i is inactive if i in (Info - ActiveInfo)

如果愿意，您可以将签名中的字段视为“属于”该签名的一个原子，但最好将字段视为关系。如果他们有同一个母亲，你不会期望两个人是一样的：

sig Person {mother: Parent}

但是如果您希望您的签名具有没有两个不同成员具有相同字段的属性，您可以将其添加为事实：

sig Coordinate {x,y: Value}
fact {all c,c': Coordinate | (c.x = c'.x and c.y = c'.y) implies c = c'}

alloy equality modeling