Alloyで言語女子会殺人事件2

またPHPが殺されました。

ルール

登場人物は、読者、Python、PHP、Ruby、Perl、JSの6人。
PHP, 読者は犯人ではない。殺害のチャンスは1度だけ。犯人は犯行時刻にPHPと一緒にいた。犯人は「自分以外はみな自分が犯人だと考えない」と考えて犯行に及んだ。
登場人物は自分以外の誰かに自分がどこに行くつもりかを事前に伝えた。
途中で気が変わって変更した人もいるが、犯人以外は最後に宣言した通りに行動した。

読者(Me)の視点

PHP殺害が発覚する

Me「RubyはPHPと一緒に裏山に行ったはず。怪しい。あとPythonの足取りがつかめない。怪しい。」

Rubyの視点

Ruby「私は犯人じゃない。犯人はPythonよ！」

Ruby「私はPHPと裏山に行く話はしたわ。でもPHPは来なかったのよ。Pythonがどこに行っていたのかわからないからPythonが犯人よ」
Me (…アリバイはなさそうね…)

Pythonの視点

Python「私は犯人じゃない。犯人はRubyよ！」

Python「私は確かに一度、裏山に行くってPHPに話したわ。だけどそのあとPerlやJSと一緒に海岸に行くことにしたの。Perlに聞いて。アリバイを証明してくれるわ。そもそも順当に考えて最初からPHPと一緒に行く予定で、アリバイのないRubyが犯人でしょう？」

全員の意見を総合すると

Me「…解けなくない？」
Ruby「解けないよね…」
Python「さっきはっきり言わなかったけど、私は『Perlは裏山に来たけどJSは来ていない』ってこと知ってるからJSが犯人には絞れるけど…」
Me「でもそういう条件を追加しないで、3人の意見を総合したら解けるって話じゃなかった？」
Ruby「ちょっと責任者でてこい！」

解けない？

Alloy「え？解けない？」
Me「解けないよ」
Alloy「そんなはずは…ちょっと3人分の意見をまとめた結果、最終時刻にどう判断しているか確認してみましょう」

Alloy「ほら、ちゃんと犯人であるJSだけがどこに行っていたのかわからないという結論が…え？それはおかしいな。そもそも複数ヶ所に存在している人がいるのはおかしい…あーっ」
Me「！」
Alloy「ごめん、今回追加した『3人分の視点を総合する』ってコードのところで、最後の殺害時刻の制約を記述するのを忘れてたわ！」
Me「え、バグってこと？」
Alloy「そうよ！」
Me「これはひどい」
Python「これはひどい」
Ruby「これはひどい」

まとめ

PHP「何がひどいって、また私が殺され役なところ…」
Python (スルー)
Ruby (スルー)
Alloy「今回、読者の視点もモデルに入れて『パズルとして解けるミステリー』を目指してみたんだけど、一つわかったことがあるの」
JS「なになに？」
Alloy「ざっくり言うとミステリーというものを『ある知識が与えられて、その知識を元に推論した結果、結論Xに到達して、それから語られていなかった事実が明らかになって、それによって結論Xが間違いだと判明し、結論Yに到達する』という過程としてモデリングしたんだけど」
JS「うんうん」
Alloy「その結論Yを出した後に別の事実が明らかになって結論Yが覆る可能性を否定出来ないからパズルとして解が一意に定まりようがないと思うの」
Python「客観的な物証で犯人が一意に定まるようにすればいいんじゃないの？」
Alloy「本当に客観的な物証からの推論なら、最初の結論Xが覆るはずがないの。客観的な物証だと思っていたものが、実は主観的な『解釈』でした、という形にしないとどんでん返しは起きなくて、それを認めたらそのどんでん返しが今後も起こることを否定出来ないの」
Python「なるほど…」
JS「あ、でも私、論理的にどんどん可能性が絞られていった挙句、犯行が可能な人がいなくなる、って小説を読んだことあるよ」
Alloy「えっ、それはどういう仕組みなの？」
JS「主人公が精神病で、お話は全部妄想でした、というオチ」
Alloy「ええー」
JS「ミステリーの価値は論理的に正しいかどうかだけで決まるわけじゃないってことね」
Alloy「まあそうかもしれないけど…それだと私の出番がないじゃない…」
JS「まあ、途中まで論理的に進みつつ最後のオチが『バグでした』でもいーんじゃない？」
Alloy「ぐぬぬ…」

ソースコード

open util/ordering[Time]

//登場人物
abstract sig Person {
  belief: Person -> Person -> Place -> Time,
  // 最終的にどこへ行ったか
  real_place: Place -> Time,
  is_killer: lone Person // as bool
}{
  all t: Time | lone real_place.t
}

