我有一个Alloy模型，其中包含以下内容：
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}
如何在两个签名之间取得平等？
从你的问题中不清楚你想做什么，从你的样本合金代码看起来好像你可能会遇到一些混乱 .
First, 您展示的模型以两种不同的方式使用名称Gender，这本身并不违法，但似乎表明存在一些混淆 . （这肯定会让这位读者感到困惑 . ）
在两个单身人士签名约翰和史蒂夫的声明中，性别表示两个二元关系，一个在签名约翰和签名人之间，另一个控制在史蒂夫和男人之间 . 以符号形式说同样的事情，性别表示（a）约翰的某些子集 - >男人，以及（b）史蒂夫的某些子集 - >男人 .
然而，在匿名事实中，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 }
重命名变量会强制您选择一种含义或另一种含义 . 这是一件好事 . （这是一个令人遗憾的事实，合金中的两种配方都没有实际令人满意 . 但是让我们一次解决一个问题;摆脱名称性别的双重用途是第一步 . ）
A second issue 无论你指的是什么形式，它几乎肯定并不意味着你想要的意思 . 暂时忽略模型的细节，你的事实就是形式
fact { all V1 : sig1, V2 : sig2 | Expression = Expression => sig1 = sig1 }
其中Expression是V1.V2或V1.Relation，用于模型中定义的某些Relation . 这里有几个问题：
V1.V2没有意义，其中V1和V2都是给定签名范围内的签名或变量的名称：只有当其中一个参数是关系的名称时，点运算符才有意义 .
如果任何表达式E都有意义，那么无论E的含义如何，形式为E = E的布尔表达式（例如，person.Gender = person.Gender）都为真 . E表示的任何东西自然都等于它自己 . 所以有条件的也可以写
1 = 1 => person = person
目前尚不清楚如何最好地帮助您前进 . 也许一种开始的方法是问自己，您试图在模型中捕获以下哪些语句 .
有一群人 .
有些人是男性（性别= 'man'） . 其他人不是男性 .
约翰是男性 .
史蒂夫是一个男性个体 .
约翰和史蒂夫是不同的人 .
如果x和y是具有相同性别的个体，则x和y是同一个体 . 即没有两个人有相同的性别 .
请注意，这些陈述不能同时成立 . （如果这不是很明显，你可能会比试图找出原因更糟糕 . 合金可以帮助你 . ）
祝好运 .
1 回答
从你的问题中不清楚你想做什么，从你的样本合金代码看起来好像你可能会遇到一些混乱 .
First, 您展示的模型以两种不同的方式使用名称Gender，这本身并不违法，但似乎表明存在一些混淆 . （这肯定会让这位读者感到困惑 . ）
在两个单身人士签名约翰和史蒂夫的声明中，性别表示两个二元关系，一个在签名约翰和签名人之间，另一个控制在史蒂夫和男人之间 . 以符号形式说同样的事情，性别表示（a）约翰的某些子集 - >男人，以及（b）史蒂夫的某些子集 - >男人 .
然而，在匿名事实中，Gender表示man类型的变量 .
如果您找到重命名其中一个或另一个的方法，您的模型将更容易理解 . 由于量化表达式中的变量名称是任意的，如果将其重新表示为，则事实将意味着相同的事情
如果这不是你想说的话，那么你可能想要说些什么
重命名变量会强制您选择一种含义或另一种含义 . 这是一件好事 . （这是一个令人遗憾的事实，合金中的两种配方都没有实际令人满意 . 但是让我们一次解决一个问题;摆脱名称性别的双重用途是第一步 . ）
A second issue 无论你指的是什么形式，它几乎肯定并不意味着你想要的意思 . 暂时忽略模型的细节，你的事实就是形式
其中Expression是V1.V2或V1.Relation，用于模型中定义的某些Relation . 这里有几个问题：
V1.V2没有意义，其中V1和V2都是给定签名范围内的签名或变量的名称：只有当其中一个参数是关系的名称时，点运算符才有意义 .
如果任何表达式E都有意义，那么无论E的含义如何，形式为E = E的布尔表达式（例如，person.Gender = person.Gender）都为真 . E表示的任何东西自然都等于它自己 . 所以有条件的也可以写
目前尚不清楚如何最好地帮助您前进 . 也许一种开始的方法是问自己，您试图在模型中捕获以下哪些语句 .
有一群人 .
有些人是男性（性别= 'man'） . 其他人不是男性 .
约翰是男性 .
史蒂夫是一个男性个体 .
约翰和史蒂夫是不同的人 .
如果x和y是具有相同性别的个体，则x和y是同一个体 . 即没有两个人有相同的性别 .
请注意，这些陈述不能同时成立 . （如果这不是很明显，你可能会比试图找出原因更糟糕 . 合金可以帮助你 . ）
祝好运 .