うみねこのなく頃に をAlloyで解く

なーんて嘘です（のっけから…）。 実際には解けませんでした。
先週あたり、「うみねこのなく頃に」EP2の密室トリックが解けないかと思ってベッドの中で無駄な努力をしてました。

Alloyとはいわゆる仕様記述言語でありますが、処理系にSATソルバを備えておりまして。逆に、SATソルバ操作言語だと思えばいろんな用途に使えます。自分はもっぱらパズル解くのに利用し（ｒｙ
バックエンドのカラクリとか細部は全然違いますが、自分の中ではMONA（OSでもAAでもないやつ）と同じカテゴリに属しています。MONAよりUIが整備された感じ。

ということで、その無駄なあがきの痕跡は以下。元の「うみねこ」での密室の定義とかは説明しませんが、朱志香（←ネタバレ防止のため色を変えてます）の死んでた部屋です。

// 部屋の内外の状況
sig Room {
  people: set Person,
  keys: set Key,
  door, window: Exit,
  next: Room  -- shift後の状況
}
{
  #people > 0
  shift[this, next]
}

// 出口
fun exit (r: Room): Exit {
  r.door + r.window
}

sig Person {
  inside: lone Bool
}

sig Key {
  inside: lone Bool
}

sig Exit {
  opened: lone Bool
}

sig Bool {}

fact {
 #Bool <= 1
}

// 人・鍵の移動、ドアや窓の開け閉めによる部屋周りの状況変化
//  r ... 変化前、r' ... 変化後
pred shift (r, r': Room) {
  #(r.people) = #(r'.people)
  #(r.keys) = #(r'.keys)
  peopleOut[r, r'] implies some r'.exit.opened
  keyIn[r, r'] implies some r'.exit.opened
  lockDoor[r, r'] implies 
		some r'.people.inside
		or some k: r'.keys | no k.inside
  lockWindow[r, r'] implies 
		some r'.people.inside
}

// ドアが施錠
pred lockDoor (r, r': Room) {
  some r.door.opened && no r'.door.opened
}

// 窓が施錠
pred lockWindow (r, r': Room) {
  some r.window.opened && no r'.window.opened
}

// 人が部屋から出て行く
pred peopleOut (r, r': Room) {
  #{ p: r.people | some p.inside } > #{ p: r'.people | some p.inside }
  
}

// 鍵が部屋の中に入る
pred keyIn (r, r': Room) {
  #{ k: r.keys | some k.inside } < #{ k: r'.keys | some k.inside }
}

// 密室の定義
pred closed (r: Room) {
  no (r.door + r.window).opened
  all p: r.people | no p.inside
  #{ k: r.keys | some k.inside } = 2
}

// 定義した状況の変化によって密室状況ができるか？
pred p1 (disj r, r': Room) {
  #keys = 2
  (some p: r.people | some p.inside) or (some e: r.exit | some e.opened)
  r' in r.^next
  closed[r']
}

run p1 for 5

（以降は「うみねこ」読者向け）これ、鍵の数が2本だとアウト。他のマスターキーが使われたと仮定して、鍵の数を増やしてみるとあっさりOK。…人間が頭ですぐ思いつくのと同じ結果が出ましたorz
他の鍵が使われたか、あるいは密室の定義を額面どおりにとってはいけないということなんでしょうなー。

まぁ密室は解けませんでしたが、なんとなく全体のルールは（以前よりは）見えてきた印象。あんまり世間では言われてなさそうだけど、個人的には飴玉とかマシュマロが6人の殺人を引き起こした何か（鍵？）なんじゃないかと思ってたり。もし最初の殺人者がEP1では絵羽、EP2では楼座だったらという前提ですが。