白と黒のとびら 第4章 金と銀と銅 その2

解けた! 部屋の数がこれまでに比べて多めなので解析にも時間がかかります。

module white_black/gold_silber_copper

abstract sig 場所 {
  値段: Int
} {
  値段 >= 0
}

sig 部屋 extends 場所{
  金: one 場所,
  銀: one 場所,
  銅: one 場所
}

one sig 入口 extends 部屋 {} {
  値段 = 0
}
one sig 中庭 extends 場所 {} {
  値段 = 12
}

pred キヌタンの家 {
  all room: 部屋 | room.金.値段 > room.値段 and room.銀.値段 > room.値段 and room.銅.値段 > room.値段
  all room: 部屋 | (room.金.値段  = plus[room.値段, 10]) or (room.金.値段 <= plus[room.値段, 10] and room.金 = 中庭)
  all room: 部屋 | (room.銀.値段  = plus[room.値段, 5]) or (room.銀.値段 <= plus[room.値段, 5] and room.銀 = 中庭)
  all room: 部屋 | (room.銅.値段  = plus[room.値段, 1]) or (room.銅.値段 <= plus[room.値段, 1] and room.銅 = 中庭)

  all disj a,b: 部屋 | (a.金 != b.金) or (a.銀 != b.銀) or (a.銅 != b.銅)
}

assert 全ての部屋はいずれ中庭に通じる {
  キヌタンの家 => all room: 部屋 | 中庭 in room.^(金+銀+銅)
}
check 全ての部屋はいずれ中庭に通じる for 20 場所, 6 Int

assert 実際の経路 {
  キヌタンの家 => 入口.金.金 = 中庭 and
                        入口.銀.銀.銀 = 中庭 and
                        入口.銅.銅.銅.銅.銅.銅.銅.銅.銅.銅.銅.銅 = 中庭
}
check 実際の経路 for 20 場所, 6 Int

assert 全ての部屋の値段は異なる {
  キヌタンの家 => all disj a, b: 部屋 | a.値段 != b.値段
}
check 全ての部屋の値段は異なる for 20 場所, 6 Int

run キヌタンの家 for 20 場所, 6 Int

今回は弟子の考察から、各部屋にはその部屋に至った段階でいくら支払うことに同意したかの値段がついていて、どの経路でも一定の値段になること、120トラヌ以上(モデル上は数値が大きくなると Int のスコープをひろげないといけないので 10 で割って値段にしました)支払うことになると中庭に抜ける、行き先が全て同じ部屋は2つ以上ない(むだな部屋がない)という設計として、その場合に弟子が実際に通った経路や推定している条件を assert でチェックしつつ作っていくようにしました。この設計でありえる構造は1つに絞られます。
なお整数の加算が a + b じゃなくて plus[a, b] なのを忘れててひっかかってたのが一番時間がかかりました。ついやってしまいますね。