时间戳

首页 > 解决方案 > 检查合金中的 Sig 等式

equality - 检查合金中的 Sig 等式

问题描述

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

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

标签： equalitymodelingalloy

解决方案

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

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

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

sig Info {}

sig ActiveInfo in Info {}

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

推荐阅读