うみねこのなく頃に8 のベルンの挑戦のAlloyモデル

umineko8challenge.als

// うみねこのなく頃に8 のベルンの挑戦のAlloyモデル
abstract sig Person { kill : set Person }
one sig
  Krauss, Natsuhi, Jessica,
  Eva, Hideyoshi, George, 
  Rudolf, Kyrie, Battler,
  Rosa, Maria,
  Nanjo,
  Genji, Shannon, Kanon, Gouda, Kumasawa
  extends Person {}

pred murderer[p : Person] { some p.kill }
pred honest[p : Person] { not murderer[p] }

pred adult[p : Person] {
  p in Krauss+Natsuhi+Eva+Hideyoshi+Rudolf+Kyrie+Rosa+Nanjo+Genji+Kumasawa
}
pred child[p : Person] { not adult[p] }

pred dead[p : Person] { some p.~kill }
pred alive[p : Person] { not dead[p] }

// 基本的な事実
fact {
  // 犯人が死ぬことはない
  all p : Person { murderer[p] => not dead[p] }
}

// 第一の晩の時点でマスターキーを持っている人
sig KeyHolders1 in Person {}
fact { KeyHolders1 = Genji+Shannon+Kanon+Gouda+Kumasawa }
// 第二の晩の時点でマスターキーを持っている人
sig KeyHolders2 in KeyHolders1 {}
// 第五の晩の時点でマスターキーを持っている人
sig KeyHolders5 in KeyHolders2 {}

// 第一の晩で食堂内にいた人
sig Room1 in Person {}
// 第一の晩で適切にロックされていたならば、ロックした人
lone sig Room1LockedBy in Person {}

// 第二の晩で部屋の中にいた人
sig Room2 in Person {}
// 第二の晩でロックされていたなら、ロックをかけた人
lone sig Room2LockedBy in Person {}

// 第一の晩
fact {
  // 鍵をかけられるのは、鍵を持っている人か、中にいる犯人
  all p : Room1LockedBy {
     p in KeyHolders1 + Room1
     murderer[p]
  }

  // 郷田: 食堂は施錠されていました / マスターキーで扉を開けると
  honest[Gouda] => some Room1LockedBy
  // 熊沢: そこに私が来たのです / 贈ｫの計6人が血塗れになって倒れていたのでございます
  honest[Kumasawa] => {
    not (Kumasawa in Room1)
    (Eva+Hideyoshi+Rudolf+Kyrie+Rosa+Genji) in Room1
  }
  // 蔵臼: 全員が食堂に集まった
  // ???
  // シャノン: お子様方はそれぞれ、自分の親が間違いなく死んでいることを
  // 確認なさいました。
  (honest[Nanjo] and honest[Shannon]) => {
    honest[Battler] => (dead[Rudolf] and dead[Kyrie])
    honest[George] => (dead[Eva] and dead[Hideyoshi])
    honest[Maria] => dead[Rosa]
  }
  // 嘉音: 僕と南條先生は、源次様が死んでいることを確認しました。
  (honest[Nanjo] and honest[Kanon]) => dead[Genji]
  // 南條: 私でなくとも、誰も検死は誤りません
  // (検視の条件にhonest[Nanjo]を追加して表現)
  // 真里亞: 犠牲者はみんな即死
  // 誰が犠牲者とは言っていない?
  (honest[Nanjo] and honest[Maria]) => {
    //all p : Eva+Hideyoshi+Rudolf+Kyrie+Rosa+Genji | dead[p]
  }
  // 蔵臼: 食堂内を調べた結果、扉も窓も、全て施錠され、密室であったことがわかった。
  honest[Krauss] => some Room1LockedBy
  // 戦人: 食堂内から、不審なものは何も見つからなかった。
  // ???
  // 譲治: 食堂内に何者かが隠れているということもなかったよ。
  honest[George] => Room1 = Rudolf+Kyrie+Eva+Hideyoshi+Rosa+Genji
  // 蔵臼: 誰も隠れていないことは明白だ。
  honest[Krauss] => Room1 = Rudolf+Kyrie+Eva+Hideyoshi+Rosa+Genji

  // 夏妃: 源次のマスターキーを破壊しておきました。
  honest[Natsuhi] =>
    KeyHolders2 = KeyHolders1 - Genji
  else
    KeyHolders2 = KeyHolders1

  // 死んだはずの人は死んでるか犯人
  all p : Eva+Hideyoshi+Rudolf+Kyrie+Rosa+Genji | dead[p] or murderer[p]
}

