A.1.6 スパニング木 - Model Base

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

---

 open util/graph[V] as gr

 -- 頂点の集合Vと辺の集合Eの定義
 some sig V{
   E: set V
   }
 -- 辺を持たない頂点は除外しておく
 fact{ V in E.univ + univ.E }
  
 pred isTree (r: univ -> univ){
   gr/tree[r]
   }
 
 pred spans (r1, r2: univ -> univ){
   r2 = E
   -- 部分グラフ
   r1 in r2
   -- すべてのノードを通る
   univ.r2 + r2.univ in univ.r1 + r1.univ
   }
 
 pred show (r, t1, t2: univ -> univ){
   spans [t1, r] and isTree [t1]
   spans [t2, r] and isTree [t2]
   t1 not = t2
   }
 
 run show for 4

インスタンスを見やすくするためにThemeを設定する。 ビジュアライザ画面のThemeアイコンを押せばテーマ設定が開くので 以下のように調整した。

• relations の $show_r　の Show as arcs をoffにする
• relations の E　のライン種を Dotted にする Applyアイコンを押して変更を反映させる。

---

スコープ4

---

スコー6

---

スコープ8

---