one sig Me extends Person{} // 読者
one sig PHP extends Person{} // 殺され役
one sig Perl extends Person{}
one sig Python extends Person{}
one sig Ruby extends Person{}
one sig JS extends Person{}

abstract sig Time {}
sig BeforeMardar extends Time {
  // 各時刻に誰かが誰かに自分がどこに行くかを伝える
  who: some Person,
  targets: some Person,
  where: Place
}{
  // 話し手は聞き手に含まれる
  who in targets
  // 聞き手が話し手と同一ではいけない
  some targets - who
}
one sig Mardar extends Time {}

sig Place {}

fact {
  // 同じ人が複数箇所に存在すると信じることはない
  all p1, p2, p3: Person, t: Time{
    lone (p1.belief)[p2, p3].t
  }
}

pred init(t: Time){
  all p: Person {
    no p.belief.t
  }
  all p: Person {
    no p.real_place.t
  }
}

pred no_change(t: Time, changable: univ -> Time){
  changable.t = changable.(t.prev)
}

pred step(t2, t: Time){
  all p: Person {
    (p in t.targets) => {
      // 聞いた人pの信念が上書きされる
      // 一緒に聞いていた人(自分を含む)の信念が上書きされる
      all p2: Person {
        (p2 in t.targets) => {
          p.belief[p2].t = p.belief[p2].t2 ++ (t.who -> t.where)
        }else{
          // それ以外は変化しない
          p.belief[p2].t = p.belief[p2].t2
        }
      }
    }else{
      // 聞き手以外は信念が変化しない
      p.belief.t = p.belief.t2
    }
    (p in t.who) => {
      // 犯人以外は自分が言ったところに行く(嘘はつかない)
      (no p.is_killer) => p.real_place.t = t.where
    }else{
      p.real_place.t = p.real_place.t2
    }
  }
}

pred on_mardar(t2, t: Time){
  all p: Person {
    let go = real_place.t2,
        place = p.go, 
        meets = go.place {
      // 全員どこかには行った
      one place
      p.real_place.t = place // 犯行時刻にそこにいた
      // 犯行時刻に同じ場所に行った人は信念が更新される
      p.belief[p].t = p.belief[p].t2 ++ (meets -> place)
    }
  }
  // 犯人と殺され役だけが犯行時刻に同じ場所にいた
  PHP.real_place.t.~(real_place.t) = PHP + (is_killer.univ)
}

fact {
  BeforeMardar = Mardar.prevs
  init[first]
  all t: BeforeMardar - first{
    step[t.prev, t]
  }
  on_mardar[Mardar.prev, Mardar]
}

// whoと同じ場所にいた可能性があるのは？
fun same_place(self: Person, who: Person): Person{
  let where = (self.belief)[self].last {
    who.where.~where + {p: Person | no p.where} - who
  }
}


run {
  one is_killer // 犯人は一人だけ
  // Ruby, Python, 読者はPHPがどこに行くつもりか聞いた
  all p: Ruby + Python + Me {
    some t: Time {
      PHP in t.who and p in t.targets
    }
  }
  // Ruby, Python, PHP, 読者は犯人ではない
  no (Ruby + Python + Me + PHP).is_killer
  // 犯人は自分以外はみな自分が犯人だと考えないと考えている
  let killer = is_killer.univ {
    all other: Person - killer - PHP{
      let where = (killer.belief)[other].last {
        killer not in PHP.where.~where
      }
    }
  }
  // 読者は当初PythonかRubyが犯人だと考えている
  same_place[Me, PHP] = Python + Ruby
  // RubyはPythonが犯人だと、PythonはRubyが犯人だと考えている
  same_place[Ruby, PHP] = Python
  same_place[Python, PHP] = Ruby
  // 読者がPythonとRubyの話を聞いた後、正しく犯人を当てられる
  // 3人分の意見を聞いている架空の人の信念を考える
  some belief: Person -> Place -> Time {
    no belief.first
    all t: BeforeMardar - first{
      let t2 = t.prev{
        (some (Me + Python + Ruby) & t.targets) => {
          // 三人の誰かが聞いていれば信念が上書きされる
          belief.t = belief.t2 ++ (t.who -> t.where)
        }else{
          // 信念が変化しない
          belief.t = belief.t2
        }
      }
    }
    // バグ: ここに最終時刻での信念の更新に関する制約を書く必要があった
    // 3人分の意見をまとめた結果、犯人を正しく推測できる
    let who = PHP, where = belief.last {
      (who.where.~where + {p: Person | no p.where} - who)
      = is_killer.univ
    }
  }
} for 6 Time, 4 Place