白と黒のとびら第1章遺跡その3

あいだが空きましたが、昨日は第1章の遺跡を Alloy で表現してみようとして少し書いていました。
今日も新たに読み進めるのではなくて Alloy で検証してみました。

まず遺跡の制約と、長老、長老の兄、遺跡に「喰われた」人の証言から遺跡の構造を記述してみます。

module white_black/ruins
abstract sig 場所 {}

sig 部屋 extends 場所 {
  白: one 場所,
  黒: one 場所
} {
  白 != 黒
}

one sig 入口 extends 部屋 {}

one sig 目の部屋 extends 部屋 {}

one sig 出口 extends 場所 {}
one sig ニポポング extends 場所 {}

fact {
}

pred 遺跡 {
  // 長老の経路
  入口.白.黒.黒.白 = 出口
  // 長老の兄の経路
  入口.黒.白.白.黒 = 出口
  // 遺跡に「喰われた」人の経路
  入口.白.黒.白.黒 = ニポポング

  入口.白.黒 = 目の部屋
  // 長老の兄の経路のどこかに目の部屋がある
  目の部屋 in (入口.黒 + 入口.黒.白 + 入口.黒.白.白)
}

run 遺跡 for 12 部屋

assert 黒が目の部屋 {
  遺跡 => 目の部屋 = 入口.黒
}
check 黒が目の部屋 for 12部屋

assert 白白黒黒で出口 {
  遺跡 => 入口.白.白.黒.黒 = 出口
}
check 白白黒黒で出口 for 12部屋

まず入口と出口、「喰われた」人が飛ばされるニポポングも含める signature として場所を定義して、遺跡の部屋はこれを継承します。遺跡の入口も白と黒の扉があるという意味で部屋の一種としたのですが、扉の先が入口になるのでこれがありえるかどうかは文中の記述では明確ではないように思います。
また出口も、長老と長老の兄が辿りついた出口と、ニポポングの2箇所だけ設定しましたが、その他の出口が存在する可能性も否定はされていないのですが、多分それを入れると発散します。

とりあえず遺跡の特徴とわかっている経路、「目の部屋の証言から、長老兄の経路のどこが「目」の部屋だったかについて検証してみたところ、「黒が目の部屋」は check をパスしました。文中で魔術師と弟子が検証した結果は正確だったようです。

つぎに第1章の最後で「白白黒黒」で出口に到着するはず、というのを検証してみたら、以下のような反例が出てしまいました。

入口から入口に戻ってきてしまっていますね。しかし経路と目の部屋の証言については一致しています。また他にも扉の先がその部屋自身であるという構造があります。これは文中では明示的には禁止されていないと思います。白と黒の扉の先が「たがいに」同じ場所であることはない、とありますが、扉の先がその部屋自身ではないという制約は書かれていません……。が、多分その制約は自明のこととして含まれていると解釈して pred 遺跡に以下の制約を追加してみます。

  // 扉の先が同じ部屋ではないという制約も入れてみる
  all room: 部屋 | room.白 != room
  all room: 部屋 | room.黒 != room

ところがまだ反例が出てしまいます。

「目」の部屋と、入口から白の扉の先の部屋が互いに黒の扉で往復できるようになっていますね。
遺跡の制約としてはこの構造は禁止されないと思います。多分「目」の部屋が経路に1回しか現れないという制約が必要なのではないかと思います。が、明示的に目の部屋を他に通らなかったと証言されていないのでどうも「白白黒黒」を辿るのは危険だったのではないかという気も……。