添え字付きの Process と Action

by takeuchi — last modified 2012-06-12 12:41

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 はすべて以下のようになる．

buff

Process Prarameter

初期値の設定が可能．

上の LTS を初期値付きの FSP で表すと以下のようになる．

BUFF(N = 3) = (in[i:0..N]-> out[i]-> BUFF).