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

FormalMethod勉強会をやられていて、最近は僕も圏論勉強会でご一緒させていただいている id:kencoba さんが前から提案されていた

Unicode identifier in Alloy Analyzer
http://alloy.mit.edu/community/node/1039

がめでたく本家のAlloy Analyzerに取り込まれることになったそうです☆

モデル検証において、識別子が日本語もOKということはソースもそうだけれど、図示したときの理解しやすさが格段にわかりやすくなる。

ってことでDining Philosophersのalloyのモデルを日本語化してみました。

まずは、デッドロック状態を図示したやつ。

ソースはコチラ。