西尾泰和のはてなダイアリー

■Alloyガール4

Alloyガール1、Alloyガール2、Alloyガール3の続き。

StateManagerにつながってないStateは良いのか悪いのか？

JS: Stateが3つの例だけが出るようになったー

僕: うんうん、よかったね

JS: でもー、さっき全パターン表示した時に気づいたんだけど、StateManagerにつながってないStateがあるよ？

Alloy: 何か問題でも？

JS: えっ？

Alloy: あなたがモデリングしようとしている対象で、StateがStateManagerに属していない状態があるの？ないの？それ次第でしょ？

JS: み？

僕: つまり、実装で表現するなら下のどっちなのか、って話だね

// A:
var state = create_new_state();
state_manager.add("state_name", state)

// B:
state_manager.create_new_state("state_name")

JS: なるほど、Aの実装だとStateManagerに属していないStateがあってもおかしくないのか。

僕: そういうこと。どちらを選ぶか、は設計判断だね。どっちを選ぶのが正しいのかは状況による。

JS: ちょっとどういう実装にしたか見てくるー。あ、Bにしてた！

僕: そうか、じゃあ「すべてのStateはStateManagerに属している」って事実があるわけだね。

JS: うん！

事実の宣言

僕: じゃあ事実を宣言しよう。

one sig StateManager {
	state: set State
}

sig State {}

fact {
	all s: State | s in StateManager.state
}

run {
} for exactly 3 State

JS: factってのが「事実」？

僕: そう。常にtrueになるような式をここに書くんだ。中身の「all s: State | …」は「すべてのState sについて…が成り立つ」って意味だよ。

JS: で、StateManaerのstateの中にsが入っている、って宣言してるのね。

僕: そうそう。これで実行すると「exactly 3 State」ってスコープにしているから、1個のStateManagerと3個のStateがつながったモデルが出てくる。Nextを押すと解がそれ1個だってわかるね。

JS: StateとStateManagerがちぎれてる例が出なくなったね！

次回予告

Alloy: まどろっこしいなぁ。それって「すべてのStateは必ず1つのStateManagerに属している」ってことじゃないの？

one sig StateManager {}

sig State {
	belong: StateManager
}

run {} for exactly 3 State

JS: そうとも言うー？

僕: いや、でもStateManagerからたどりたいじゃない？

Alloy: たどる？何を言っているのかしら。もしかしてStateManager.stateがStateManagerのメンバ変数だとか、State.belongがStateのメンバ変数だとか勘違いしているんじゃない？

僕: えっ、違うの？

Alloy: ぜんぜん違う。オブジェクト指向に毒されているわね。

ツイートする

Permalink | コメント(1) | トラックバック(1) | 11:07