find unreachable state

StateTransitionCheck.als

/*

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 {}