كيف يمكن للمرء أن يعبر عن أن العلاقة يجب ألا تكون دورية؟

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 }