割と分かり易い。
ただ、「どういう操作をすると目的の値が出るのか」
を検査するのにこの方法は使えない、よね。
eventDrivenStyle.als
// 「形式手法入門」P157 「6.2.5 イベント駆動スタイル」
open util/ordering [Time]
open util/natural
sig Time{}
sig State {
a, b, c, n : Natural one -> Time,
d : Natural
}{
add[a.Time, add[b.Time, c.Time]] = n.Time // a + b + c = n
a.Time = Zero or c.Time = Zero // a = 0 or c = 0
gte[d, n.Time] and gt[d, Zero] // (d >= n) and (d > 0)
}
pred MLout[t, t' : Time] {
gt[State.d, add[(State.a).t, (State.b).t]] and (State.c).t = Zero
(State.a).t' = inc[(State.a).t]
(State.b).t' = (State.b).t and (State.c).t' = (State.c).t
}
pred ILin[t,t' : Time] {
gt[(State.a).t, Zero]
(State.a).t' = dec[(State.a).t] and (State.b).t' = inc[(State.b).t]
(State.c).t' = (State.c).t
}
pred ILout[t,t' : Time] {
gt[(State.b).t, Zero] and (State.a).t = Zero
(State.b).t' = dec[(State.b).t] and (State.c).t' = inc[(State.c).t]
(State.a).t' = (State.a).t
}
pred MLin[t, t' : Time] {
gt[(State.c).t, Zero]
(State.c).t' = dec[(State.c).t]
(State.a).t' = (State.a).t and (State.b).t' = (State.b).t
}
pred I [t : Time] {
(State.a).t = Zero and (State.b).t = Zero
and (State.c).t = Zero
}
pred T [t, t' : Time] {
MLin[t,t'] or MLout[t,t'] or ILin[t,t'] or ILout[t,t']
}
pred Path1 {
let t0 = first, t1 = next[t0], t2 = next[t1],
t3 = next[t2], t4 = next[t3], t5 = next[t4] | {
I[t0] and T[t0,t1] and T[t1,t2] and T[t2,t3] and T[t3,t4] and T[t4, t5]
and (State.a).t5 = One
}
}
// 以下のようにEvaluatorに入力すると、時間ごとの変数aの値が分かる
// ~(State.a)
run Path1 for 5 but 8 Time