Document Actions
Guarded Actions
定義
(when B x -> P | y -> Q) は，guard B が true のとき action x も y も選択可能であるが，Bが false ならば action x を選択することはできないことを意味する．
サンプル
COUNT (N=3) = COUNT[0],
COUNT[i:0..N] = (when(i<N) inc->COUNT[i+1]
|when(i>0) dec->COUNT[i-1]
).
1行目は，CONST の初期値は COUNT[0] であることを示す．2行目で inc アクションが起こると COUNT[i+1] になることを示す．3行目も同様． また，FSP は整数表現だけをサポートしており，0は大抵 false を表し，ほかの数字は true を表す．上の FSP の LTS は以下のようになる．
