2011-08-01から1ヶ月間の記事一覧

[形式手法][モデル検証] AlloyでDining Philosophors 日本語版

FormalMethod勉強会をやられていて、最近は僕も圏論勉強会でご一緒させていただいている id:kencoba さんが前から提案されていた Unicode identifier in Alloy Analyzer http://alloy.mit.edu/community/node/1039 がめでたく本家のAlloy Analyzerに取り込ま…

AlloyでDining Philosophers 〜その２: デッドロックを検出しよう〜

形式手法 モデル検証

さて、この前の日記で、哲学者たちとフォークを一つのテーブルに着かせる事ができました。 では、今度はナイーブなアルゴリズムでデッドロックが起きる事を検証してみましょう。 今回のアルゴリズム 哲学者は同時に１本のフォークをとる。 ２本獲得して満足…