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

付録A 練習問題続きます。
A.1.10 の地下鉄路線のモデリングの (f), (g), (h) なんですが、あれ多分それ以前の問題で出てきた記述を使ってやれってことだったんですね。というわけで別解を作りました。インスタンスを減らすために駅の順番のヒントは少し増やしています。「circle は環状」とか、それぞれの路線の端点や分岐点だけを指定しているので、実際とは違う解も出てきます

module exercises/tube2

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 = jubilee - iden
  central = central - iden
  circle = circle - iden

  -- 全ての Station はいずれかの路線に所属する
  all s: Station | s in Jubilee or s in Central or s in Circle

  -- jubilee に含まれている駅の集合が Jubilee
  Jubilee = jubilee.univ + univ.jubilee
  -- central に含まれている駅の集合が Central
  Central = central.univ + univ.central
  -- circle に含まれている駅の集合が Circle
  Circle = circle.univ + univ.circle

  -- 各路線には切れ目がない
  all disj x, y: Jubilee | y in x.^jubilee or x in y.^jubilee
  all disj x, y: Central | y in x.^central or x in y.^central
  all disj x, y: Circle | y in x.^circle or x in y.^central

  -- jubilee の from は Stanmore, to は Waterloo
  Stanmore = jubilee.univ - univ.jubilee
  Waterloo = univ.jubilee - jubilee.univ
  -- central の from は WestRuislip と EalingBroadway, to は Epping
  WestRuislip + EalingBroadway = central.univ - univ.jubilee
  Epping = univ.central - central.univ
  -- circle には端点(from, to)がない
  none = circle.univ - univ.circle
  none = univ.circle - circle.univ

  -- jubilee には分岐合流点がない
  no s: Jubilee | #s.jubilee > 1 || #jubilee.s > 1
  -- central の分岐合流点は NorthActon
  NorthActon = { s: Central | #s.central > 1 || #central.s > 1 }
  -- circle には分岐合流点がない
  no s: Circle | #s.circle > 1 || #circle.s > 1

  -- 路線内の連結のヒント
  -- central で WestRuislip の次が NorthActon
  WestRuislip.central = NorthActon
  -- central で NorthActon の次が NottingHillGate
  NorthActon.central = NottingHillGate
  -- jubilee で Stanmore の次が  BakerStreet
  Stanmore.jubilee = BakerStreet
  -- jubilee で LiverpoolStreet の次が Epping
  LiverpoolStreet.jubilee = Epping
  -- circle で LiverpoolStreet の次に BakerStreet
  LiverpoolStreet.circle = BakerStreet
  -- circle で NottingHillGate の次に Westminster
  NottingHillGate.circle = Westminster
}

A.2.1 電話のスイッチング接続
- (a), (b) 自由に追加した制約は「接続要求と接続は少なくとも1つはある」「自分自身に接続要求も接続もできない」です。

module exercises/phones

sig Phone {
  requests: set Phone,
  connects: lone Phone
  }

// 接続要求と接続は1つ以上ある
pred SomeRequestsExist {
  #requests > 0
  }
pred SomeConnectionsExist {
  #connects > 0
  }
// 自分自身に接続しない
pred AvoidSelfConnection {
  no p: Phone | p -> p in requests
  no p: Phone | p -> p in connects
  }

// (b)-1 すべての接続には対応する要求がある
fact {
  all p1, p2: Phone | p1 -> p2 in connects => p1 -> p2 in requests
}
// (b)-2 会議通話(複数の接続をもつ通話)はない
fact {
  all p: Phone | #p.connects + #connects.p < 2
  }

run {
  SomeRequestsExist
  SomeConnectionsExist
  AvoidSelfConnection
}