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

付録A.3 の古典的パズル終わりました。まだ A.4、A.5、A.6 があります……

• A.3.6 外科医のグローブ
  • まず普通にモデリングしてみてグローブを重ねて使わないと解がないことはわかるのと、内側のグローブ(医者の手に触れる面)は変更しないほうが利用効率がいいことは自明なので、内側のグローブと外側のグローブは one sig で明示的に分けてしまっています
  • あと各手術での選択肢は、外側のグローブをしないか、表裏どちらを使うかという3通りだけなので、そこからひとつ選択するというようにしています。ちょっと負けた気分ですがこのあたり決め打ちにしないとモデリングが難しいです
  • 各手術前後の状態を ContaminateStatus として util/ordering で順序付きのシグネチャとして定義して、init と traces で時間経過をモデリングする手法を採用
  • 最初 ContaminateStatus には GloveUsage への関連は持たせてなかったのですが、モデルのインスタンスを可視化した時に、どの手法を採用したのかわかりにくいので追加しました

open util/ordering [ContaminateStatus]

sig Patient {}

sig Surface {}
abstract sig Glove {
  inside: one Surface,
  outside: one Surface
} { inside != outside }
one sig DoctorGlove extends Glove {}
one sig OuterGlove extends Glove {}

sig ContaminateStatus {
  contaminate: set Surface,
  waiting: set Patient,
  usage: lone GloveUsage
}

fact {
  // 全てのグローブの裏表の面(Surface)が別ものであること
  all disj g1, g2: Glove |
    no (g1.inside+ g1.outside) & (g2.inside + g2.outside)
}

pred init (s: ContaminateStatus) {
  s.contaminate = DoctorGlove.inside
  s.waiting = Patient
  s.usage = none
}

enum GloveUsage { NoOuterGlove, NormalOuterGlove, ReversedOuterGlove }

pred taint (s, s': ContaminateStatus, outer: Surface, touch: set Surface) {
  no s.contaminate & touch
  implies s'.contaminate = s.contaminate + outer
  else s'.contaminate = s.contaminate + outer + touch
}
pred operation (s, s': ContaminateStatus, u: GloveUsage) {
  one p: s.waiting | s'.waiting = s.waiting - p
  u = NoOuterGlove
  implies taint [s, s', DoctorGlove.outside, none]
  else u = NormalOuterGlove
    implies taint [s, s', OuterGlove.outside, DoctorGlove.outside + OuterGlove.inside]
    else taint [s, s', OuterGlove.inside, DoctorGlove.outside + OuterGlove.outside]
}
pred NoExposure (s: ContaminateStatus, u: GloveUsage) {
  u = NoOuterGlove
  implies not DoctorGlove.outside in s.contaminate
  else u = NormalOuterGlove
    implies not OuterGlove.outside in s.contaminate
    else not OuterGlove.inside in s.contaminate
}

pred traces {
  init [first]
  all s: (ContaminateStatus - last) | {
    let s' = s.next | {
      one u: GloveUsage |
        s'.usage = u and
        NoExposure [s, u] and
        operation [s, s', u]
    }
  }
  no last.waiting
}

run {
  traces
} for 4 but exactly 3 Patient