检查合金中的 Sig 等式答案

【问题标题】：Checking Sig Equality in Alloy检查合金中的 Sig 等式
【发布时间】：2021-09-29 04:49:12
【问题描述】：

在下面的合金模型中，我想检查两个具有 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 中重新定义等号。）”

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

【问题讨论】：

标签： equality modeling alloy

【解决方案1】：

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

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

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

sig Info {}

sig ActiveInfo in Info {}

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

【讨论】：

感谢您的回答。但是，使用子类型不适合我的模型。请检查我编辑的问题。

【解决方案2】：

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

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'}

【讨论】：