Alloy Analyzer について軽く文法を調べれたので,試しに動かしてみました.
サンプル
問題
A, B, C, D の 4 人は,総務,外務,財務,防衛の 4 つの大臣に重複なく割り振られる.割り振りに関して,以下の情報が得られた:
- B の担当は外務大臣でも財務大臣でもない;
- 総務大臣の担当は A か D;
- D の担当は財務大臣か防衛大臣.
さて,割り振りはどうなっていたか?
解答
まずは,普通に解いていきます.
3 から,D は総務大臣ではないので,2 より A が総務大臣となります.
あとは外務,財務,防衛の 3 個の候補が残っていますが,1 より B は外務でも財務でもないので,B は防衛と定まります.
再び 3 より,D の候補は財務に絞られるので,D が財務大臣となり,C は残った外務大臣となります.
Alloy で解いてみた
まずは,ホニャララ大臣を定義します:
// 大臣
abstract sig Minister {}
one sig Soumu extends Minister {}
one sig Gaimu extends Minister {}
one sig Zaimu extends Minister {}
one sig Bouei extends Minister {}
次に,人を定義します:
// 人
abstract sig Person {
tantou: one Minister
}
one sig A extends Person {}
one sig B extends Person {}
one sig C extends Person {}
one sig D extends Person {}
条件についてですが,問題文の 3 個の他に,それぞれ異なる大臣になる,という条件もあるので,合わせて記述します.これらは確定事項なので,fact として記述します:
// ファクト
fact fact1 {
B.tantou != Gaimu && B.tantou != Zaimu
}
fact fact2 {
A.tantou = Soumu || D.tantou = Soumu
}
fact fact3 {
D.tantou = Zaimu || D.tantou = Bouei
}
fact distinctTantou {
A.tantou != B.tantou &&
A.tantou != C.tantou &&
A.tantou != D.tantou &&
B.tantou != C.tantou &&
B.tantou != D.tantou &&
C.tantou != D.tantou
}
って,distinctTantou の書き方がダサすぎる(名前もダサいのは置いといて!!!).
以下のように pred を使って書き直します:
fact distinctTantou {
/*
A.tantou != B.tantou &&
A.tantou != C.tantou &&
A.tantou != D.tantou &&
B.tantou != C.tantou &&
B.tantou != D.tantou &&
C.tantou != D.tantou
*/
all a, b: one Person | neq[a, b]
}
pred neq [a, b: one Person] {
a != b implies a.tantou != b.tantou
}
最後に,表示用の pred を記述して run すれば OK.
全体像は以下の通り:
// 大臣
abstract sig Minister {}
one sig Soumu extends Minister {}
one sig Gaimu extends Minister {}
one sig Zaimu extends Minister {}
one sig Bouei extends Minister {}
// 人
abstract sig Person {
tantou: one Minister
}
one sig A extends Person {}
one sig B extends Person {}
one sig C extends Person {}
one sig D extends Person {}
// ファクト
fact fact1 {
B.tantou != Gaimu && B.tantou != Zaimu
}
fact fact2 {
A.tantou = Soumu || D.tantou = Soumu
}
fact fact3 {
D.tantou = Zaimu || D.tantou = Bouei
}
// だっさ!!!!!
fact distinctTantou {
/*
A.tantou != B.tantou &&
A.tantou != C.tantou &&
A.tantou != D.tantou &&
B.tantou != C.tantou &&
B.tantou != D.tantou &&
C.tantou != D.tantou
*/
all a, b: one Person | neq[a, b]
}
pred neq [a, b: one Person] {
a != b implies a.tantou != b.tantou
}
pred show {}
run show
そんで,出てきたのが以下の図:
正しく表示されてるし,Next を押しても他の例が表示されない!やったね!
コメント