Alloyガール完結編

JS: 最近難しい話ばっかり…
僕: ごめんごめん、なんだっけ。
Alloy: JSちゃんが作った「状態遷移するイベントディスパッチャ」の設計をAlloyでモデリングして、何か有益な知見が得られるか試したい、という話ね
僕: そうだっけ…
JS: もう2週間も前の話だよ。Alloyガール4

前回の設計を思い出す

僕: えーと、StateManagerがシングルトン(one sig)で、0個以上のStateインスタンスを持っている。前回は「Stateインスタンスは全部StateManagerに属していて、とりあえずStateはちょうど3個ということにしてある」ってやったけど、話を簡潔にするために今回は割愛しよう。

one sig StateManager {
	state: set State
}

sig State {}

run {}

JS: うん、それでStateManagerはcurrent_stateを持ってるの。
僕: 1個だけ持ってるんだよね

one sig StateManager {
	state: set State,
	current_state: one State
}

Alloy: one Stateって書かなくてもデフォルトでoneよ。
僕: あ、そうか。でもまあ明示してもいいでしょ。
JS: それでね、StateManagerを作成して1個ずつStateを追加していくの。
僕: 「追加する」ってことは時間によって変化するんだよね
JS: うん
僕: じゃあ時間を導入しよう。

時間の導入

open util/ordering[Time]
sig Time{}

僕: Timeを導入して、それに順序が入っていることをutil/orderingライブラリを使って表現したんだよ。
JS: これでもう時間によって変化するようになったの？
僕: いや、まだ「順序関係のあるTimeって名前のアトムの集合がある」って宣言しただけなので。
JS: ？？
僕: 「current_stateが時間によって変化する」なら「current_stateはある時刻ではなになに、別の時刻ではなになに」ってなるわけだよね？
JS: うん
僕: ということはcurrent_stateは時刻と状態の対の集合なわけだ
JS: 対の集合？
僕: JavaScript的に言えばArrayのArrayって言えばいいかなぁ。時刻1には状態2で、時刻2に状態1に変わった、というのは[[Time1, State2], [Time2, State1]]で表現できるよね、という話。
JS: なるほど！
僕: というわけでこうなりました

one sig StateManager {
	state: State -> Time,
	current_state: State -> Time
}

JS: あれ？ Time -> State じゃなくていいの？
僕: どちらでもいいよ。それは[[Time1, State2], [Time2, State1]]って書くか[[State2, Time1], [State1, Time2]]って書くかの違い。
JS: 順番が違うだけかー。でも Time -> State のほうが自然じゃない？
僕: 僕もそう思うけど、教科書では * -> Time の形で書かれてて、時刻tのfooはfoo.tになってた。Time -> * の形にする場合はfoo[t]って書くことになるだろうね。
JS: やっぱりfoo[t]の方が自然な気がするなぁ。

各時刻に1個という制約

JS: あと、さっきはstateがset(0個以上)でcurrent_stateがone(1個)って書いてたのになくなったよ？
僕: そうだねぇ。oneとかは実はunary setにしか使えないんだ。
JS: unary？
僕: まあ、対が入ってない普通の集合だと思ったらいいよ。
Alloy: State -> Time は長さが2であるタプルの集合で、これを「アリティが2」って表現するの。Stateはアリティが1だからone StateとかできたけどState -> Timeではできないわ。
JS: そうなの？じゃあどうするの？
僕: 「各時刻tについてcurrent_stateが1個だ」って宣言しようか。

one sig StateManager {
	state: State -> Time,
	current_state: State -> Time
}{
	// すべての時刻でcurrent_stateは1個
	all t: Time {
		one current_state.t
	}
}

僕: stateは？
JS: 特に制約はないよ？
僕: じゃあ、質問を変えよう。「特定の時刻ではこうである」ってのはない？
JS: ああー、じゃあStateManagerを作った直後にstateは空っぽで、最終的にはすべてのStateはstateの中に入っている。

one sig StateManager {
	state: State -> Time,
	current_state: State -> Time
}{
	// すべての時刻でcurrent_stateは1個
	all t: Time {
		one current_state.t
	}
	// 最初はstateは空っぽ
	no state.first
	// 最終的にすべてのStateがStateManagerに追加される
	all s: State {
		s in state.last
	}
}

僕: こうやって制約を足しながら、セーブをする感覚でrunをして、そこまでに書いた宣言に矛盾がないか確認するんだよ。
JS: いまのところ矛盾はないみたいだね
僕: まあ矛盾はないって言っても「最低1個の制約を満たす解が存在する」ってだけにすぎないから、その解が全く想定外の形だったりする可能性は否定出来ないわけだけど。
JS: たまにShow Latest Instanceしてぎょっとするものができてないか見ればいいのかな。
僕: まあお好みで。このあたりで一度ソースコード全体を載せておこう

