AlloyでDining Philosophers 〜その１: とりあえず全員テーブルに着席させよう〜

形式手法 モデル検証

最近形式手法について勉強したくて、この本を買ってAlloyって言語について勉強してみたので書いてみる。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

抽象によるソフトウェア設計−Alloyではじめる形式手法−

Alloyって？

いわゆる形式手法と呼ばれる「仕様がちゃんとしているチェックしようぜ」って手法の一つである、「軽量形式手法」という手法をサポートするツールです。
仕様をモデル記述言語で書いて、その仕様が「へんてこな事になってないか？」ってのを、状態を網羅的にチェックして検査してくれるというモノです。
で、Alloyってのは

軽量形式手法のツールで、タダで、グラフィカルに例示ができて、言語自体も、論理と集合の言葉と、みんなが大好きSQLが基にしている「関係」がわかってれば、覚える事は「記法」くらい。と、とりあえずモデリングさえできれば、取っ付ける、とっても取っ付きやすい形式手法のツールです。

中身としてはモデルと制約を全部論理式に展開してSATソルバにかけるっていう風にやってるみたいです。
[参考]Alloyの紹介記事：

さて、Dining PhilosophersをAlloyで解いてみよう！

システムの陥ってほしくない状態の代名詞でもあるデッドロック。これを検出させるのを目標にしてAlloyでモデルとアルゴリズムの仕様を記述してみましょう。蛇足ですが、僕が大学でこの概念に出会った時はたしか「死の抱擁」って訳されてた覚えたがありますw

問題の説明は割愛します。定義はwikipedia参照。
wikipedia - 食事する哲学者の問題

さて、小難しい説明は抜きにして書いてみましょう。まずは哲学者とフォークを定義してみましょう。

-- 哲学者
sig Philosopher {
	-- 左と右には異なるフォークが1本ずつある
	disj leftFork, rightFork: one Fork,
	-- 左と右には哲学者が１人ずついる
	left, right: one Philosopher
}
-- フォーク
sig Fork { 
	-- フォークの左と右には異なる哲学者が一人ずついる
	disj left, right: one Philosopher
}

さて、これだとフォークと哲学者の間に何の制約も無いので、leftとかrightってフィールドに何でも代入できちゃいますから、哲学者とフォークが互い違いに並んでいるように制約を書きましょう。制約はfactってキーワードで記述します。

fact{
	-- フォークと哲学者の数は同じ
	#Philosopher = #Fork
	-- すべての哲学者に対して、右(左)の哲学者は、右(左)のフォークの右(左)の哲学者と等しい
	(all p: Philosopher | p.left = p.leftFork.left and p.right = p.rightFork.right )
	-- すべてのフォークに対して、左(右)の哲学者の右(左)のフォークは自分
	(all f: Fork | f = f.left.rightFork and f = f.right.leftFork)
}

これで隣どうしの哲学者の間に共通のフォークが存在している制約がかけました。なんか足りない気もしますが、進みましょう。まずは、この制約の上でどんな例が存在するのかAlloyに探させてみましょう。そうすれば色々わかるはずです。そんな時によく使うイディオムがこれ。

-- 常に真であるという述語
pred show{}
-- showという述語が成立する例を探せ
run show for 4 Philosopher, 4 Fork

run は述語を第１引数にとって、その述語が成立する例を探してくれるコマンドです。for 〜〜で続けると、探索範囲を指定できます。この例だと、フォークも哲学者も最大４個(人)で、っていう指定です。showって述語はいつも真になるような述語を定義しておくことでとりあえず制約を満たすモデルを例示できるというわけ。
Alloy Analyzerでこれを打ち込むと、いろんなパターンが出てきます、サイズ２、３、４でちゃんとテーブルに並んで座ってる図もでてきますが、こんな図も出てきてしまいます。

これだと、一つのテーブルにつけてません。足りなかった制約はこれのようです。そうですね。フォークと哲学者が交互に並んでるというだけでは、テーブルは複数でもOKだということですね。ということで次の制約を付け加えてテーブルを一つにしてみます。

-- テーブルは一つ
fact OneTable{
	-- すべての哲学者に対して、どの哲学者も左、左(右、右)とたどる事で到達できる
	-- left(right)の推移的閉包は哲学者全体を含む
	(all p: Philosopher | Philosopher in p.^right and Philosopher in p.^left)
	-- すべてのフォークに対して、どのフォークも左、左(右、右)とたどる事で到達できる
	-- left.leftFork(right.rightFork)の推移的閉包はフォーク全体を含む
	(all f: Fork | Fork in f.^( left.leftFork ) and Fork in f.^( right.rightFork ))
}

さて、これでどうでしょうか。同じようにrunしてみると、さっき出てきた２テーブルの例は出てこなくなるのがわかると思います。
うん。よしよし。これで、哲学者とフォークを１つのテーブルに並べる事ができました。
次は、単純なアルゴリズムを記述してみて、デッドロックが発生してしまうことを検出してみます。