A.1.8 無向グラフの非循環性を定義する - Model Base

更新日2011-09-03[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ]

---

 sig Node {adjs: set Node}
 pred acyclic () {
   adjs = ~adjs
   -- 非反射的
   no iden & adjs
   -- 全域的
   Node in adjs.Node
 }
 run acyclic for 4

---