如何在Alloy中明确指定签名？

Question

我正在学习Alloy建模语言，并且看到了这段代码。

sig Person {
  partner: Person
}

fact partnerProperties {
  partner = ~partner
  no p: Person | p in p.partner
}

此代码表示“人的partner关系是相互的”。

我可以理解上面的代码，但是我认为如何表达partner是明确地写在Person中的关系。由于可读性。

我想这样写。

fact partnerProperties {
  Person.partner = ~Person.partner
  no p: Person | p in p.partner
}

我是研究生来帮助我。

Answer 1

您可以按如下方式编写量化：

sig Person {
  partner: Person
}

fact partnerProperties {
  all p1,p2:Person| p1.partner=p2 implies p2.partner=p1
  no p: Person | p in p.partner
}

run{}

请注意，在这种情况下，每个人只能有一个伴侣。该模型允许多元性：

sig Person {
  partner: some Person
}

fact partnerProperties {
  all p1,p2:Person| p2 in p1.partner  implies p1 in p2.partner
  no p: Person | p in p.partner
}

run{} for 5