合金平等

Question

我有一个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}

如何在两个签名之间取得平等？

Answer 1

从你的问题中不清楚你想做什么,从你的样本合金代码看起来好像你可能会遇到一些混乱.

首先,您展示的模型以两种不同的方式使用"性别"这一名称,这本身并不违法,但似乎表明存在一些混淆.(这肯定会让这位读者感到困惑.)

在两个单身人士签名约翰和史蒂夫的声明中,性别表示两个二元关系,一个在签名约翰和签名人之间,另一个控制在史蒂夫和男人之间.以符号形式说同样的事情,性别表示(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 
}

重命名变量会强制您选择一种含义或另一种含义.这是一件好事.(这是一个令人遗憾的事实,合金中的两种配方都没有实际令人满意.但是让我们一次解决一个问题;摆脱名称性别的双重用途是第一步.)

第二个问题是,无论你的意思是什么形式,它几乎肯定不代表你想要的意思.暂时忽略模型的细节,你的事实就是形式

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
  

• 出于同样的原因,无论模型如何,person = person将始终为true:对于任何模型实例,实例中的一组人员将与实例中的一组人员相同.所以条件总是成立,事实上实际上不会对模型的实例施加任何约束.

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

• 有一群人.
• 有些人是男性(性别='男性').其他人不是男性.
• 约翰是男性.
• 史蒂夫是一个男性.
• 约翰和史蒂夫是不同的人.
• 如果x和y是具有相同性别的个体,则x和y是相同的个体.也就是说,没有两个人具有相同的性别.

请注意,这些陈述不能同时成立.(如果这不是很明显,你可能会比试图找出原因更糟糕.合金可以帮助你.)

祝好运.