システムα

「4日で学ぶモデル検査」より。
愚直にモデリングしてるだけで、これではスイッチがOn,Offされることを
確認できない・・・

open util/ordering[State] as so
/*
4日で学ぶモデル検査
システムα
*/
abstract sig Switch {}
one sig On,Off extends Switch {}
abstract sig Number {}
one sig Zero,One,Two extends Number {}

sig State {
	a: one Number,
	b: one Number,
	s: one Switch
}

pred first[st:State] {
	st.a = Zero and
	st.b = Zero and
	st.s = Off
}

pred trans[st,st':State] {
	st'.a = next_a[st.a,st.b] and
	st'.b = next_b[st.a,st.b] and
	st'.s = next_s[st.a,st.b,st.s]
}

fun next_a[a,b:Number]:Number {
	{ n:Number |
		(b = One)  => n = a   else
		(a = Zero) => n = One else
		(a = One)  => n = Two else
		(a = Two)  => n = Zero
	}
}

fun next_b[a,b:Number]:Number {
	{n:Number |
		(a = b) => n = b else
		(b = Zero) => n = One else
		(b = One)  => n = Two else
		(b = Two)  => n = Zero
	}
}

fun next_s[a,b:Number,ss:Switch]:Switch {
	{ss':Switch |
		(a = b and a = Two) => ss' = On else
		(a = b and a = One) => ss' = Off else
		ss' = ss
	}
}

pred show [] {
	first[so/first] &&
	( all pre: State - so/last | let post = so/next[pre] |
		trans[pre,post]
	)
}

run show for 9