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 は以下のようになる.