添え字付きの Process と Action
FSP では,添え字付きの process や action を使用することができます.LTS では,添え字はドット表記に直されます.
BUFF = (in[0] -> out[0] -> BUFF
|in[1] -> out[1] -> BUFF
|in[2] -> out[2] -> BUFF
|in[3] -> out[3] -> BUFF
).
上の FSP は下の2つの FSP と同じ LTS を表す."0..3" は,"0,1,2,3"と同義である.
BUFF = (in[i:0..3]-> out[i]-> BUFF).
range は範囲の宣言である.定数の宣言は const.
range T = 0..3
BUFF = (in[i:T] -> STORE[i]),
STORE[i:T] = (out[i] -> BUFF).
LTS はすべて以下のようになる.
Process Prarameter
初期値の設定が可能.
上の LTS を初期値付きの FSP で表すと以下のようになる.
BUFF(N = 3) = (in[i:0..N]-> out[i]-> BUFF).