Page 210 - 《软件学报》2021年第6期

1784 Journal of Software 软件学报 Vol.32, No.6, June 2021

2 混成位置-时间通信顺序进程 HP-TCSP

2.1 混成位置-时间通信顺序进程语法
定义 4. 对于一个系统 S,进程变量集合 PV:={X,Y,P,Q,...}表示 HP-TCSP 中的进程,离散变量集合 DV:={d,t,
m,n,x,y,z,...}包括系统变量、时间变量以及位置中的坐标变量(默认 x,y,z 这 3 个符号代表三维坐标变量,其他变
量中不使用该符号).
混成位置-时间通信顺序进程 HP-TCSP 可以定义为:
d
| Δ
⋅
| ; | ,
| → STOPSKIP
| Q
( ) |
|| Q P Q
| ( ) | P A P
P ::= | |WAIT t a Q P Q P | P Š Q P Q PQ f P \ | AB | ||| | μX f X
ϕ

z
ϕ y
Con >> ( P Con := Pf & &Place [ ( ) ( ),ϕ x , ( )] & Pcon | true) | P Fin Con (Fin _Con := Fcon | tr )eu A Q
_
其中,
• STOP:停止,表示一个进程的中断,该进程不与外部发生通信,可表示死锁或进程不收敛;
• SKIP:跳过,表示一个进程除终止外不做任何事情;
• WAIT t:等待,表示进程在 t 时间后终止,其间不做任何事情;
• a→Q:前缀操作,表示事件 a 执行完后执行进程 Q;
• P;Q:顺序复合,表示进程 P 执行完后执行进程 Q;
• P,Q:外部选择,表示执行进程 P 或 Q 依赖于进程执行的第 1 个事件;
• PŠQ:内部选择,表示执行进程 P 或 Q 由进程内部决定;
d
• PQ :超时,如果 d 时间内两个进程未发生通信则认为超时,控制权由 P 交给 Q;
• PΔQ:中断,Q 的任何事件执行都能导致 P 的中断;
• f(P):换标,f(P)和进程 P 有着同样的结构,只是 P 中的事件经过函数 f 映射为另一个名字;
• P\A:集合隐藏,表示不显示进程 P 中任何属于 A 的事件;
• P A || B Q:同步并发,P 和 Q 在集合 A∩B 的事件并发,在其他集合的事件交叉进行;
• P|||Q:异步并发,进程所执行的每个事件为进程 P 或 Q 中的一个事件;
• μX⋅f(X):f(X)是包含进程变量 X 的一个前缀表达式;
• Con>>P(Con:=Pf&&Place[ϕ(x),ϕ(y),ϕ(z)]&Pcon|true)称为条件执行算子,在 Con 条件成立时,继续执行
进程 P.Con 条件变量按照微分方程 Pf 连续变化,位置变量的三维坐标分别按照微分方程ϕ(x),ϕ(y), ϕ(z)
的微分方程变化,并且微分方程 Pf,ϕ(x),ϕ(y),ϕ(z)中的变量满足谓词公式 Pcon,即 Pcon:=x~c|y~c|
z~c|Pcon 1 ∧Pcon 2 |true,其中,c 是一个实数,~∈{>,≥,<,≤,=}.当条件中无需有位置约束时,则该条件默认
为 true,始终成立.例如(m=2n+1&&Place[x=x+1]&n>1∧x>2)>>P,即:当前 m 变量满足微分方程 2n+1,位
置的 x 坐标按照 x+1 变化.其中,变量 n>1,位置坐标 x>2 时执行进程 P,否则不执行 P.以下 Place
[ϕ(x),ϕ(y),ϕ(z)]也可简写为 Place(x,y,z);
• P Fin_Con(Fin_Con:=Fcon|true)AQ 称为条件中断算子,Fcon 为谓词公式,是进程 P 终止执行时所涉
及的变量的条件,默认为 false,可省略.如果条件 Fin_Con 满足,则中断正在执行的进程 P 进而执行进程
Q.如:P (x<2)AQ 表示当进程 P 执行时,x 坐标小于 2 时,终止 P 进程,执行 Q 进程,且在条件同时满足用
“∧”,条件至少一个满足用“∨”.
TCSP 的基本操作 a?x 表示进程通过通道 channel a 接收 x 的输入,TCSP 中提供通道表示一类事件的集合,
例如:channel a:Int,表示通道 a 能够与任何带有整型数据的事件通信,事件 a.2 是通道 a 声明的一个元素.a!x 表
示向通道 a 中输出消息 x.
2.2 HP-TCSP的混成位置-时间迁移系统

下面讨论 HP-TCSP 的混成位置-时间迁移系统 HP-TCSP 的语义.文献[13]将 TCSP 的语义定义为时间迁移
系统,进程中一个事件的执行在时间迁移系统里可以看作为一个迁移,我们在研究 HP-TCSP 时引入混成位置-