Model Base
A.1.6 スパニング木
最終更新:
modelbase
-
view
更新日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