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

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

用一组声明即可,所以只针对输出接口 Pgo,Pstop 和自定义参数 count 产生相应的全局声明.组件中的每条迁移
都至少对应时间自动机中的一条迁移,首先 TrafficLight_normal_down?接收顶层传来的同步,然后 TrafficLight_
Sec_isPresent 判断输入接口信息是否满足,再判断迁移的约束条件是否满足:若满足,则对输出接口进行赋值并
更新参数,为赋值的输出接口产生同步信号,更新到目的状态;若不满足,则返回迁移的源状态.时间自动机中除
初始状态外,每个状态都对应有一条以初始状态为目标状态的迁移 TrafficLight_Normal_init?,用于初始化时间
自动机.

Fig.11 Automaton of CarLightNormal
图 11 CarLightNormal 时间自动机

图 12 是由有限状态机 PedestrianLightNormal 转换而来并进行优化的时间自动机,输出接口 Pred 和 Pgrn
连接的组件与模型的整体逻辑无关,所以不再为其产生同步信号,只为每个输入接口产生 int 和 bool 的全局声
明.每组迁移首先 TrafficLight_normal_down?接收顶层传来的同步,然后判断迁移的约束条件是否满足:若满足,
则对输出接口进行赋值并修改参数,更新到目的状态,同时产生同步信号 TrafficLight_normal_sync!与顶层同步;
若不满足,则返回迁移的源状态,同时产生同步信号 TrafficLight_normal_sync!与顶层同步.时间自动机中除初始
状态外,每个状态也都对应有一条以初始状态为目标状态的迁移 TrafficLight_Normal_init?,用于初始化时间自
动机.