2012-04-09
■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: あら、学園ものの登場人物が出社するのは制約に反するわね
僕: あ、えっと、そうちょっと保健室に呼ばれていてね。続きは後で！
Permalink | コメント(0) | トラックバック(0) | 08:46 
■Alloyガール2
Alloyガール1の続き。
僕: ただいまー
Alloy: あら、随分長い間保健室にいたのね。何してたの
僕: それはもうJavaScriptとイチャイチャと…って何言わすねん
Alloy: 冗談よ。
僕: …。
JS: ねえねえ、StateManagerが2個ある問題を解決しようよー
僕: そうだったそうだった。
StateManagerは1個である
僕: じゃあそういうわけで、StateManagerは1個だと宣言することにしましょう。
JS: えっと、コンストラクタをプライベートにするんだよね。
僕: いや、それJavaだし。
JS: あれ？objectって宣言するんだっけ？？
僕: それはScalaか？
Alloy: 前回oneだって言ったじゃないの。聞いてなかったの？
JS: oneってどこに書くの？
Alloy: ここよ
one sig StateManager {
state: State
}
sig State {}
run {}
JS: run {}のところに書くんじゃなかったの？
Alloy: そこに書きたいのであればこうね
sig StateManager {
state: State
}
sig State {}
run {
one StateManager
}
JS: どう違うの？
Alloy: 等価だけど何か？
僕: んー、例えばrunを複数個書いた時に、どれを実行するかはメニューから選べるから、オプションの違う探索を使い分けたい時とかにrunの述語の方に書くといいのかな？
JS: うーん、そんなめんどくさいことするかなぁ
僕: うむむ…。
JS: まあいいやー、ようするにrun {}の方に書いてあるのはなんか一時的みたいなー、常に使われるわけじゃないみたいなー、そんな感じね！
僕: うん、まあ、それでいいや。
Stateは0個以上
Alloy: ところでStateManagerとStateの関係が1対1でもいいのかしら
JS: えっ？
Alloy: stateの宣言に何も修飾がついていないから、これはデフォルトで1対1の関係よ
sig StateManager {
state: State
}
JS: それは困るなー。
Alloy: 0個以上ならset、1個以上ならsome、0または1個ならloneね。
JS: どこに書くの？
Alloy: こう
sig StateManager {
state: set State
}
JS: 実行してみよう！エイッ☆
JS: わー、それっぽいものができたよー
僕: ちなみにShow Metamodelすると
JS: メタモデルがShowするんだね！
僕: 何の説明にもなってないぞそれ…
次回予告
僕: 次は何をしようか
JS: えっとねー、各Stateが引数のないメンバ関数enterとexitを持っていて、あとオブジェクトの型とイベントの型から適切なイベントハンドラを探してディスパッチするtriggerって関数がある！あ、あとStateManagerはcurrent_stateを持ってる！
僕: なんかとてもAlloy的じゃないことを言ってる気がするけど…まあいいか。じゃあ次回はそれをAlloyで表現して見ることにしよう。
Permalink | コメント(0) | トラックバック(0) | 22:48
