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

陆芝浩 等:Ptolemy 离散事件模型形式化验证方法 1841

Fig.6 Ptolemy DE model of traffic environment
图 6 交通灯 Ptolemy DE 模型

如图 7,TrafficLight normal 是 TrafficLight 中 normal 状态的一个细化模型,表示系统在正常情况下,交通灯
控制器的详细模型 , 包含两个控制器 : 车辆交通灯控制器 CarLightNormal 和行人交通灯控制 器
PedestrianLightNormal.当 CarLightNormal 的输出接口 Pgo 和 Pstop 产生输出信号时,PedestrianLightNormal 会
立即作出相应,确保车辆的行为发生改变时,行人的行为也立即发生改变.

Fig.7 Refinement of the normal mode in TrafficLight
图 7 TrafficLight normal 细化模型
如图 8,CarLightNormal 是一个有限状态机,是车辆交通灯的控制器.控制器首先让输出接口 Cred 输出 1,
Cyel,Cgrn 输出 0,是为了初始化车辆交通灯只有红灯亮.CarLightNormal 在 Cred 状态停留 3 个时间单元,使得红
灯持续亮了 3 个时间单元,之后输出接口 Cyel 产生输出,修改参数 Cyel 的值为 1,使得黄灯亮;输出接口 Pstop 产
生输出,使得行人交通灯控制器处于 Pred 状态;CarLightNormal 更新到 Credyel 状态.紧接着,下一个时刻,
CarLightNormal 从 Credyel 状态更新到 Cgrn 状态,并让输出接口 Cred,Cyel,Cgrn 产生 0,0,1 的输出,使得车辆交
通灯只有绿灯亮.CarLightNormal 在 Cgrn 状态停留两个时刻,更新到 Cyel 状态,使得黄灯亮、绿灯灭.下一时刻,
CarLightNormal 由 Cyel 状态更新到 Cred 状态,并使得车辆交通灯只有红灯亮了,同时输出接口 Pgo 产生输出,
通知行人交通灯控制器要更新到 Pgrn 状态,表示行人可以行动了.如此重复这个过程,使得车辆交通灯在红、
黄、绿、黄间不断变化.
如图 9,PedestrianLightNormal 是一个有限状态机,是行人交通灯的控制器.控制器首先让输出接口 Pred 输
出 1,Pgrn 输出 0,是为了初始化行人交通灯只有红灯亮.当 PedestrianLightNorma 的输入接口 Pgo 接收到信号时,
表示行人可以行动了,因此控制器跳转到 Pgrn 状态,并且输出接口 Pred,Pgrn 分别输出 0,1,使得信号灯变为绿灯
亮、红灯灭;当输入接口 Pstop 接收到信号时,表示行人不可以行动了,因此控制器跳转到 Pred 状态,并且输出接
口 Pred,Pgrn 分别输出 1,0,使得信号灯变为红灯亮、绿灯灭.