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: ぜんぜん違う。オブジェクト指向に毒されているわね。