かけっこのパズル revisited

Alloy本翻訳のレビュワー募集記事で、過去に自分が「かけっこのパズル」をAlloyで解いた記事を参照したのですが…
参考）

• 駆けっこのパズルを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のキーワード色づけされる日が来ないかな…

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