不正な状態遷移を見つけるアルゴリズム

a-sanさんの日記より、
http://d.hatena.ne.jp/a-san/20090626/p2

Alloyだとこれだけなのか？

/*

http://d.hatena.ne.jp/a-san/20090626/p2
*/

abstract sig State {
	transient:set State
}
one sig O,A,B,C,D,E,F,G,H,I extends State {}

fact {
	transient =
		O -> A +
		A -> B +
		B -> C +
		C -> B +
		C -> A +
		D -> B +
		D -> H +
		H -> D +
		E -> F +
		F -> G +
		G -> F +
		G -> E +
		I -> I
}

fun reachables [s:State]:set State {
	s.^transient
}

fun unreachables [s:State]:set State {
	State - reachables[s]
}

run {}

Evaluatorで以下の様に関数を実行すれば良い。

unreachables[O$0]

{D$0,E$0,F$0,G$0,H$0,I$0,O$0}