抽象によるソフトウェア設計 付録A 練習問題 その8

付録A 練習問題続きます。先はまだまだ長いです。

• A.1.11 地下鉄をモデリングする (続き)
  • 一昨日書いたのだと line が二項関係になっていたので少し変更
  • (a) 路線 line にある駅の集合が S
    • 「路線 line」というのがどういう意味かよくわからないので単に Station の派生シグネチャとしました
    • また line は「路線 line での駅のあいだの隣接関係(一方通行)」としました
    • また line が自分自身と繋がるのは妙なのでそれも禁止しました

abstract sig Station {
  line: lone Station
  }
fact {
  no s: Station | s -> s in line
  }
sig S extends Station {}

• • (b) line には切れ目がない(これは変わらず)

fact {
  all disj x, y: S |
    y in x.^line or x in y.^line
}
assert C {
  all disj x, y: S | some z: S |
    z in x.^line and z in y.^line
}
check C

• • (c) line の端点 from と to。これは多分表現する式を書けばいいんですよね

-- from
line.univ - univ.line  -- line の始点側に含まれているけど終点側に含まれてないもの
-- to
univ.line - line.univ  -- line の終点側に含まれているけど終点側に含まれてないもの

• • (d) line の分岐合流点は集合 S 内
    • ここでの S は (a) の S と同じものを指してるんでしょうか(それだと自明なような)、それとも line の分岐合流点の集合を S として形式化しろということなのか……

some s: S | #s.line > 1 || #line.s > 1

• • (e) line が環状になっている (a〜d を使って書ける)

run Circle {
  -- line に切れ目がない
  all disj x, y: S | y in x.^line or x in y.^line
  -- line の端点が空集合
  no (line.univ - univ.line)
  no (univ.line - line.univ)
  -- line の分岐集合点が空集合
  no s: S | #s.line > 1 || #line.s > 1
  }

A.1.11 はまだ続きがあって、今度は具体的な駅名でモデリングするようです。