Alloy日記2: 時系列で変化する状態

「複数の人がいて、時系列で状態が変化しつつインタラクションする」っていうのをやろうと思ったんだけど(具体的には既婚・未婚状態が変わりながら男女が結婚したり離婚したりするってものを作って、最初は制約が足りなくて重婚が起きてしまい、それを修正するってのをやろうと思ったんだけど)状態を扱うとか難しかったので、昨日は挫折したのでした。

今日は散髪待ちの時間と帰りの電車で6章の事例を写経した。なんとなくわかったので実装してみよう。でもまだ複数人出てくると混乱しそうなので人は1人だけ。で、その人が3つの状態を持っている。緑からは緑と黄色に遷移できて、黄色はすぐに赤に遷移して、赤は緑と赤に遷移できる。

open util/ordering[Time]

sig Time {}
one sig Person {
	state: State -> Time
}

enum State {Green, Yellow, Red}

pred step (t, t' : Time, s: State){
	Person.state.t in Green => Person.state.t' in Green + Yellow
	Person.state.t in Yellow => Person.state.t' in Red
	Person.state.t in Red => Person.state.t' in Green + Red
}

fact {
	all t: Time { // 各時点で1つの状態だけ存在する
		one Person.state.t
	}
}

fact Traces {
	all t: Time - last {
		let t' = t.next {
			all s: State {
				step [t, t', s]
			}
		}
	}
}

run {
	all s: State { // すべての状態について、1回は存在する
		some s <: Person.state
	}
} for 5 Time

「すべての状態について、1回は存在する」を付けないと、最初が赤くて、ずっと赤いまま、なんていう楽しくないものがでてしまった。修正すると、黄色→赤→赤→赤→緑、がでた。めでたしめでたし。楽しくなってきたぞ。