一般的には、事前条件P、受け取るメッセージ列M、状態遷移（move）m、発行されるメッセージ（イベント）列Nを使って、on P receiving M causes m emits N が仕様記述文てことになります。が、状態遷移は、遷移後の状態が満たす条件＝事後条件を書けば指定できるので、on P receiving M results Q emits N でもいいでしょう。
受信も送信もメッセージとして抽象化してあるので、パイプラインの記述が自然にできます。
spec Counter {
// 安全なとき
on (value() < 100) receiving {inc();}
emits {valueChanged();}
// 限界を超えているとき
on (value() >= 100) receiving {inc();}
emits {overflow();}
}spec Alarm {
on (true) receiving {valueChanged();}
emits {} // 何も起きない
on (true) receiving {overflow();}
emits {warn();}
}
CounterとAlarmを直列結合したものは、次の仕様を満たすことがわかるでしょう。
spec CounterWithAlarm {
// 安全なとき
on (value() < 100) receiving {inc();}
emits {} // 何も起きない
// 限界を超えているとき
on (value() >= 100) receiving {inc();}
emits {warn();}
}
とまー、こういう仕様の計算が自由にできたらいいな、と思っているのです。
（仕様の話、おわり）
