spec.zed のエラー処理の記述に問題がある
act_tsk が真になる状態 = act_tsk サービスコールが正常に実行される状態である．
一番外側の構造をみると， act_tsk == (残り全部) ∨ Context_Error となっているので，Context_Error が発生した時は，(残り全部)はどういう 状態でもよい，という事になる．
それは例えば，Make_Runnable が実行されたり， 起動要求がキューイングされていてもよい，という事になる．
しかし，「act_tsk が(Context)エラーを帰しているのに， 実は中では正常動作している」というのは，仕様記述としてはおかしい． さらに極端な例では，Make_Runnable とキューイングが両方行われても よいことになり，これは明らかに変な動作である．
Context_Error 以外の，内側のエラー記述についても，本質的に同じ構造を 持っているので，同じ問題を抱えているため，エラー時に変更しない状態は 変更しないことを明示的に変更したりするなどの修正が必要．
act_tsk が真になる状態 = act_tsk サービスコールが正常に実行される状態である．
一番外側の構造をみると， act_tsk == (残り全部) ∨ Context_Error となっているので，Context_Error が発生した時は，(残り全部)はどういう 状態でもよい，という事になる．
それは例えば，Make_Runnable が実行されたり， 起動要求がキューイングされていてもよい，という事になる．
しかし，「act_tsk が(Context)エラーを帰しているのに， 実は中では正常動作している」というのは，仕様記述としてはおかしい． さらに極端な例では，Make_Runnable とキューイングが両方行われても よいことになり，これは明らかに変な動作である．
Context_Error 以外の，内側のエラー記述についても，本質的に同じ構造を 持っているので，同じ問題を抱えているため，エラー時に変更しない状態は 変更しないことを明示的に変更したりするなどの修正が必要．