• 先挖个坑，改天再填

FSP 的优势好处

FSP 的使用场景

FSP 的语法规则

递归语句和分句

TRAFFIC_LIGHT = (green ->yellow ->red->TRAFFIC_LIGHT).

• 等价于：

TRAFFIC_LIGHT = GREEN ,
GREEN = (green -> YELLOW),
YELLOW = (yellow -> RED),
RED = (red -> GREEN).

• 注意：
  • 每个分句后面要逗号分隔
  • 整个句子结束要使用句号结束

选择分支语句

(x -> P | y -> Q) 

• 代表通过 $x$ 出发状态 $P$，通过 $y$ 触发状态 $Q$

TRAFFIC_LIGHT = (button -> YELLOW | none -> GREEN),
GREEN = (green -> TRAFFIC_LIGHT),
YELLOW = (yellow -> RED),
RED = (red -> TRAFFIC_LIGHT).

不定状态选择

(x -> P | x -> Q)

• 同一个 $x$ 可能触发 $P$ 也可能触发 $Q$，这是有进程决定的

TRAFFIC_LIGHT = ( button -> YELLOW
| button -> green -> YELLOW
| none -> GREEN
),
GREEN = (green -> TRAFFIC_LIGHT),
YELLOW = (yellow -> RED),
RED = (red -> TRAFFIC_LIGHT).

索引进程

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

• 等价于：

BUFF = (in[0] -> out[0] -> BUFF
|in[1] -> out[1] -> BUFF
|in[2] -> out[2] -> BUFF
|in[3] -> out[3] -> BUFF
).

const 和 range 定义常量

const N = 3
range T = 0..N
BUFF = (in[i:T] -> STORE[i]),
STORE[i:T] = (out[i] -> BUFF).

guarded action

(when B x -> P | y -> Q)

• 当 $B$ 条件（guard）被满足， $x$ 和 $y$ 行为都可能被选择进入，但如果 $B$ 不满足，那么 $x$ 操作就没有进入的可能

COUNT (N=3) = COUNT[0],
COUNT[i:0..N] = (when(i<N) inc ->COUNT[i+1]
|when(i>0) dec ->COUNT[i-1]
).

结束进程

ONESHOT = (once -> STOP).

• 不存在循环重复执行的情况，STOP 单独是一种状态
  
• 结束态 STOP 的定义：

const False = 0
P = (when (False) doanything -> P).