Alloyでパズル (11) かけっこのパズル

Alloyでパズル(1) と変わらないようにしか見えない かけっこのパズル。
でも書いている人が人だし、自分が何か見落としているのかもしれない。

問題

一郎、二郎、三郎の三人で駆けっこをして、その結果を次のように言っています。

一郎：「僕は一番じゃない」
二郎：「僕は一番だ」
三郎：「僕は二番だ」

三人のなかで一人だけウソをついています。それは誰でしょう？

リスト

普通のウソつきパズルだった。
何か自分的に新規要素をと思ってseqを使ってもみたが、順位が 0,1,2 になって読みづらいのでやめた。
sig Raceとか別建てしてみたがかえってややこしくなるだけだったのでやめた。

// かけっこのパズル
abstract sig Runner { ranking: disj (1+2+3) }
one sig Ichiro, Jiro, Saburo extends Runner {}
sig Lier in Runner {}
fact {
    one Lier
    Ichiro not in Lier <=> Ichiro.ranking!=1
    Jiro not in Lier <=> Jiro.ranking=1
    Saburo not in Lier <=> Saburo.ranking=2
}
run {}

結果的には、ルートシグネチャ１種類＆enum不使用しばり くらいが牛と違うところか。
１ヶ月以上前に書いたものから何も進歩していないのが、なんか悔しい。

結果

参考

• bonotakeの日記 : かけっこのパズル revisited
• 檜山正幸のキマイラ飼育記 : 長男に教わったパズル