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

付録A 練習問題続きます。ようやく A.1 は終わりそうです。

• (f), (g), (h) はまとめて。(g) の「順番のヒント」という表現や (h) の「対称的な解が数多くある」というところから、解答はこういう書き方じゃないと思います(これだとインスタンスは1つだけ)。直接的な表現もいい練習になったのでこのままで。

module exercises/tube

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 {}

run {
  Jubilee = Stanmore + BakerStreet + BondStreet + Westminster +
                 Waterloo
  Central = WestRuislip + EalingBroadway + NorthActon +
                     NottingHillGate + BondStreet + LiverpoolStreet + Epping
  Circle = BakerStreet + NottingHillGate + Westminster + LiverpoolStreet

  -- jubilee
  jubilee = Stanmore -> BakerStreet +
            BakerStreet -> BondStreet +
            BondStreet -> Westminster +
            Westminster -> Waterloo

  -- central
  central = WestRuislip -> NorthActon +
            EalingBroadway -> NorthActon +
            NorthActon -> NottingHillGate +
            NottingHillGate -> BondStreet +
            BondStreet -> LiverpoolStreet +
            LiverpoolStreet -> Epping

  -- circle
  circle = BakerStreet -> NottingHillGate +
           NottingHillGate -> Westminster +
           Westminster -> LiverpoolStreet +
           LiverpoolStreet -> BakerStreet
}

• (i) [難解] と付けられているように問題文が難しいですが、何度か読んで、要するに途中に分岐などがある時にどちらにいっても到達できるかどうかの差だと考えて以下のように記述してみました

sig Station {
  line: set Station
  }
fact {
  no s: Station | s -> s in line
  }

-- 路線 line に from から to に到達する経路がある
pred CanReach (from, to: Station) {
  from = to or
  to in from.^line
  }

-- 路線 line でどの経路を選んでも from から to に必ず到達する
pred MustReach (from, to: Station) {
  no mid: Station |
    mid in from.^line and
    not mid in to.^line and
    not CanReach [mid, to]
  }

run {
  some from, to: Station |
    CanReach [from, to] and not MustReach [from, to]
  }

これで A.1 は終わりました。付録 A はまだまだ続きます。