Alloy本翻訳のレビュワー募集記事で、過去に自分が「かけっこのパズル」をAlloyで解いた記事を参照したのですが…
参考)
今見直すと、なんかイマイチ。
特に、3人の嘘を見抜くのに、いちいち3回コマンド走らせないといけないのがダサい。
ということで、書き直してみました。
内容の詳細はコメント見てください。
-- かけっこ one sig FootRace { -- 順位の配列 runner: seq Person } { -- すべての人に順位が決まる runner in Int one -> Person } -- 一郎、二郎、三郎の宣言 enum Person { Ichiro, Jiro, Saburo } -- うそつきが一人 one sig Liar in Person {} -- 順位 fun rank (p: Person): Int { FootRace.runner.idxOf[p] } -- 「僕は一番じゃない」 pred word1(p: Person) { not p in Liar iff p.rank != 0 } -- 「僕は一番だ」 pred word2(p: Person) { not p in Liar iff p.rank = 0 } --「僕は二番だ」 pred word3(p: Person) { not p in Liar iff p.rank = 1 } -- 誰が嘘をついた? pred whoIsLiar { -- 一郎が word1 を発言 Ichiro.word1 -- 二郎が word2 を発言 Jiro.word2 -- 三郎が word3 を発言 Saburo.word3 } run whoIsLiar
うう、Alloyのキーワード色づけされる日が来ないかな…
てな感じで、実行結果のスクリーンショット。