Alloy日記3: 結婚と離婚をモデリング - 西尾泰和のはてなダイアリー

2012-04-07

■Alloy日記3: 結婚と離婚をモデリング

Alloyは「関係」が言語の基本的な構成要素なので、やっぱり身近な関係として「人間関係」を使うとわかりやすいですね。というわけで檜山さんのAlloyで人生モデリングその2：時間軸を設定する - 檜山正幸のキマイラ飼育記の続編を勝手に作ってみました。

orderingの説明については檜山さんのエントリーを参照。時系列で変化する状態をモデルに入れる方法については6.1章を見るか、それを見ながら書いた僕のAlloy日記2: 時系列で変化する状態を参照。

というわけでまずはソース。空行・コメントを除くとたかだか29行ですね。

open util/ordering[Time]

sig Time {}

sig Person {
	state: State -> Time,
}

enum State {Married, NotMarried}

pred init (t: Time) {
  all p: Person | p.state.t = NotMarried
}

pred step (t, t': Time) {
	some disj p1, p2 : Person {
		{
			// marrige
			p1.state.t = NotMarried and p2.state.t = NotMarried
			p1.state.t' = Married and p2.state.t' = Married
		} or {
			// divorce
			p1.state.t = Married and p2.state.t = Married
			p1.state.t' = NotMarried and p2.state.t' = NotMarried
		}
	}
}

fact Traces {
	init[first]
	all t: Time - last {
		step[t, t.next]
	}
}

run {} for exactly 3 Person, 5 Time

fact Tracesの中では「最初の時点で述語initが成立している」「連続する2時刻について述語stepが成立している」の連言。initの中身は「最初は誰も結婚していない」で、stepの中身は「相異なるPerson p1, p2がいて、(両方前の時刻で結婚しておらず次の時刻で結婚している) または (両方前の時刻で結婚していて、次の時刻で結婚していない)」という意味。

実行してみると、3人の人が出てきてくっついたりはなれたりするのが観察できる。あ、もちろんVisualizerの設定でTimeでProjectionする必要がある。こういうVisualizerへの指示をコード中にコメントか何かで埋め込んだりできないのかな？

さて、現状ではまだPerson0とPerson1の結婚とかで面白みが足りないので、先日作ったライブラリを使って人間に名前をつけてみる。そもそも現時点では人間に性別がないしね。

登場人物に名前をつける

 open util/ordering[Time]
+open named_man_ja [Man]
+open named_woman_ja [Woman]
 
 sig Time {}
 
-sig Person {
+abstract sig Person {
 	state: State -> Time,
 }
 
+abstract sig Man, Woman extends Person {}
+
 enum State {Married, NotMarried}

名前がつきました、が、幸子と節子が女同士で結婚してしまった！性別が異なるペアでなければならない、って制約が入ってないな。

性別が異なる

-       some disj p1, p2 : Person {
+       some p1 : Man, p2 : Woman {

よし、男と女で結婚した。だけど、あれれ？進が「未婚とか既婚とか俺には関係ないし」とか言い出してしまった。

これは「結婚や離婚をした人以外は直前の状態から変化しない」って制約が入ってないから。

他の人は状態を変えるな


        some disj p1 : Man, p2 : Woman {
-               {
+               {{
                        // marrige
                        p1.state.t = NotMarried and p2.state.t = NotMarried
                        p1.state.t' = Married and p2.state.t' = Married
 		} or {
                        // divorce
                        p1.state.t = Married and p2.state.t = Married
                        p1.state.t' = NotMarried and p2.state.t' = NotMarried
+               }}
+               // others don't change their state
+               let others = (Person - p1 - p2) {
+                       others.state.t = others.state.t'
                }

うーむ、うまくいくようになりました、って見せいたところだけどスクリーンショットを手作業で5枚取るのがめんどくさいな。連番画像として出力してくれる機能とかないんだろうか。

まず最初はみんな未婚で、次に久美子と進が結婚して、離婚して、隆と結婚しなおして、そしてまた離婚しました、というシナリオが生成されている。めでたしめでたし(ぇ？)

リファクタリング

さあ皆さん大好きなリファクタリングのお時間です。Alloyの長所は探索範囲での網羅的テストが書いてあるようなもんだから安心してリファクタリングできるところですね。

pred change_state (
	p1 : Man, p2 : Woman,
	t, t': Time,
	before, after : State){
		p1.state.t = before
		p2.state.t = before
		p1.state.t' = after
		p2.state.t' = after
		// others don't change their state
		let others = (Person - p1 - p2) {
			others.state.t = others.state.t'
		}	
}

pred step (t, t': Time) {
	some disj p1 : Man, p2 : Woman {
		change_state[p1, p2, t, t', NotMarried, Married]
		or
		change_state[p1, p2, t, t', Married, NotMarried]
	}
}

しかしまあ過信は禁物ね

探索範囲が狭いとバグを発見できない

リファクタリングをしているときに僕の生身の目が上記のコードのバグを見つけました。なんでそれがAlloyで補足されてないか？それは登場人物が3人までの範囲でしか探索してなかったから。まずはそれをAlloy自身に発見してもらいましょう。えーと、登場人物が5人で、時間が4以上の時に発生しうるのか。

run {} for exactly 5 Person, 4 Time

実行してみたら、同じバグが原因で、僕が思いついたのとは違うシナリオで、4人でも発生しうるケースを教えてくれました。なるほど、たしかにそれでも起こる。

何が原因か？

-               let others = (Person - p1 - p2) {
-                       others.state.t = others.state.t'
-               }
+               all other: (Person - p1 - p2) {
+                       other.state.t = other.state.t'
+               }

修正前の書き方では「others全員のstateの集合が変化してない」だったので「AさんがMでBさんもM」って状態から「AさんだけMでBさんはナシ」って状態でも成立してしまうわけだ。これはまあ僕が「各時点で各人が持つ状態はちょうど1つ」っていう当たり前の制約を書き忘れていたことにも原因がある。

僕が思いついた方の失敗例は「各時点で各人が持つ状態はちょうど1つ」を暗黙に仮定していたので、5人以上で発生する「AさんがMでBさんがN」って状態から「AさんがNでBさんはM」っていう「状態の交換」が発生しうるって点だったんだけど、暗黙の仮定が崩れてたのでもっと小さい実例があったわけですね。

修正後の書き方ではallでothersの中の個々人について状態が変わらないことを宣言しています。