KAOS (108) イベントベースの仕様 (4.4.4-2)

SCRは表を中心的な表現手段として用いる．以下の表を用いる．

括弧内は，観測変数／制御変数のうち，どちらに対するものかを示している．観測変数は，環境中で関心のある情報であり，環境から機械（システム）に伝わる．制御変数は，システムが環境に働きかけるときの情報である．

最初のモード遷移表について見てみる．以下が，境界書で用いている列車の例である．

モード遷移表（MovementState モードクラス）

モード遷移は状態遷移と考えることができる．モードが状態に相当する．表題にあるモードクラスとは，観測変数に関する状態遷移を示している．ここでの観測変数とは，列車の速度であり，上記で measuredSpeedとして示される．

一行目を見てみる．自車速度がゼロであれば，車両は停止状態となる（新しいモードStopped）．この表で違和感を感じるかもしれない．制御変数ではなく，観測変数に対する遷移表であることを思い起こす必要がある．

@Tの定義を見てみる．

@T(P₁) WHEN P₂

この意味は，「P₂が真であるとき，P₁はあるタイミングで，偽から真に変わる」である．即ち，P₂ ∧ ¬P₁∧P₁’　である（ここでプライムは，Z言語で見たように，イベント受信後を指す）．

@T(measuredSpeed = 0)　イベントの場合だと，観測変数である列車速度について，次の説明となる．括弧内の否定（列車の速度が0ではない）ときは，MovingOKという古いモードである．括弧内が成立したとき（0になった瞬間），Stoppedにモードが変化する．

(nil)

risk = nil;