Как можно выразить, что отношения не должны быть циклическими?

Question

Рассмотреть а upgrades отношение:

Мне нужно убедиться, что upgrades не может быть круговым. Как я могу сделать это в сплаве?

Answer 1

Достаточно для обеспечения соблюдения транзитивности и противоречивления.

fact {
  no a: Item | a in a.upgrades
}

fact{
  all a,b,c: Item |
  a in b.upgrades and b in c.upgrades implies
  a in c.upgrades
}

Answer 2

С вашего примера я вывод, что upgrades Соотношение не предназначено для того, чтобы быть транзитивными: в примере, алмазный мечод обновляет каменный меч, а каменный мечод обновляет деревянный меч, но пара Woodsword -> Diamondsword не в upgrades связь.

Так что вы хотите сказать, это что-то вроде

fact upgrades_acyclic {
  no x : univ | x in x.^upgrades
}

Некоторые моделиры предпочитают более скланктивную формулировку с точки зрения отношений:

fact upgrades_acyclic { no ^upgrades & iden }