alloy - 合金中的平等

Question

我有一个合金模型，其中包含以下内容：

abstract sig person{}

one sig john,Steve extends person  {Gender: man} 

sig man{}

fact {
  all name: person, Gender: man | 
      name.Gender = name.Gender => person =person}

如何使两个签名相等？

Answer 1

从您的问题中不清楚您想要做什么，并且从您的示例合金代码看来，您可能会遇到一些困惑。

首先，您展示的模型以两种不同的方式使用 Gender 这个名称，这本身并不违法，但似乎暗示了一些混淆。（这肯定会让这位读者感到困惑。）

在两个单例签名 john 和 Steve 的声明中，Gender 表示两个二元关系，一个在签名 john 和签名 man 之间持有，另一个在 Steve 和 man 之间持有。以符号形式表示同样的事情，Gender 表示 (a) john -> man 的某个子集，以及 (b) Steve -> man 的某个子集。

然而，在匿名的事实中，Gender 表示一个 man 类型的变量。

如果您找到重命名其中一个或另一个的方法，您的模型将更容易理解。由于量化表达式中的变量名称是任意的，如果您将其重新表述为，您的事实将意味着同样的事情

fact { all P : person, M : man | P.M = P.M => person = person }

如果这不是你的意思，那么你可能想说的是

fact { all P : person, M : man | 
    P.Gender = P.Gender => person = person 
}

重命名变量会迫使您选择一种含义或另一种含义。这是一件好事。（不幸的事实是，这两种配方在 Alloy 中实际上都不能令人满意。但让我们一次处理一个问题；第一步是摆脱对名称 Gender 的双重使用。）

第二个问题是，无论您对事实的任何表述，它几乎肯定并不意味着您想要它的意思。暂时忽略模型的细节，你的事实采取了形式

fact { all V1 : sig1, V2 : sig2 | 
  Expression = Expression => sig1 = sig1
}

对于模型中定义的某些关系，表达式是 V1.V2 或 V1.Relation。这里有几个问题：

• V1.V2 在 V1 和 V2 都是签名的名称或范围在给定签名上的变量的情况下是没有意义的：点运算符只有在其参数之一是关系名称时才有意义。

• 如果任何表达式 E 是有意义的，那么无论 E 是什么意思，形式为 E = E（例如，person.Gender = person.Gender）的布尔表达式都是真的。用 E 表示的任何东西自然会等于它自己。所以条件也可以写成

  1 = 1 => person = person
  

• 出于同样的原因，person = person 将始终为真，无论模型如何：对于任何模型实例，实例中的人员集都将与实例中的人员集相同。因此，条件将始终为真，并且事实实际上不会对模型的实例施加任何约束。

目前尚不清楚如何最好地帮助您前进。也许开始的一种方法是问自己，您试图在模型中捕获以下哪些陈述。

• 有一组人。
• 有些人是男性（有性别='男人'）。其他人不是男性。
• 约翰是一个男性个体。
• 史蒂夫是一个男性个体。
• 约翰和史蒂夫是不同的个体。
• 如果 x 和 y 是具有相同性别的个体，则 x 和 y 是同一个体。即没有两个人具有相同的性别。

请注意，这些陈述不可能同时为真。（如果这不明显，你可能会比试图找出原因更糟糕。合金可以在这方面有所帮助。）

祝你好运。