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

付録A 練習問題続きます。A.3 の古典的パズル続きです。

A.3.4 Halmos の握手問題
- カップルが集まったパーティで Alice 以外の全員が握手した回数がばらばらの時に、Alice のパートナーの Bob が握手した回数は何回か？
- この問題は Alloy でモデリングしてても解答がわからなかった。他の問題はモデリングしているうちに要点が判るようなものだったけど

sig Person {
  shakehands: set Person,
  partner: one Person
  }
one sig Alice in Person {} {
  partner = Bob
  }
one sig Bob in Person {} {
  partner = Alice
  }

fact {
  // shakehands は対称的
  ~shakehands in shakehands
  // partner も対称的
  ~partner = partner
  // パートナーは自分自身ではない
  all p: Person | not p = p.partner
  // 自分自身とは握手しない
  no iden & shakehands
  // 自分のパートナーとも握手しない
  all p: Person | no p.partner & p.shakehands
  }

fact {
  // Alice 以外の全員が握手した回数が異なる
  all disj p1, p2: (Person - Alice) |
    #p1.shakehands != #p2.shakehands
  }

run {} for exactly 10 Person

assert BobShakehandsWithFourPerson {
  #Bob.shakehands = 4
}
check BobShakehandsWithFourPerson for exactly 10 Person

- 解析器で例をいくつか作ってみるとどうやら Bob の握手した回数は常に 4 らしい。そこで assert を追加して check コマンドで検証したらやはり10人の参加者の場合は常に 4になる
- (b) Bob の握手する回数が異なる別解があるかもしれないのでモデルを拡張せよ、という問題なのですが、どこをいじっていいのかわからないのでパス。回数変えられるのかな？
A.3.4 ヤギ、キャベツ、狼
- 目を離すとヤギがキャベツを、狼がヤギを食べてしまうという条件のなかで1つの舟でどうやって川を渡るかというよくあるパズル

open util/ordering [Time]

sig Time { dir: Direction }
enum Direction { Forward, Backward }
abstract sig Place {
  exist:  Property set -> Time
}
one sig NearSide extends Place {}
one sig Boat extends Place {} {}
one sig FarSide extends Place {}

abstract sig Property {
  eat: set Property
}
one sig Cabbage extends Property {} { eat = none }
one sig Goat extends Property {} { eat = Cabbage }
one sig Wolf extends Property {} { eat = Goat }

fact {
  // 複数の場所に同時に存在することはできない
  all p: Property | all t: Time | #exist.t.p = 1
  // Boat には1つまでしか積めない
  all t: Time | #Boat.exist.t < 2
}

pred init (t: Time) {
  // 最初はボートが NearSide 側にある
  t.dir = Forward
  // こちら側にキャベツ、山羊、狼がいて他は空
  NearSide.exist.t = Cabbage + Goat + Wolf
  Boat.exist.t = none
  FarSide.exist.t = none
}

// 食ってしまうペアがいる場所はない
pred AvoidTragedy (t: Time) {
  all p: Place |
    no p1, p2: Property | p1 in exist[p].t and p2 in exist[p].t and p2 in p1.eat
}

// 荷の積み降ろし。ボートに乗せた荷は常に降ろす
// 乗せたまま引き換えすと同じ状態の繰り返しで意味がないので除外
pred Charge (t, t': Time, side: Place) {
  lone p: side.exist.t |
    side.exist.t' = side.exist.t - p + Boat.exist.t and
    Boat.exist.t' = p
}
// 反対の場所の状態は変化しないことを制約にする
pred NotChange (t, t': Time, side: Place) {
  side.exist.t' = side.exist.t
}
pred Transit (t, t': Time) {
  t.dir = Forward
    implies Charge [t, t', NearSide] and
                 NotChange [t, t', FarSide] and
                 t'.dir = Backward
    else Charge [t, t', FarSide] and
            NotChange [t, t', NearSide] and
            t'.dir = Forward
}

pred traces {
  init [first]
  all t: (Time - last) | let t' = t.next |
    Transit [t, t'] and
    AvoidTragedy [t']
}
run {
  traces
  // 最後はボートが向こう岸に着いてて
  last.dir = Backward
  // 最後の荷をボートに乗せている状態
  #FarSide.exist.last = 2 and #Boat.exist.last = 1
} for 8 Time

- util/ordering を使って順序付きの Time シグネチャを導入して時間の概念を入れる方法
- 両岸(NearSide, FarSide)から荷の積み降ろしをして引き換えすごとを1つのイベントとしている
- 最後のイベントは全部の荷が渡ったところではなくて、最後の荷をボートに乗せて向こう岸に着いた状態とするようにしている

A.3 のパズルはあと1問です。これがモデル化が難しそう。