alloy - 如何表达一种关系不能是循环的？

Question

考虑一个upgrades关系：

我需要确保它upgrades不能是循环的。我怎样才能在合金中做到这一点？

Answer 1

从您的示例中，我推断upgrades关系不是传递关系：在示例中，钻石剑升级石剑，石剑升级木剑，但 WoodSword -> DiamondSword 对不在upgrades关系中。

所以你想说的是

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

一些建模者更喜欢在关系方面更简洁的表述：

fact upgrades_acyclic { no ^upgrades & iden }

Answer 2

强制传递性和反反射性就足够了。

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
}