白と黒のとびら 第2章 帰郷 その2

というわけでガレットの故郷の神殿の構造について Alloy で検証してみます。

利用したコードはこちら。

module white_black/home_temple

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

one sig 入口 extends 部屋 {}

one sig 竜の部屋 extends 部屋 {}

pred 神殿 {
  // 祖父の経路
  入口.黒.白.白.黒 = 入口
  入口.黒 != 入口
  入口.黒.白 != 入口
  入口.黒.白.白 != 入口
  // 弟の経路より(竜の部屋は同一と考える)
  入口.白.黒 = 竜の部屋
  竜の部屋.黒.白 = 入口
  竜の部屋.黒 != 入口
  // 父の経路より
  入口.白.黒.白.白.白.黒 = 入口
  入口.白 != 入口
  入口.白.黒.白 != 入口
  入口.白.黒.白.白.白 != 入口
  入口.白.黒.白.白 = 竜の部屋
  入口.白.黒.白 = 入口.白.黒.白.白.白

  // 古代語に書かれてた詩の内容の解釈から(若干あいまいな制約ですが)
    入口.白.白 = 入口
    入口.黒.黒 = 入口

  // すべての部屋1回だけ通る経路が存在する
  // 最短経路を 部屋 -> 部屋の二項関係の集合 route として定義してみる
  some route: 白+黒 |
    // route の移動元には全ての部屋が1度だけ含まれる => 定義域と地域が部屋と一致し、全ての部屋からの移動先が1つだけ
    部屋.route = 部屋 and
    route.部屋 = 部屋 and
    all room: 部屋 | #room.route = 1 and
    // 入口から route を辿ると全ての部屋を通る(独立したループができず全体で一本道になるように)
    部屋 = 入口.^route
}

run 神殿 for 8 部屋

「全ての部屋を1回だけ通る経路が存在する」という制約をどうするかでしばし悩みました。Alloy本でよくやった順序をもつ時刻のシグネチャを導入して部屋を移動するイベントを作ることで重複がないことを示すようにしようかと思いましたが、それをやると複雑になるので、なんとか時間の概念なしに表現してみました。Alloy 本の付録 A の路線の表現の演習問題が参考になりました。

で、これを execute してみましたが、以下のような反例がありました。

線が密接しててみにくいですが、1部屋多いです。本文中には「左右対称なんじゃないか」とかあいまいな推測からくる条件を元に構造を推測しているので、まあ1つに限定できないのは想定済みではありますが、多分もうひとつの隠れた制約は「入口に戻る時に辿る白と黒の扉が偶数」というのだと思います。ルル語の文法にそういうのがあって、多分それも遺跡の構造と対応しているんでしょうね。

とりあえずこれで納得できたので次は第3章へ進みます。