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

しつこくまだ第1章です。いや、どうも検証がうまくいかないんです。

あれから、「目」の部屋が長老の経路で1回しか通らなかった(他の部屋には「目」がなかったという暗黙の証言があったとする)という制約や、扉の先が入口に戻ることがないという制約などを加えてみたのですが「白白黒黒」で出口に辿り着かない構造がどうしてもできてしまうんですよね。

現在の 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 (入口.黒 + 入口.黒.白 + 入口.黒.白.白)

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

  // 長老の経路に目の部屋は1回だけだったという制約も入れてみる
  not 目の部屋 in 入口.白 + 入口.白.黒.黒
}

run 遺跡 for 12 部屋

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

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

おそらく、扉で繋がっている部屋同士に互いに通じるような循環した構造はない、という前提が必要なんだと思いますが、本文を読んでもどうもそういう制約があるようには思えないので、これは暗黙の条件なのではないかという気がします。
Alloy はこういう無意識のうちに置いてしまう前提条件をあぶり出すのにはよいツールですね。

いいかげんそろそろ次は第2章に進もうと思います。