管理メニュー

Model Base

A.1.11 地下鉄をモデリングする

最終更新：

modelbase

- view
管理者のみ編集可

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

( a ) 路線line にある駅の集合がS である

"路線line上の駅の集合はSである" という述語を定義する。

路線lineの各区間の始端の集合は line.univ 、各区間の終端の集合は univ.line となる。
路線lineの駅の集合は始端と終端の和集合となる。 

 pred stations[line: univ->set univ, S: set univ]{
   let Points = univ.line+line.univ |
     S = Points
   }

( b ) line には切れ目がない

"路線lineには切れ目がない" という述語を定義する。

路線の走行方向を無視した関係(line+~line)を考える。路線内の到達可能な2点の関係は、^(line+~line) で表せる。 異なる任意の2点がこれに含まれていれば、切れ目がないと言える。 

 pred continuous[line: univ->set univ]{
   let Points = univ.line+line.univ |
     all disj p1,p2: Points | p1->p2 in ^(line+~line) 
   }

もし路線に切れ目がないとき、これは2 人の乗客がそれぞれ任意の駅から乗車して、互いが合流できる3 つめの駅が常に存在することを意味するか？

まず検証用に駅と路線を定義する。 

 sig Eki{ rosen: set Eki }

目的の検証に沿った適当な制約を課す。 

 fact{
   -- 全ての駅は路線上の駅である
   Eki in rosen.univ + univ.rosen
   -- 駅は3つ以上あり、乗車可能な駅は2つ以上ある
   #(rosen.univ + univ.rosen) > 2 and #(rosen.univ) > 1
   -- 路線上の各区間を片方向に走る
   oneWay[rosen]
   }
 
 pred oneWay[line: univ->set univ]{
   let Points = univ.line+line.univ |
     no p,p': Points | p->p'+p'->p in line
   }
 
 run rosen{} for exactly 6 Eki

こんな感じの路線図が出てくる。

制約Cを以下のようにして検証してみる。 

 check C{
   -- 路線に切れ目がないなら
   continuous[rosen] =>
     -- 任意の異なる2駅から乗車させて合流できる3つ目の駅が存在する
     all disj e1,e2: rosen.univ | some e: Eki-e1-e2 | e1->e + e2->e in ^rosen
   }for 6 Eki

反例が現れた。 

