bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

かけっこのパズル revisited

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のキーワード色づけされる日が来ないかな…

てな感じで、実行結果のスクリーンショット

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。