Alloyでパックマン
Alloyを使ってみた。 数年前に使ったときはなんでこんなの使うのと思っていたけど考えが変わったのだ。
- ちょっとした規模のプログラムを書くには設計が必要だ。
- コードを書く前に、問題の本質的な部分を知っておこう。
- 本質がわかっていれば、 適切な部分にモジュール分割したり、適切なライブラリを選択したり、アルゴリズムを書いたりできるはずだ。
- もちろんお絵描きツールでもいいのだけど、動いたりチェックしたりできれば、設計で得られる知見はより多くなるはず。
- 述語論理で書くけれど、モデルが絵になるのが直感的でよい
- サクサク設計するために Alloy が使えないか ?
Alloyについて
- Alloy は 一階述語論理でモデルを書く。 だから概念は Prolog に近いかもしれない。 いわゆる公理的意味論というやつだ。 が書ける述語はホーン節に限らず自由である。 モデルと制約を自由に書ける。 そのかわり？ モデルのインスタンスの大きさに制限がある。 実装には SAT solver というちょっぱやのソルバが使われている。
- 文法は、関数やデータ構造を書いていく感じなので、手続き型、関数型、果てはオブジェクト指向プログラマ！にも優しい…ように見える。 が、細かい違いがあるので、やっぱり一階述語論理で書いてると思ったほうがいいだろう。
- 公理的意味とはいえ、状態遷移をエンコードしてやることもできる。 そしてそのための便利なライブラリもある。 これをパックマンの例で紹介する。
- 特筆すべき？は、得られるモデルのインスタンスが 様々なやりかたで 視覚化されることだ。 ベタに書くと関係を表す矢印で複雑になりすぎることもあるが、このエントリで示すように、適切な projectionを指定すれば、それなりにすっきりするみたいだ。
- Alloy は SPINのようなモデル検査器とは違い、 ソフトウェアの全状態を網羅的に検査するという思想ではない。
- いわゆる lightweight formal method というやつで、 似たようなコンセプトの VDMやZと違って気軽に使える。
- プログラミング言語の型システムのような、生のコードを保証してくれるたぐいのものではないが、設計が重要であるるようなソフトウェアを書いている人には福音となるかもしれない。
- アジャイル？ 漸進的にモデルを作成して、検査して…というスタイルで設計ができる。 モデル全部ができあがるまで走らない、なんてことはない。
書籍では Software Abstractions : Logic, Language, and Analysis という本が有名だ。 素敵な例がたくさん掲載されている Alloy の教科書だ。 タイトルに惹かれてずいぶん前に買った。ソフトウェアの抽象！ …が放置していた。 一般的すぎるタイトルではある。ちなみに現時点では.comでドルで買うのが安い。
今回は かの有名ゲーム パックマンのモデル を Alloyのサイトからダウンロードして動かしてみた。どうやらコードは短い。
コード
Alloy 4.0 になって関数呼び出しと述語の書き方が変わったらしい。 () を [] に直した。
たったこれだけでパックマンがそれなりに動く。3x3のマス目の上だが、壁とエサもちゃんとある。
module examples/toys/pacman
open util/ordering[State] as ord
abstract sig Position { adjacent : set Position }
one sig p00,p01,p02,
p10,p11,p12,
p20,p21,p22
extends Position {}
fact AdjacentPositions {
adjacent =
p00 -> p01 + p00 -> p10 +
p01 -> p00 + p01 -> p02 + p01 -> p11 +
p02 -> p01 + p02 -> p12 +
p10 -> p00 + p10 -> p11 + p10 -> p20 +
p11 -> p10 + p11 -> p12 + p11 -> p01 + p11 -> p21 +
p12 -> p11 + p12 -> p02 + p12 -> p22 +
p20 -> p10 + p20 -> p21 +
p21 -> p20 + p21 -> p11 + p21 -> p22 +
p22 -> p12 + p22 -> p21
}
abstract sig Status {}
one sig Play, Won, Lost extends Status {}
sig State {
walls : set Position,
food : set Position,
pacman : Position,
blinky : Position,
status : Status
}
fact WallsAreSolid {
all s : State |
s.walls & s.food = none and
not (s.pacman in (s.walls)) and
not (s.blinky in (s.walls))
}
fact GameIsWonWhenAllTheFoodIsGone {
all s : State |
s.status= Won iff s.food = none
}
fact GameIsLostWhenBlinkyGetsPacman {
all s : State |
s.status = Lost iff s.blinky = s.pacman
}
pred FoodSupplyNeverIncreases(s, s' : State)
{
s'.food in s.food
}
pred FoodIsEatenByPacman(s, s': State)
{
s'.food = s.food - s.pacman
}
pred WallsDontMove(s, s' : State)
{
s.walls = s'.walls
}
pred MovementIsOnlyToAdjacentPosition(s, s':State)
{
let p = (s'.pacman), q = (s.pacman) | p->q in adjacent
let p = (s'.blinky), q = (s.blinky) | p->q in adjacent
}
pred MovementIsPossibleOnlyWhilePlaying(s,s':State)
{
s.status != Play implies s = s'
}
fact ValidBehaviour {
all s: State, s': ord/next[s] {
FoodSupplyNeverIncreases[s,s'] and
FoodIsEatenByPacman[s,s'] and
MovementIsOnlyToAdjacentPosition[s,s'] and
WallsDontMove[s,s'] and
MovementIsPossibleOnlyWhilePlaying[s,s']
}
}
pred InitGame(s : State)
{
s.walls = p01 + p11 and
s.food = p00 + p02 + p10 + p12 + p20 +p22 and
s.status = Play
}
fact initialState {
InitGame[ord/first[]]
}
pred GameWon() {
ord/last[].status = Won
}
pred GameLost() {
ord/last[].status = Lost
}
pred GamePlay() {
ord/last[].status = Play
}
//run GamePlay for 1 State
//run GameLost for 2 State
run GameWon for 8 State
実行結果1 パックマン食われた
run GameLost for 2 State
を実行した場合。
めっちゃ複雑なグラフが出るけど、 Stateに Projectionして 最後の状態を見るとこんな風に簡潔になる：
- adjacent は となりあうマス目を表す。
- wall はそのマスがブロックで埋まっていることを示す。
- pacman はそこにパックマンがいることを示す。
- blinky はおばけ。
- food はパックマンのエサ。
うん、パックマンがおばけに食われたときはちゃんと status が 負け(Lost)になっているね。
実行結果2 バグ発見
この単純なモデルでは、次のように パックマンと おばけが「すれちがう」ことができてしまう。
run GameWon for 8 State
を実行すると、途中で
こいつが
こうなる。
これを防ぐための fact を追加するか、もう少し細かいモデル(経路上をドット単位で動けるとか)を考える必要がある。
おぼえたこと
- 型と値の区別が普通のプログラミング言語と異なる。
- 状態遷移っぽいことをするには モジュール util/orderingを使う
- まずは 状態の型を sig State {...} と定義open util/ordering[State] as ord とやる
- 初期状態init・状態遷移next・終状態lastを fact で縛る
所感
わからないこと
- sig における extend と in の違い というか inの使い方
