どのようにして関係が周期的であってはならないことを表現することができますか？

Question

upgradesの関係を考えてみます：

私はupgradesが円形でないことを確認する必要があります。私はそれが合金中にどのように行うことができますか？

Answer 1

これは推移とantireflexivityを強制するのに十分である。

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

一例では、ダイヤモンドの剣は石の剣をアップグレードして、石剣は木製の剣をアップグレードしますが、ペアWoodSwordは - > DiamondSwordではありません。

あなたの例から、私はupgrades関係が推移的であることを意図していないことを推測しますupgradesの関係でます。

だから、何が言いたいことは、

のようなものです

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

いくつかのモデラーは関係の面でより簡潔製剤を好むます：

fact upgrades_acyclic { no ^upgrades & iden }