alloy - 関係が循環的であってはならないことをどのように表現できますか？

Question

関係を考えてみましょうupgrades：

upgrades私はそれが循環できないことを確認する必要があります。どうすればAlloyでそれを行うことができますか？

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 }