「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