Files」のようにスペースの入っているパスだと、rjbのビルドに失敗するようなので2行パッチ。Alloyで知識論理を使って論理パズルを解くbonotakeさんの日記で時々取り上げられているAlloy、パズルを解くのに便利とのことなので、ちょっと週末に遊んでみた。対象とするのは、以前にSPASSで知識の論理を使って論理パズルを解く?でも取りあげた「赤いぼうし」の問題で、これは以下のような問題。AさんとBさんがいて、少なくとも一人は赤い帽子を被っていて、赤い帽子を被っていない人は白い帽子を被っている。二人とも他人の帽子の色は分かるが、自分の被っている帽子の色は分からない。Aさんが「自分の帽子の色が分からない」と発言した。Bさんは自分の被っている帽子の色が分かるか?この前提となる状況をAlloyでは以下のようにモデル化することが出来る。世界の集合を外延として持つ。Wこれを実行すると以下のような結果とモデルが得られる。29ms.B_wears_a_redhatが成り立っている世界があるので、Bさんの帽子がちゃんと決まるとしたら、それは赤の帽子。assertとcheckを使って反例がないかをチェックする。19ms.結果、反例は見つからなかった。大きなモデルに反例がある可能性はあるけど、まあこの場合には多分大丈夫だろう。次に、Bさんが「自分は赤い帽子を被っている」ことを知っているかもチェック。30ms.やはり反例は見つからない。いうわけで、どうやらBさんの被っているのは赤い帽子で、しかもBさんもそのことを知っているようです。冬らしい寒々とした風景をもう少し味わいたかったが、昨日の雪はもうあらかた解けてしまって残念。最終発表会打ち上げ萩野・服部研の最終発表会後の打ち上げに参加。おっぱいチョコ某会の新人歓迎のゲームで、「おっぱいチョコ」なるものを貰った。いうのを考える人はすごいなぁ。