车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(14)
4.2 进路锁闭
4.2.1 进路锁闭流程分析
当进路处理模块的发送SearchSucc后，进路锁闭模块收到这个命令后，查看锁闭条件，满足的话进路处理程序转到执行进路锁闭模块。此外，进路锁闭模块应完成：检查道岔位置正确、检查照查条件满足、在条件满足时，实现进路锁闭。将道岔和敌对进路都锁闭，使道岔不能再转动，敌对进路不能建立，准备好要信号开放。如果检查的条件不满足则要回到初始状态，等待重新办理进路。进路锁闭流程图如图4.12。
图4.12 进路锁闭流程图
4.2.2 进路锁闭模型
图4.13 进路锁闭的时间自动机模型
进路选排成功后发送SearchSucc命令后就进入进路锁闭阶段，在这个模块还要检查道岔的位置和照查条件是否满足，如果满足则锁闭进路，若不满足则回到初始状态，重新办理进路。进路锁闭的时间自动机模型如图4.13。
表4.3 进路锁闭模型主要位置、通道说明表
位置集合 通道集合
主要位置 说明 通道 说明
Idle 初始位置 SearchSucc 进路选排成功
LockCheck 锁闭条件检查 opensignal 信号开放命令
LockSetup 锁闭设置
RS_lock 进路锁闭状态
SearchSucc命令是进路锁闭模块启动的一个十分关键的命令，只有收到该消息才能表示进路进入锁闭处理阶段，如果没有这个命令则这个模块将一直处于等待状态。函数lockCheck（）是对进路的一些特定条件进行检查，因为铁路上的信号等于是火车的眼睛，如果信号随便开放了，开放的对，则没有事情，只要有一点点和规定有出入，则很有可能就是车毁人亡，所以这个锁闭模块十分重要，不仅关系到道岔锁闭，还关系到信号是否正确开放。这里我们用变量LockFill判断进路锁闭条件是否满足。这里用时钟变量clock_lock对锁闭设置阶段的一些动作进行时间约束，该过程可能需要在2个时间单位左右内完成。变量Swit_Lock是道岔锁闭的一个标志，如果这个变量置1的话则表示该道岔已经锁闭，如果这个变量置0的话则表示该道岔还没有锁闭。变量FS_Lock是监控区段锁闭的一个标志，置1了则表示当前监控区段处于锁闭状态，不可办理进路，而当变量置0了则表示当前监控区段处于空闲状态，可以办理进路。通道opensignal表示锁闭阶段结束，发送这个命令表示本锁闭模块已结束，并告诉信号控制模块可以开始启动了，这个命令会产生一定的延迟，这里我们估且设定该延迟为1-2个时间单位。
4.2.3 进路锁闭模拟仿真
图4.14 进路锁闭满足锁闭条件的消息序列
图4.14为进路锁闭过程中检查照查和道岔条件后满足的消息序列，当该模块收到SearchSucc命令后，将进路状态设置成routestatus=2，然后通过函数lockCheck（）来检查道岔和照查条件是否满足，检查下来是满足的，然后到LockCheck位置，将时钟clock_lock置0，然后到LockSetup，2秒动作以后将FS_Lock监控轨锁闭和Swit_Lock道岔锁闭置1，表示已经锁闭，无法办理新进路了，到了RS_lock状态，然后将clock_lock清零，并发送opensignal！命令，通知信号开放模块启动，然后回到idle位置。
图4.15 进路锁闭不满足锁闭条件的消息序列
图4.15为进路锁闭过程中检查道岔和照查条件不满足时的消息序列，前面都一样，收到SearchSucc然后检查条件，检查出不满足后，将进路状态routestatus设为0，然后回到初始状态，等待重新办理进路。
下一篇：投资者情绪与股票收益率的关系研究