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

付録A 練習問題続きます。今日は雨で時間がなかったので1つだけ。

• A.2.1 (c) 通話転送機能をくみこむ
  • 転送先が接続元だったら？と思いましたが、相互の接続は禁止していないのでそのままにしました。うーん、こういう細かいところ悩みますね。

module exercises/phones

sig Phone {
  requests: set Phone,
  connects: lone Phone,
  forward: 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
  no p: Phone | p -> p in forward
  }

// (b)-1 すべての接続には対応する要求がある
fact {
  all p1, p2: Phone | p1 -> p2 in connects => p1 -> p2 in requests
}
// 会議通話(複数の接続をもつ通話)は forward を除いて存在しない
fact {
  all p: Phone | #(p.connects - p.forward) + #connects.p < 2
  }
// forward をもつ電話に電話がかかったら転送する
fact {
  all p: Phone |
    none = connects.p or  // p に電話がかかってないか
    none = p.forward   or  // 転送先が設定されていなければ
    p -> p.forward in connects // 転送先にも接続する
  }
run {
  SomeRequestsExist
  SomeConnectionsExist
  AvoidSelfConnection
}