hatena
<body>
*1335233091*Alloyで言語女子会殺人事件2
またPHPが殺されました。
** ルール
登場人物は、読者、Python、PHP、Ruby、Perl、JSの6人。
PHP, 読者は犯人ではない。殺害のチャンスは1度だけ。犯人は犯行時刻にPHPと一緒にいた。犯人は「自分以外はみな自分が犯人だと考えない」と考えて犯行に及んだ。
登場人物は自分以外の誰かに自分がどこに行くつもりかを事前に伝えた。
途中で気が変わって変更した人もいるが、犯人以外は最後に宣言した通りに行動した。
** 読者(Me)の視点
-7:00 Me, Perl, JS「河川敷へ行く」聞いていた人= Me, Perl, Python, Ruby, JS
-11:00 PHP, Ruby「裏山へ行く」聞いていた人= Me, PHP, Perl, Python, Ruby
** PHP殺害が発覚する
Me「RubyはPHPと一緒に裏山に行ったはず。怪しい。あとPythonの足取りがつかめない。怪しい。」
** Rubyの視点
Ruby「私は犯人じゃない。犯人はPythonよ！」
-7:00 Me, Perl, JS「河川敷へ行く」聞いていた人= Me, Perl, Python, Ruby, JS
-8:00 PHP「公園へ行く」聞いていた人= PHP, Ruby, JS
-11:00 PHP, Ruby「裏山へ行く」聞いていた人= Me, PHP, Perl, Python, Ruby
Ruby「私はPHPと裏山に行く話はしたわ。でもPHPは来なかったのよ。Pythonがどこに行っていたのかわからないからPythonが犯人よ」
Me (…アリバイはなさそうね…)
** Pythonの視点
Python「私は犯人じゃない。犯人はRubyよ！」
-7:00 Me, Perl, JS「河川敷へ行く」聞いていた人= Me, Perl, Python, Ruby, JS
-9:00 Python「裏山へ行く」聞いていた人= PHP, Python
-10:00 Perl, Python, JS「海岸へ行く」聞いていた人= PHP, Perl, Python, JS
-11:00 PHP, Ruby「裏山へ行く」聞いていた人= Me, PHP, Perl, Python, Ruby
Python「私は確かに一度、裏山に行くってPHPに話したわ。だけどそのあとPerlやJSと一緒に海岸に行くことにしたの。Perlに聞いて。アリバイを証明してくれるわ。そもそも順当に考えて最初からPHPと一緒に行く予定で、アリバイのないRubyが犯人でしょう？」
** 全員の意見を総合すると
-7:00 Me, Perl, JS「河川敷へ行く」聞いていた人= Me, Perl, Python, Ruby, JS
-8:00 PHP「公園へ行く」聞いていた人= PHP, Ruby, JS
-9:00 Python「裏山へ行く」聞いていた人= PHP, Python
-10:00 Perl, Python, JS「海岸へ行く」聞いていた人= PHP, Perl, Python, JS
-11:00 PHP, Ruby「裏山へ行く」聞いていた人= Me, PHP, Perl, Python, Ruby
Me「…解けなくない？」
Ruby「解けないよね…」
Python「さっきはっきり言わなかったけど、私は『Perlは裏山に来たけどJSは来ていない』ってこと知ってるからJSが犯人には絞れるけど…」
Me「でもそういう条件を追加しないで、3人の意見を総合したら解けるって話じゃなかった？」
Ruby「ちょっと責任者でてこい！」
** 解けない？
Alloy「え？解けない？」
Me「解けないよ」
Alloy「そんなはずは…ちょっと3人分の意見をまとめた結果、最終時刻にどう判断しているか確認してみましょう」
[f:id:nishiohirokazu:20120424110809p:image]
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「ぐぬぬ…」
** ソースコード
>|javascript|
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
||<
*1335276581*Alloyで次にしたいこと
ミステリーのネタの生成は、いま時系列的な変化を入れてるけど、それはあんまり重要ではない気がする。それより「どこにいた」などの「客観的な証拠」と、嘘を付いている可能性や誤解の可能性のある「主観的な証言」を区別するべきだな。
最初Aの証言を聞いて、Aが嘘をついていないと仮定すると犯人がBで、次にBの証言を聞いて、その証言単独でBが嘘をついていないと仮定するとAが犯人で、両方あわせて考えるとCが犯人で…とか。あとは意図的な嘘と、誤解に基づいた誤情報や、曖昧な表現(Aが「場所Xにいた」と主張してBが「その時刻にAに会った」と言った場合、Bが正直であってもXにいたとは限らない。Aが嘘を付いている可能性がある)とか。
解が一意になるパズルの生成は、ミステリーのよりももっとシンプルなもので考えないとなと思う。3人の人がいて、ウソを付くのは1人だけで、Xは「Zが嘘つき」Yは「Zが嘘つき」と言う場合、嘘つきはZに定まる。この推論の過程では何が起こっているか。
Alloy自体をAlloyでモデリングする必要があるかなー。
現実のモデリング路線ではもっかアウトオブオーダー実行が課題。命令のキューを用意して、命令をキューに入れることを1つの時刻でのステップに割り当てるとよいのではないかと考えている。キューの中身はランダムに実行される。それをキューって呼ぶのかという気はするが。キューに入れていいかどうかの制約でR→Rの制約とかを記述できると思う。「Read→Readの順序が保存される」は「キューにReadが入っている時にはReadを追加してはいけない」になる。
</body>