open util/ordering[Time]
sig Time{}

one sig StateManager {
	state: State -> Time,
	current_state: State -> Time
}{
	// すべての時刻でcurrent_stateは1個
	all t: Time {
		one current_state.t
	}
	// 最初はstateは空っぽ
	no state.first
	// 最終的にすべてのStateがStateManagerに追加される
	all s: State {
		s in state.last
	}
}

sig State {}

run {}

ダウト！

Alloy: ところで、この制約だとcurrent_stateがstateの中になくてもOKということになるけど、いいの？
JS: あー、それはダメ
僕: じゃあそれも追加しよう

open util/ordering[Time]
sig Time{}

one sig StateManager {
	state: State -> Time,
	current_state: State -> Time
}{
	// すべての時刻でcurrent_stateは1個
	all t: Time {
		one current_state.t
	}
	// StateManagerを作った直後にstateは空っぽ
	no state.first
	// 最終的にすべてのStateがStateManagerに追加される
	all s: State {
		s in state.last
	}
	// すべての時刻でcurrent_stateはstateの中にある
	all t: Time {
		current_state.t in state.t
	}
}

sig State {}

run {}

Alloy: はいダウト！
JS: えっ
僕: えっ
Alloy: この一連の制約を満たす解は存在しません！
僕: あー、なるほど
JS: えー、なになに？
僕: つまり「StateManagerを作った直後にstateの個数は0個」ってのと「current_stateはstateの要素で、かつ常時1個存在する」は両立できないということさ。
JS: あー、なるほどー。じゃあcurrent_stateを「0個または1個」にすればいいのね？
Alloy: それはloneって宣言になるけど、でもそれだけが解決法じゃないわよね。「StateManagerを作った時点でのstateを空集合にしない」って手もあるわよ。
僕: うん、そこは設計判断だね。「current_stateを0個または1個にする」という設計はJavaScriptで言うなら変数に値がちゃんと入っていたりnullやundefinedだったりするってことだよね。

/** @type {State?} */
var current_state = null;

JS: なるほど、じゃあ「StateManagerを作った時点でのstateを空集合にしない」っていうのは初期化の時点で適当なStateを作ってstateに追加するということね。

/** @type {State} */
var current_state = create_new_state();

僕: そういうこと。Null Objectパターンだね。
JS: どちらの方法を使うかは設計判断ってことなのね。えーと今の設計はnullを使う方になってて、状態遷移goの時に前の状態がnullでないかどうかだけ確認しているなぁ

function go(state) {
    if (current_state != null) {
        if (current_state.exit != null) {
            current_state.exit();
        }
    }
    var current_state = state_table[state];
    nhiro.assert(current_state != null);
    if (current_state.enter != null) {
        current_state.enter();
    }
}

僕: ふむふむ。で、現状ではStateManagerを使い始める前にgoで自分で登録した状態へ遷移してから使っているわけか。
JS: そう。それで問題なく動いているよ。
僕: でも問題が起きるパターンをアドホックに潰しただけで、今のコードで問題ないことを可能な全パターンで確認したわけじゃないよね。たとえば遷移しないで使い始めたらどうなるの？
JS: うーん、それは考えてなかったなぁ。
僕: 失敗する方法があればいずれ失敗する*1し、Null Objectパターンにしておいたほうがいいんじゃない？

余談

筆者: ちなみに、この状態遷移ライブラリを使って別のプロトタイプを作った際にgoで状態遷移しておくのをすっかり忘れて、しかもそれを作っている最中にはきちんと状態遷移が起きてから状態のプロパティを読むパスしか試されてなくて、デモの最中に思いつきで操作の順番を変えたらcurrent_stateがnullのままプロパティアクセスして Uncaught TypeError: Cannot read property of null で死ぬというミスを…「失敗する可能性のあるものは最悪の状況で失敗する」ですな。
Alloy: そもそも2週間前にStateManagerを題材に取り上げた時点で「lone current_state と one state.first を比較して今回みたいな話にする」って予定していたくせに、自分の手元のコードは悪い設計のままってのがバカとしか言いようがないわね
筆者: ぐぬぬ…まったくそのとおりで、当時は状態遷移のコードを切り出したばっかりで、まさに「ちょっと汚いけど、問題なく動いているからまあいいや」だったんだよね。まあ2週間前の自分は他人だったというわけだ。
Alloy: で、私が設計を手伝ったほうがいいものができる、ってのは納得してもらえたかな。
僕: うん、まあ僕個人としては十分納得したよ。だけど、現在主流の言語と使う語彙にギャップがありすぎるね。「no X のシチュエーションで実害のないオブジェクトを指すようにして lone X を one X に変える」が要するに「Null Objectパターン」だとか、そういう対応付けのノウハウが溜まってもっとスムーズに翻訳できるようになる必要があるかなぁ。

*1:マーフィーの法則