A.1.5 木を特徴付ける - Model Base

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

---

木の有向グラフを作るにあたって頂点と辺の定義を準備する。

 -- 頂点の集合Vと辺の集合Eの定義
 some sig V{
   E: set V
   }
 -- 辺を持たない頂点は除外
 fact{ V in univ.E + E.univ  }

発見的に木を作ってみる

まずは、始端は１つだけであるという性質だけを与える。

 pred isTreeH(r: univ -> univ){
   let 
   -- ノード
   NODE = r.univ,
   -- 始端
   START = NODE - univ.r |{
     -- 始端は唯一存在する(ルートノードのこと)
     one START
     }
   }

こんな感じのインスタンスが出てきた。

単射的な性質を加えることにする。

 pred isTreeH(r: univ -> univ){
   let 
   -- ノード
   NODE = r.univ,
   -- 始端
   START = NODE - univ.r |{
     -- 始端は唯一存在する(ルートノードのこと)
     one START
     -- 単射的
     r.~r in iden
     }
   }

こんな感じのインスタンスが出てきた。

始端ノードから、全ノードへ到達できる性質を加える。

 pred isTreeH(r: univ -> univ){
   let 
   -- 始端のノード
   START_NODE = r.univ - univ.r |{
     -- 始端のノードは唯一存在する(ルートノードのこと)
     one START_NODE
     -- 単射的
     r.~r in iden
     -- 始端ノードから、全ノードへ到達できる
     all n: START_NODE |  r.univ+univ.r in n.*r 
     }    
   }

木になっている感じがする。

定義に沿って木を作ってみる

今度は定義に沿って木を作ってみる。
グラフで"木"と呼ばれるものは、

閉路を持たない単連結なグラフ

という定義らしい。

 pred isTreeD(r: univ -> univ){
   -- 閉路を持たない
   no (^r  & iden)
   -- 単連結
   connected1[r]
   }
 
 pred connected1(r: univ -> univ){
   -- 単射
   r.~r in iden
   -- 連結
   let R = r+~r,     -- 無向グラフ化 
       U = R.univ |  -- 全ノード
     -- 任意のノードへ到達可能
     all u: U | U in u.*R
   }

単連結は定義できているか自信がないが、いくつかのインスタンスを見る限り 木が作れているようだ。
最初に作ったisTreeHと次に作ったisTreeDが同じ定義と なっているのか、検算してみる。

 -- 検算
 check sameDef {
   isTreeH[E] <=> isTreeD[E]
   }for 4

反例がないのでスコープ4の範囲では同じだ。
しかし、実のところisTreeHとisTreeDで全く同じ誤定義をしているかもしれない。

念のため、ライブラリと比較してみる。 (冒頭でutil/graphをオープンしておく。)

 open util/graph[V] as gr
 
 ...
 
 -- 検算
 check valid{
   --どちらか一方の定義だけ比較すればよし
   isTreeH[E] <=> gr/tree[E]
   //isTreeD[E] <=> gr/tree[E]
   }for 4

反例はなかった。

---