「形式手法入門」P157 「6.2.5 イベント駆動スタイル」

割と分かり易い。
ただ、「どういう操作をすると目的の値が出るのか」
を検査するのにこの方法は使えない、よね。

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