Alloyガール1 - 西尾泰和のはてなダイアリー

僕: 普通にAlloyさんのことを説明してもイマイチ反応がないんだよね
Alloy: 「普通」の定義があいまいね
僕: …で、とりあえず会話形式にしてみたらいいんじゃないかと思ったんだ！
Alloy: 論理が飛躍しすぎね。まったく何を言っているのかわからないわ。
僕: まあ、そこは僕(人間)のフィーリングを信じてよ！
Alloy: …。
僕: で、ミルｋ…じゃなかったAlloyさんと僕だけでは、制約が厳しすぎて解がなくなると思うんだ。で、教えられ役としてJavaScriptちゃんを連れてきたよ
JS: ハーイ、ローラだよー、あ、いけない、間違えちゃった、じゃばすくりっとだよ☆ (声: ローラ)
Alloy: ………(ため息)

状態遷移図をモデリング

僕: まあまあ、とりあえずこの前JavaScriptと実装した状態遷移図のモデリングをやってみようかな。まず状態を管理しているStateManagerがあって、それがStateを持っているの。

sig StateManager {
	state: State
}

sig State {}

JS: 実行してみるよー、エイッ。あれー「There are no commands to execute.」ってエラーが出ちゃった。
僕: 実行するコマンドを書いていないね。Alloyでは実例を探すrunってコマンドと判例を探すcheckってコマンドがあるよ。
JS: なるほどー。実例を探すときには run {} って書くのかー。この{}って何だろー？
Alloy: それは無名の述語よ
JS: (ポカン)
僕: えっと「とにかく探せ」じゃなくて「こういう条件のものを探せ」って指定ができるんだけど、その「こういう条件」のところを述語っていうんだ。つまり真か偽かを返す式のことだよ。
Alloy: 私がそう言ってるってわけじゃなくて、一般的な用法よ。
僕: いや、コンピュータサイエンスの専門用語は一般的とは言えないと思うけど…

実行してみよう

僕: で、run {} では空っぽの述語を指定していて、それは常に真を返すんだ。
JS: なんでもいいや、実行するよ！エイッ☆ うわーまたなんか出た

Executing "Run run$1"
   Solver=minisatprover(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   115 vars. 15 primary vars. 152 clauses. 3ms.
   . found. Predicate is consistent. 1ms.

僕: いや、それは「成功しました」って書いてあるんだよ。実例を探せって命令して、実例が見つかりました、って返事が戻ってきたの。それもおよそ4msでね。
JS: ふーん、なんか面白くない。
僕: いや、そりゃそうだ。ここでGUIメニューのShow Latest Instanceをクリックすると
JS: インスタンスがShowするのね！
僕: いや、インスタンスってカタカナで書くと何かJavaのclassをnewしたら出来るものっぽくない？ここは英語の元の意味で「事例」って訳したほうがいいのでは
JS: なんでもいいっ！えいっ☆

表示

JS: なんか出た！
僕: そうだね「StateManagerがStateを持っている」という条件を満たしているような例が表示されるんだ。
JS: でもStateManagerが2つなんて常識的に考えておかしくない？
Alloy: …あなたそもそもStateManagerがoneだなんてひとことも言ってないじゃない。
僕: まあまあ、そうだね、今回のコードではStateManagerが1個だとは書いてなかった。じゃあそれを追加してもう一度試そう、と言いたいところだが僕は出社の時間だ
Alloy: あら、学園ものの登場人物が出社するのは制約に反するわね
僕: あ、えっと、そうちょっと保健室に呼ばれていてね。続きは後で！