Executing "Check C for 6 Eki"
  Solver=minisatprover(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
  1869 vars. 54 primary vars. 3354 clauses. 63ms.
  Counterexample found. Assertion is invalid. 15ms.

反例では乗車駅がEki5とEki4であり、確かに２人が合流できる駅がない。

( c ) line の端点は駅の2 集合、from とend である

"路線lineの始端駅の集合はfromであり、終端駅の集合はendである" という述語を定義する。

路線は片方向に走ると仮定しているので、 univ.line は下車可能な駅の集合、line.univ は乗車可能な駅の集合となる。 

 pred fromAndEnd[line: univ->set univ, from, end: set univ]{
   let Points = univ.line+line.univ |{
     from = Points - univ.line
     end = Points - line.univ
     }
   }

( d ) line の分岐合流点は集合S 内の駅である

"路線lineの分岐合流点は集合Sに含まれる" という述語を定義する。

点p への流入経路数は #line.p、点pからの流出経路数は #p.line となる。
分岐合流点は、流入経路か流出経路、またはその両方が複数路存在することで定義付ける。 

 pred junction[line: univ->set univ, S: set univ]{
   let Points = univ.line+line.univ |
     all p: Points | (#line.p > 1 or #p.line > 1)=> p in S 
   }

( e ) line が円環になる

"路線lineは円環である" という述語を定義する。

端点が存在しないことで定義付ける。 

 pred ring[line: univ->set univ]{
   fromAndEnd[line, none, none]
   }

( f ) 簡易版の地下鉄マップにある実際の駅と路線を使い、制約を具体化せよ

テンプレートにならって、地下鉄マップにある路線(駅の2項関係)と駅のシグネチャを導入する。
また、地下鉄網についての以下の制約を記述して、述語 tubeNetwork にまとめる。

  • 路線は一方向のみに走る
  • 路線を構成する駅の集合
  • 路線と駅の集合の関連付け
  • 路線に切れ目はない
  • 路線の端点
  • 路線circleは環状線
  • 合流点
  • 循環区間がない 
     abstract sig Station{
   jubilee, central, circle: set Station
   }
 sig Jubilee, Central, Circle in Station{}
 one sig
   Stanmore, BakerStreet, BondStreet, Westminster, Waterloo,
   WestRuislip, EalingBroadway, NorthActon, NottingHillGate,
   LiverpoolStreet, Epping
   extends Station {}
 
 pred tubeNetwork{
   -- 路線は一方向のみに走る
   oneWay[jubilee]
   oneWay[central]
   oneWay[circle]
   -- 路線を構成する駅の集合
   Jubilee = Stanmore + BakerStreet + BondStreet + Westminster + Waterloo
   Central = WestRuislip + EalingBroadway + NorthActon + NottingHillGate + BondStreet + LiverpoolStreet + Epping
   Circle = BakerStreet + LiverpoolStreet + Westminster + NottingHillGate
  -- 路線と駅の集合の関連付け
   stations[jubilee, Jubilee]
   stations[central, Central]
   stations[circle, Circle]
   -- 路線に切れ目はない
   continuous[jubilee]
   continuous[central]
   continuous[circle]
   -- 路線の端点
   fromAndEnd[jubilee, Stanmore, Waterloo]
   fromAndEnd[central, WestRuislip + EalingBroadway, Epping]
   -- 環状線
   ring[circle]
   -- 合流点
   junction[jubilee, none]
   junction[central, NorthActon]
   junction[circle, none]
   -- 循環区間がない
   not loop[jubilee]
   not loop[central]
   }
 
 -- 循環区間がある
 pred loop[line: univ->set univ]{
   some iden & ^line
   }
 
 run tubeNetwork
    とりあえず run tubeNetwork を実行してみたが、地下鉄マップのようにはならない。

( g ) 各駅の順序に関するヒントを追加せよ

駅の並び順についてのヒントを与えれば与えるほど、Alloyが提示する地下鉄網の候補は絞り込まれる。
色々試してみた末、候補を1つに絞り込むため、 central線、circle線、BondStreet駅について、以下のヒントを与えた。 

 pred stationOrderHint{
   -- central線についてのヒント
   NorthActon -> NottingHillGate in central
  
   -- circle線についてのヒント
   BakerStreet -> LiverpoolStreet in circle
   Westminster -> NottingHillGate in circle
 
   -- BondStreet駅についてのヒント
   BakerStreet -> BondStreet in jubilee
   BondStreet -> Westminster in jubilee  
   NottingHillGate -> BondStreet in central
   BondStreet -> LiverpoolStreet in central
   }

( h ) コマンドを起動し、サンプルとなるインスタンスを生成せよ 

 run withHint{
   tubeNetwork
   stationOrderHint
   }

run withHint を実行してみると地下鉄マップのようになった。

( i )[難解]

駅from から出発して、line 上の駅to に至る経路がある、という制約を記述せよ。

駅to は路線line上の駅であること、そして地下鉄網tubeに駅fromから駅toへ至る経路があることを宣言する。
推移閉包を用いれば特に難しいわけでない。 

 -- 駅from から出発して、line 上の駅to に至る経路がある、という制約
 pred hasPath[tube: univ->set univ, from: univ, line: univ->set univ, to: univ]{
   -- toはline上の駅
   to in univ.line + line.univ
   -- fromからtoへ到達可能
   to in from.^tube 
   }

次に、もしfrom を出発してline を経由したならば、必然的にto に到達するという制約を記述せよ。

lineとかtoでは頭の整理がつかなかったので、出題とは若干用語を変え、
"もしfrom を出発してlineX を経由したならば、必然的にSX に到達する"
と言い換えて、述語 if_take_lineX_always_reachable_SX を作ってみる。

最初に、述語を分解してみる。

「from を出発してlineX を経由した」ならば「必然的にSX に到達する」…①

束縛変数"駅dx"を導入して①を書き直す。

任意の駅dxについて、
「駅fromを出発点とする場合に、駅dxが路線lineXによる経由路の出発点である」
ならば
「駅dxで路線lineXに乗車すれば、必然的に駅SXに到達する」
 …②

前件をdx∈R、後件をP(dx)として②を一階述語の論理式(数学記法は書籍「コンピュータのための数学」に準拠)で書くと、

∀dx|: dx∈R ⇒ P(dx)　…③

これは、制限域をRとした記述に変形できる。 

∀dx|R: P(dx)  …④

さらに②の後件に束縛変数"駅next"を導入して書き直すと、

任意の駅dxについて、
「駅nextが、駅dxの路線lineX上の次の駅」
 ならば、
 「駅nextから必然的に駅SXに到達する」

となる。上記の前件をnext∈R'(dx)、後件をQ(next)とすれば④は、 

∀dx|R: next∈R'(dx) ⇒ Q(next) 
≡
∀dx|R: ∀next|R'(dx): Q(next)  …⑤

となり、
Rを DX という名の関数、Qを anyPathReachable という名の述語、R'(dx)を dx.lineX として、 ⑤をAlloy語で書くと、以下のようになる。

all dx: DX[ ... ] | all next: dx.lineX | anyPathReachable[ ... ] …⑥

以下、⑥の述語と関数について考える。
まずは関数 DX について検討するが、その前に関数DXの動作を観察するための環境を事前に準備しておく。 

 abstract sig STATION{
   lineA, lineB, lineC: set STATION
   }
 one sig
   S1, S2, S3, S4, S5, S6
   extends STATION{}
 
 fact tubeNetwork2{
   -- 路線は一方向のみに走る
   oneWay[lineA]
   oneWay[lineB]
   oneWay[lineC]
   -- 路線は1区間以上ある
   some lineA
   some lineB
   some lineC
   -- 路線に切れ目はない
   continuous[lineA]
   continuous[lineB]
   continuous[lineC]
   -- 地下鉄網に切れ目はない
   continuous[lineA+lineB+lineC]
   }

関数DXは、
　「駅fromを出発点とする場合に、駅dxが路線lineXによる経由路の出発点である」
ような駅dxの集合である。

したがって、
　「駅fromを出発してlineX以外の路線で進んだあとに、路線lineXへの初めての乗り換えのための乗車駅となる駅dxの集合」
としてDXを求めればよい。なお、駅fromが路線lineXの乗車駅ならば、fromをDXに含める必要がある。

 fun DX[tube: univ->set univ, from: univ, lineX: univ->set univ]: set univ{
   let DepartureOfLineX = lineX.univ |
   { dx: DepartureOfLineX | dx in from.*(tube-lineX) }
 }
 
 -- ビジュアライザ観察用
 fun DX: set univ{
   let tube = lineA+lineB+lineC,--地下鉄網 
       lineX=lineA, --経由路線
       from=S1 | --出発点
       DX[tube, from, lineX]
   }

ちなみに、ビジュアライザ観察用の引数なしの関数DXは、内部で実際の関数DX[…]を呼んでいる。 こうすることで図中に$DXの表示が現れるので観察しやすくなる。

ビジュアライザ観察用のDXを実行すると下のようなインスタンスをが得られる。
この場合、DXは駅S1から出発して路線lineAによる経由路の出発駅の集合なのだが、駅S4がDXに含まれていない。
S1→S3→S4 とlineBで移動し、S4で初めてlineAに乗車することができるのだから、S4もDXに含まれているべきだ。

どうやら、前述の"lineX以外の路線"という表現を tube-lineX と表現したのがまずいらしい。 路線lineXを地下鉄網から除いた情報を関数の外から与える。 

 fun DX[tube_without_lineX: univ->set univ, from: univ, lineX: univ->set univ]: set univ{
   let DepartureOfLineX = lineX.univ|
   { dx: DepartureOfLineX | dx in from.*tube_without_lineX }
   }
 
 -- ビジュアライザ観察用
  fun DX: set univ{
    let tube' = lineB+lineC,--路線lineXを除いた地下鉄網 
      lineX=lineA, --経由路線
      from=S1 | --出発点
      DX[tube', from, lineX]
    }

今度はS4もDXに含まれている。

次に⑥の述語 anyPathReachable について。

述語 anyPathReachable は、
　「駅Sから必然的に駅SXに到達する」
であり、言い換えれば、
　「駅Sから駅SXへは全ての経路で到達する」
となる。さらに言い換えると、
　「駅Sから駅SXへは、駅SXを通過せずに駅Sから到達可能な全ての駅から到達する」
となる。
これは以下のように書ける。 

 pred anyPathReachable[tube: univ->set univ, S, SX: univ]{
   let tubeEndAtSX = (univ-SX)<:tube,
       reachableFromS = S.*tubeEndAtSX |
       all S': reachableFromS | SX in S'.*tubeEndAtSX
   }

"駅SXを通過せずに"の部分は、SXが終端駅となる地下鉄網tubeEndAtSX、 

tubeEndAtSX = (univ-SX)<:tube

を導入して準備する。
"駅SXを通過せずに駅Sから到達可能な全ての駅"は、駅の集合reachableFromS、 

reachableFromS = S.*tubeEndAtSX

で定義できる。SXとSが同じ駅の場合でもこの集合に含まれるように、tubeEndAtSXの反射推移閉包を用いた。
"駅Sから駅SXへは、reachableFromS(=駅SXを通過せずに駅Sから到達可能な全て)の駅から到達する"は、 

all S': reachableFromS | SX in S'.*tubeEndAtSX

と書ける。

上記の関数DXと述語anyPathReachableで⑥を以下のようにして、述語 if_take_lineX_always_reachable_SX を完成させる。 

 pred if_take_lineX_always_reachable_SX
 [tube_without_lineX: univ->set univ, from: univ, lineX: univ->set univ, SX: univ]{
   let tube = tube_without_lineX + lineX |
   all dx: DX[tube_without_lineX, from, lineX] |
     all next: dx.lineX | anyPathReachable[tube, next, SX]
   }

解析器を使ってこの2制約を区別するような路線を生成せよ。

前記の記述をまとめたものが以下になる。 

 -- 駅from から出発して、line 上の駅to に至る経路がある
 pred hasPath[tube: univ->set univ, from: univ, line: univ->set univ, to: univ]{
   -- toはline上の駅
   to in univ.line + line.univ
   -- fromからtoへ到達可能
   to in from.^tube 
   }
   
 -- 駅fromを出発してlineX以外の路線で進んだあとに、
 -- 路線lineXへの初めての乗り換えのための乗車駅となる駅dxの集合
 fun DX[tube_without_lineX: univ->set univ, from: univ, lineX: univ->set univ]: set univ{
   let DepartureOfLineX = lineX.univ|
   { dx: DepartureOfLineX | dx in from.*tube_without_lineX }
   }
 
 -- ビジュアライザ観察用
 fun DX: set univ{
    let tube_without_lineX = lineB+lineC,--路線lineXを除いた地下鉄網
      lineX=lineA, --経由路線
      from=S1 | --出発点
      DX[tube_without_lineX, from, lineX]
    }
   
 -- 駅Sから必然的に駅SXに到達する
 pred anyPathReachable[tube: univ->set univ, s, SX: univ]{
   let tubeEndAtSX = (univ-SX)<:tube,
       reachableFromS = s.*tubeEndAtSX |
       all s': reachableFromS | SX in s'.*tubeEndAtSX
   }
   
 -- もしfrom を出発してlineX を経由したならば、必然的にSX に到達する
 pred if_take_lineX_always_reachable_SX
 [tube_without_lineX: univ->set univ, from: univ, lineX: univ->set univ, SX: univ]{
   let tube = tube_without_lineX + lineX |
   all dx: DX[tube_without_lineX, from, lineX] |
     all next: dx.lineX | anyPathReachable[tube, next, SX]
   } 
   
 -- 地下鉄網の状況設定
 abstract sig STATION{
   lineA, lineB, lineC: set STATION
   }
 one sig
   S1, S2, S3, S4, S5, S6
   extends STATION{}
 
 -- 路線lineには切れ目がない
 pred continuous[line: univ->set univ]{
   let Points = univ.line+line.univ |
     all disj p1,p2: Points | p1->p2 in ^(line+~line) 
   }

 -- 路線上の各区間を片方向に走る
 pred oneWay[line: univ->set univ]{
   let Points = univ.line+line.univ |
     no p,p': Points | p->p'+p'->p in line
   }
   
 fact tubeNetwork2{
   -- 路線は一方向のみに走る
   oneWay[lineA]
   oneWay[lineB]
   oneWay[lineC]
   -- 路線は1区間以上ある
   some lineA
   some lineB
   some lineC
   -- 路線に切れ目はない
   continuous[lineA]
   continuous[lineB]
   continuous[lineC]
   -- 地下鉄網に切れ目はない
   continuous[lineA+lineB+lineC]    
   }
     
 run {
   -- 設問のfromをS1、toをS2、lineをlineA とする
   hasPath[lineA+lineB+lineC, S1, lineA, S2]
   not if_take_lineX_always_reachable_SX[lineB+lineC, S1, lineA, S2]
   }

インスタンスをいくつか見てみると、いずれも駅S1を出発して駅S2へ到達することができる。 しかし、路線lineAを経由したからといって、必ず駅S2へ到達できるわけではない。

Fig A.1.11.i-31

↑路線lineAを経由するのは駅S2を通過した後なのだが、確かに 「路線lineAを経由したからといって、必ず駅S2へ到達できるわけではない」 である。

Fig A.1.11.i-32

Fig A.1.11.i-33












「A.1.11 地下鉄をモデリングする」をウィキ内検索
記事メニュー
人気記事ランキング
  1. 「状態遷移システムの構成概念を理解する」のPFD
もっと見る
最近更新されたページ
もっと見る
目安箱バナー