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を追加してはいけない」になる。