// 第二の晩
fact {
  // 鍵をかけられるのは、鍵を持っている人か、中にいる犯人
  all p : Room2LockedBy {
     p in KeyHolders2 + Room2
     murderer[p]
  }

  // ト書き: 蔵臼夫妻だけが戻ってこない
  // すなわち以下の人物は部屋の中にはいなかった
  no p : Jessica+George+Battler+Maria+Nanjo+Shannon+Kanon+Gouda+Kumasawa | p in Room2
  // 郷田: 奥様の部屋は施錠されておりました。
  honest[Gouda] => some Room2LockedBy
  // 紗音: 私が鍵を開けました。
  honest[Shannon] => some Room2LockedBy
  // 嘉音: 部屋の中には、蔵臼さまと夏妃さまが倒れていました。
  honest[Kanon] => Krauss+Natsuhi in Room2
  // 戦人: 南條先生がすぐに脈を取ったぜ。そして、二人とも即死だったと宣言した。
  (honest[Battler] and honest[Nanjo]) => (dead[Krauss] and dead[Natsuhi])
  // 南條: 私が二人の死亡を確認しました。あれは間違いなく即死でした。
  honest[Nanjo] => (dead[Krauss] and dead[Natsuhi])
  // 朱志香: 窓も扉も完全に施錠されていて、密室だったことがわかった。
  honest[Jessica] => some Room2LockedBy
  // 紗音: 私たち使用人全員は、常に一緒におりました。
  // 嘉音: 僕たち使用人全員は、それぞれが使用人全員のアリバイを証明できます。
  (honest[Shannon] or honest[Kanon]) => {
    no ((Krauss+Natsuhi) & (Shannon+Kanon+Gouda+Kumasawa).kill)
    no p : Shannon+Kanon+Gouda+Kumasawa | p in Room2LockedBy
  }

  // 真里亞: 外からガムテープでベタベタと、窓や扉を封印したよ。
  // 朱志香: 警察がくるまで絶対、誰の出入りも出来ないようにした！
  // 赤: 一同は退出と同時に部屋を封印した。その退出に犯人は加われない。
  // 赤: 全ての封印は、決して破られることはない
  // = 中にいた人は以降の殺人を犯せない
  Room2.kill in Room1+Room2

  // 戦人: 俺達はさらに食堂も同様に封印した。
  // 南條: 屋敷自体にも封印をし、私たちは全員、ゲストハウスへ避難しました。
  // = ただし、第一の晩の犯人は脱出可能なので制約にはならない

  // 赤: 第一の晩の犯人は確実に6人を殺している
  some disj a, b, c, d, e, f : Room1.~kill.kill & (Room1+Room2) {
    // 冗長だけど、warningを消すために残しておく
    all p : a+b+c+d+e+f | dead[p]
  }

  // 死んだはずの人は死んでるか犯人
  all p : Krauss+Natsuhi | dead[p] or murderer[p]
}

// 第四の晩
fact {
  // 譲治: 僕は彼女が死んでいることを認めなければならなかった
  (honest[Nanjo] and honest[George]) => dead[Shannon]
  // 南條: 私も検死し、彼女の死亡を確認しました
  honest[Nanjo] => dead[Shannon]
  // 郷田: 私たちにはみんなアリバイがないのです
  // ???
  // 朱志香: 紗音殺しに限って言えば譲治兄さんにはできない
  honest[Jessica] => not Shannon in George.kill
  //  戦人: 譲治の兄貴以外なら誰にでも殺せたわけだ
  // ???
  // 郷田: 紗音さんの持っていたマスターキーは、その場で破壊しました。
  // 赤: 嘉音のマスターキーも破壊されたものとして扱うわ。
  honest[Gouda] =>
    KeyHolders5 = KeyHolders2 - Kanon - Shannon
  else
    KeyHolders5 = KeyHolders2 - Kanon
  // 赤: 以後、嘉音は殺されたものとして扱う。
  // 犯人は死なないので
  //dead[Kanon]
  no Kanon.kill

  // 死んだはずの人は死んでるか犯人
  dead[Shannon] or murderer[Shannon]
}

