图4.23  信号正常开放和保持后无法正常关闭的消息序列
图4.23为信号正常开放并且保持后，无法正常关闭的处理消息序列。前面的模拟仿真与图4.16的模拟仿真都一样，到了OpenCondiCheck位置，判定CanClose是0还是1，这里的模拟中CanClose=0，信号不能正常关闭，于是进入到FailDeal位置，然后将变量SigStatus设置为0，将信号关闭，并发出HoldEnd命令，表示信号保持结束，进入区段解锁模块。
4.4    正常解锁
4.4.1    正常解锁流程分析
这里我们采取分段解锁的方式，进路被分成若干个区段，这里我将其简化成三个区段，即起始区段、中间区段和终止区段。随着列车的前进，当出清一个区段的时候，该区段就自动解锁。进路正常解锁主要采取“三点检查”的方式，即前一区段已解锁，本区段占用且出清，下一区段占用。进路正常解锁的流程如图4.24所示。
 
图4.24  进路正常解锁模块流程图
4.4.2    正常解锁模型
 
图4.25  进路自动解锁的时间自动机模型
当列车进入该进路，信号立即关闭，进路进入自动解锁阶段。此时锁闭的进路分段自动解锁，各轨道区段原则上满足三点检查后，延迟3秒自动解锁。
表4.5  进路解锁模型主要位置说明表
位置集合    通道集合
主要位置    说明    通道    说明
Idle    初始位置    UnlockSucc2    中间区段解锁成功
FirstUnlock    第一区段解锁    EndUnlock    终止区段解锁
FreeCheck    区段空闲检测    UnlockSucc3    终止区段解锁成功
TS_check    三点检查    AllUnlock    所有区段解锁完毕
UnlockSucc1    第一区段解锁成功    Fail    解锁失败
MidUnlock    中间区段解锁    FailUnlock    故障解锁
由于区段太多会使整个模型变的非常复杂，所以这里我将其简化成三个区段，即起始区段、中间区段和终止区段。每个区段按照三点检查的要求逐段解锁，直到所有区段都解锁完毕，进路正常控制流程结束，进路消亡。如图4.25所示。
正常解锁模块收到HoldEnd命令表示信号保持结束，进路进入正常解锁阶段。进路的自动解锁要进行三点检查，函数check3section（）主要用来判断三点检查的条件是否满足，通过变量unlockfill表示解锁条件是否满足。RouteFreeApp命令表示区段空闲检测申请，ZC收到后回复ZC_RouteOcc，通过变量Occupied等于1还是等于0来表示这个区段是否空闲。
局部变量SectionN表示正在解锁的区段是第一区段还是第二区段还是第三区段，当第一个区段解锁成功后变量FS_Lock=0，表示监控区段空闲，进路可以被再次办理。变量fail表示在解锁过程中是否出现了故障状态，当fail=1表示出现了故障，那么此时就要进入故障解锁，解锁以后令fail=0。Unlock_T为计时器，用来进行时间约束。变量Train表示是否有列车，当Train=1时说明有列车，当出清后Train置0。
进路解锁阶段是整个进路控制的最后一个阶段，解锁后表示本次进路办理全部动作结束，等待下一次的进路办理，下一次再通过ATS发出进路办理申请。
4.4.3    正常解锁模拟仿真
 
图4.26  起始区段解锁的消息序列
 
图4.27  中间区段解锁的消息序列
 
图4.28  终止区段解锁的消息序列 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(17):http://www.youerw.com/shuxue/lunwen_767.html