bonotakeの日記

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

駆けっこのパズルをAlloyで解く (Alloyチュートリアル風)

ここんとこハイペースで更新してますが、仕事が忙しいことからの逃避です。

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

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

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

引用元のコメントにも書きましたが、

モデルの存在/非存在に基づいて公理系(あるいはセオリー)の充足可能性をチェックするって話

ならば、モデル発見器の出番です*1。ということで、書いてみます。

ただまぁ、パズルとしては頭で考えたほうが明らかに&圧倒的に速そうなくらいシンプルな問題なので、Alloy Analyzerのモデル発見器としての使い方に重点をおいて、Alloyでの仕様の作り方を順を追って説明してみます。


まずは、3人が駆けっこする状況をぱぱっと書いてみます。

one sig FootRace {
  runner: seq Person
}

abstract sig Person {}
one sig Ichiro, Jiro, Saburo extends Person {}

sig ってのは指標で、Javaのクラスみたいなもんです。one ってのは、インスタンスが1個だけ、という意味です。abstract とか extends とかはJavaと同じような働きをします。
FootRaceは、かけっこした状況そのものを表します。Ichiro, Jiro, Saburoの三人が駆けっこして、それがrunnerに並びます。seq Person とは Person の配列のこと。具体的には、0以上のIntからPersonへの写像になります。

これで、次のような何も書いてない述語*2showを書いて、その述語が成り立つ状況下でのモデルを探します。

pred show() {}

run show

でてきたモデル。

Saburoの順番がないモデルが出てきました。つまり、runnerに対する制約が足りないと。

モデルが変なので、書き直します。以下のようにFootRaceの制約(二つ目の{}で囲まれている部分)をつけ足すと、IntからPersonへの対応が1対1になります。あんまりきれいな書き方じゃないんですが。

one sig FootRace {
  runner: seq Person
}
{
  Person in Int.runner
  all p: Person | one p.~runner
}

~runner は、runner の逆写像です。
これで、モデルを出してみます。うまくいったっぽい。


3人が駆けっこして順番を決める、という状況を表すモデルは作れたので、今度は、三人の言うことをそれぞれ述語として書いていきます。
まず一郎の言葉から。一郎は0番じゃない、と。配列のインデックスが0番始まりになってるので、元の問題の一番は0番です。

pred word1() {
  Ichiro.~(FootRace.runner) != 0
}

~(FootRace.runner) は FootRace.runner の逆写像(Person -> Int)です。


このword1を満たすようなモデルを出してみます。とりあえず、一郎が一番にはならないみたい。

同じように、次郎の言うことをword2で、三郎の言うことをword3で。

pred word1() {
  Ichiro.rank != 0
}

pred word2() {
  Jiro.rank = 0
}

pred word3() {
  Saburo.rank = 1
}

rankは、Personを引数に取って、それぞれの順番を返す関数です。さっきの ~(FootRace.runner) を返すだけですが。

fun rank: Person -> Int {
  ~(FootRace.runner)
}


で、3人のうち1人がウソをつく3つの状況を述語として書きます。

pred ichiroIsLiar {
  not word1
  word2
  word3
}

pred jiroIsLiar {
  word1
  not word2
  word3
}

pred saburoIsLiar {
  word1
  word2
  not word3
}

述語 ichiroIsLiar, jiroIsLiar, saburoIsLiarのそれぞれでモデルを探してみると、saburoIsLiarだけがモデルを発見。

見つけたモデル。


ということで、「3人のうち1人が嘘つき」という前提なら、三郎が嘘つきだったと。ぱちぱち。
Alloyで仕様を書くときはこんなノリで進めます*3。ちょっと記法がキモいのが玉に瑕です。


最後に、書いた「仕様」のソースを貼り付けます。
[2011/2/10追記] 全体を書き直しました → こちら

one sig FootRace {
  runner: seq Person
}
{
  Person in Int.runner
  all p: Person | one p.~runner
}

abstract sig Person {}
one sig Ichiro, Jiro, Saburo extends Person {}


pred show() {}

run show

fun rank: Person -> Int {
  ~(FootRace.runner)
}

pred word1() {
  Ichiro.rank != 0
}

pred word2() {
  Jiro.rank = 0
}

pred word3() {
  Saburo.rank = 1
}

pred ichiroIsLiar {
  not word1
  word2
  word3
}

run ichiroIsLiar

pred jiroIsLiar {
  word1
  not word2
  word3
}

run jiroIsLiar

pred saburoIsLiar {
  word1
  word2
  not word3
}

run saburoIsLiar

*1:対象がセオリーだったらSMTソルバじゃないのか、とかいうお話があるかもしれませんが、まぁそれはそれ。

*2:常にtrueと評価されます。

*3:実際は、制約を充足するモデルを見つけるだけじゃなくて、「本当に想定していること以外が起きない」というアサーションを書いて、反例をチェックしたりもします。

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