うーん、命題を指標にするのかー。
と感心しつつ、自分も眠気覚ましに解いてみました。途中様相論理をものすごく使いたくなったけど、敢えて使わない方針で。ちょっと嘘くさいんだけど。
-- Aさん、Bさん abstract sig Person { wears: some Hat, -- 被っている帽子と思われるものの「集合」 } one sig A, B extends Person {} -- 帽子(赤を被らない人は白、はここの定義で言えている) abstract sig Hat {} sig RedHat, WhiteHat extends Hat {} fact Rules { -- 少なくとも一人は赤い帽子を被っている some p: Person | p.wears in RedHat -- 帽子の数は人数分 #Hat = 2 } -- (相手の帽子の色を)知っている pred knows(p: Person) { p.wears in RedHat || p.wears in WhiteHat }
様相論理を使わない代わりに、AさんとBさんが被ってる帽子 'wears' を集合にしてやりました。で、
- どの帽子を被ってるのがわかっている ⇔ wears の集合が、赤の帽子か白の帽子かのどちらかに含まれる
- どの帽子を被ってるのがわかっていない ⇔ wears の集合に、赤帽子も白帽子も含まれる
という勝手な解釈で。非決定性を扱うのにリストで表現するようなもんです(本当か?)
Alloyという言語は述語論理と集合論のミクスチャーなんで、そこいらへんうまく使い分けると便利。(逆に、初学者にはひたすら混乱の元になってる気もしなくもないですが)
で、モデルのインスタンスがあるかチェック…するんだけど、見た目的に面白くないので絵は省略。記述はたとえばこんな感じで。
pred show() { knows[B] } run show for 10
で、下記アサーションで反例なしです。
assert BsHatInRed { (knows[B] and not knows[A]) => B.wears in RedHat } check BsHatInRed for 8
んー、やっぱちょっと嘘くさいんですがね。きちんとした解は、元記事のさかいさんをご参考に。