Как указать подпись прямо в Alloy?

Question

Я изучаю язык моделирования Alloy, и я видел этот код.

sig Person {
  partner: Person
}

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

Этот код express "Отношение человека partner является взаимным".

Я могу понять код выше, но я думаю, что express 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

Answer 2

Обратите внимание, что Person.partner не означает, что вы думаете, что это значит. Это соединение набора Персона и партнера по отношениям. Чтобы указать партнера по отношениям, принадлежащего подписи Person, вы должны написать Person <: partner, но в этом нет необходимости, так как это делает Alloy.

Answer 3

Вы делаете его более кратким, добавляя его в качестве факта в Person

sig Person { partner : Person } {
   this not in partner
   this in partner.@partner
}

Факт, добавленный к sig, сделает автоматическое c количественное определение с this по всем атомам из sig. Все поля, которые являются частью sig, будут расширены с this. перед ними. Это объясняет использование знака @. Без знака @ расширение будет выглядеть следующим образом:

sig Person { partner : Person } {
   this not in this.partner
   this in this.partner.this.partner
}

this. подходит для первого partner, но для второго partner соединение должно быть с результатом (this.partner) а не this. Знак @ перед вторым partner говорит Alloy не ставить this перед ссылкой. Расширение тогда:

sig Person { partner : Person } {
   this not in this.partner
   this in this.partner.partner
}

Это решение:

┌───────────┬───────┐
│this/Person│partner│
├───────────┼───────┤
│Person⁰    │Person³│
├───────────┼───────┤
│Person¹    │Person²│
├───────────┼───────┤
│Person²    │Person¹│
├───────────┼───────┤
│Person³    │Person⁰│
└───────────┴───────┘