// 第五の晩・第六の晩
fact {
  // 南條: 郷田さんも熊沢さんも、この傷では即死
  honest[Nanjo] => (dead[Gouda] and dead[Kumasawa])
  // 朱志香: 死んでるよ、郷田さんも熊沢さんも
  (honest[Nanjo] and honest[Jessica]) => (dead[Gouda] and dead[Kumasawa])
  // 戦人: 俺たち全員、アリバイがない。
  // 朱志香: いとこ4人と南條先生には、郷田さんと熊沢さんは殺せない。
  honest[Jessica] => no ((Gouda+Kumasawa) & (Maria+George+Battler+Jessica+Nanjo).kill)
  // 譲治: ゲストハウスの戸締りは完璧だったよ。
  // = 中の人もしくは鍵を持っている人に犯人がいる
  honest[George] => some p : Maria+George+Battler+Jessica+Nanjo+KeyHolders5 | murderer[p]
  // 戦人: マスターキーは、もうここで死んでる2人の2本以外、存在しない。
  honest[Battler] => KeyHolders5=Gouda+Kumasawa

  // 死んだはずの人は死んでるか犯人
  all p : Gouda+Kumasawa | dead[p] or murderer[p]
}

lone sig Locked7 {}

// 第7の晩
fact {
  // ト書き: そして、今度は南條先生が殺された
  dead[Nanjo]
  // 朱志香: し、死んでる…。殺されてる……!
  (honest[Nanjo] and honest[Jessica]) => dead[Nanjo]
  // 譲治: これは即死だったに違いない
  (honest[Nanjo] and honest[George]) => dead[Nanjo]
  // 真里亞: 戸締りは完璧だよ
  // = 内側の誰かがウソをついている
  honest[Maria] => (murderer[Battler] or murderer[Jessica] or murderer[George])
  // 朱志香: 私にも真里亞にも、戦人にも譲治兄さんにも、南條先生は殺せない！
  honest[Jessica] => not Nanjo in (Jessica+Maria+Battler+George).kill
  // 譲治: ゲストハウス内で南條先生を殺すことは不可能
  // = 何の制約にもならない?
  // 戦人: 南條先生がゲストハウスを出ていない証拠だ…！
  // = これも何の制約にもならない?

  // 死んだはずの人は死んでるか犯人
  all p : Nanjo | dead[p] or murderer[p]
}

// 第8の晩
fact {
  // ト書き: それは誰が見ても一目でわかる、無残な死体だった……。
  dead[Jessica]
  // 譲治: 即死だったろう
  (honest[Nanjo] and honest[George]) => dead[Jessica]
  // 真里亞: これで生きているわけがない
  (honest[Nanjo] and honest[Maria]) => dead[Jessica]
  // 戦人: 俺も譲治の兄貴も真里亞も、朱志香は殺せねぇぞ
  // 真里亞: 私たち3人に朱志香は殺せない
  (honest[Battler] or honest[Maria]) => not Jessica in (Maria+George+Battler).kill
  // 譲治: 真里亞ちゃんには誰も殺せないよ
  honest[George] => honest[Maria]
  // 真里亞: 譲治お兄ちゃんだって、大人は殺せないよ。子供は殺せるけれど
  honest[Maria] => all p : George.kill | child[p]
  // ト書き: 譲治、戦人、真里亞には、朱志香は殺せない。
  not Jessica in (Battler+George+Maria).kill

  // 死んだはずの人は死んでるか犯人
  all p : Jessica | dead[p] or murderer[p]

  // 最後にこの3人は生き残っている
  alive[Battler]
  alive[Maria]
  alive[George]
}

// 同じ人を複数人で殺せない
pred condition1 { all p : Person | lone p.~kill }

// 譲治は嘉音を殺せない
pred condition2 { not George->Kanon in kill }

// 第一の晩の犯人の中には1人で6人殺している人がいる
pred condition3 {
  some k : Room1.~kill {
    some disj a, b, c, d, e, f : k.kill & (Room1+Room2) {
      // 冗長だけど、warningを消すために残しておく
      all p : a+b+c+d+e+f | dead[p]
    }
  }
}

pred show {}
run show

assert BattlerIsMurderer {
  murderer[Battler]
}
check BattlerIsMurderer

pred show2 {
  condition1
  condition2
  condition3
}
run show2

assert BattlerIsMurderer2 {
  condition1 and condition2 and condition3 => murderer[Battler]
}
check BattlerIsMurderer2

pred test {
  condition1
  //condition2
  condition3
  honest[Battler]
}
run test