Model Base
A.1.5 木を特徴付ける
最終更新:
modelbase
更新日2011-09-03
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計/付録 A 練習問題 解答例 ]
木の有向グラフを作るにあたって頂点と辺の定義を準備する。
-- 頂点の集合Vと辺の集合Eの定義 some sig V{ E: set V } -- 辺を持たない頂点は除外 fact{ V in univ.E + E.univ }
発見的に木を作ってみる
まずは、始端は1つだけであるという性質だけを与える。
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
反例はなかった。