首先进路解锁模块收到HoldEnd命令，然后将变量SectionN设为1，表示检查起始区段，并将变量Train置1，表示有列车。来到FirstUnlock位置，然后发出RouteFreeApp！命令，要求ZC模块告诉是否该区段有车占用。这里我们模拟出的是第一次讯问时给出Occupied=1，并发送ZC_RouteOcc命令，然后由于有车占用，回到mid6位置，然后再次讯问，ZC模块告诉Occupied=0，并发送ZC_RouteOcc命令，来到FreeCheck位置，这时将Unlock_T置0，开始计时，通过check3section（）函数来判定三点检查是否满足，还要判定Occupied是否等于0，这里我们模拟的首先三点检查下来条件不满足，于是再次发送RouteFreeApp！命令，要求ZC模块告诉现在是否该区段有车占用，并回到mid6位置，ZC模块告诉Occupied=0，并发送ZC_RouteOcc命令，然后又进行三点检查，此时检查出条件满足unlockfill=1，来到TS_check位置，这时判定unlockfill是否为1，还有区段号，这里区段号当前为1，将Unlock_T重置，来到UnlockSucc1位置，表示第一区段解锁成功，然后判定是否到3秒，将FS_Lock置0，Unlock_T计时器清零，将进路状态设置为5，来到MidUnlock位置，继续发送RouteFreeApp！命令，要求ZC模块告诉现在是否该区段有车占用，并将区段号设置为2，表示第1区段已经解锁，现在要解锁第2区段，ZC模块告诉Occupied=0，并发送ZC_RouteOcc命令，来到FreeCheck位置，然后通过三点检查，判定unlockfill是否为1，还有区段号，这里区段号当前为2，将Unlock_T重置，来到UnlockSucc2位置，表示第二区段解锁成功，然后判定是否到3秒，将FS_Lock置0，Unlock_T计时器清零，将进路状态设置为5，来到EndUnlock位置，继续发送RouteFreeApp！命令，要求ZC模块告诉现在是否该区段有车占用，并将区段号设置为3，表示第2区段已经解锁，现在要解锁第3区段，ZC模块告诉Occupied=0，并发送ZC_RouteOcc命令，来到FreeCheck位置，然后通过三点检查，判定unlockfill是否为1，这里区段号当前为3，将Unlock_T重置，来到UnlockSucc3位置，表示第三区段解锁成功，然后判定是否到3秒，将FS_Lock置0，Unlock_T计时器清零，然后来到AllUnlock位置，表示所有区段都已出清，则判定进入状态routestatus是否为5，是的话将进路状态routestatus、Swit_Lock、Train都清零，正常解锁完成。
 
图4.29  区段故障解锁的消息序列
图4.29为区段故障时所采取故障解锁的消息序列。首先进路解锁模块收到HoldEnd命令，然后将变量SectionN设为1，表示检查起始区段，并将变量Train置1，表示有列车。做完以上几步来到FirstUnlock位置，然后发出RouteFreeApp！命令，要求ZC模块告诉现在是否该区段有车占用，ZC模块告诉Occupied=0，并发送ZC_RouteOcc命令，然后又进行三点检查，此时检查出条件满足unlockfill=1，这时由于发生故障fail=1，因此经过判定来到Fail位置，然后到达FailUnlock位置进行故障解锁，解锁完后判定区段号是否为1，将Unlock_T清零，fail设置为0，进路状态routestatus设为5，FS_Lock清零，然后来到MidUnlock位置，继续发送RouteFreeApp！命令，要求ZC模块告诉现在是否该区段有车占用，并将区段号设置为2，表示第1区段已经解锁，现在要解锁第2区段，回到mid6位置。
4.5    延时解锁
4.5.1    延时解锁流程分析
信号开放后车已经接近，此时进路处于接近锁闭状态时，如果要想改变进路，必须先使进路解锁，这时就会采用延时解锁。当收到进路延时解锁命令，首先关闭信号机，从信号关闭起开始计时，过了30秒之后自动解除锁闭。延时的目的是当司机看到禁止信号后刹车可能无法及时将车子刹下来，这时就先将信号机关闭，但不解锁，30秒后保证车子已经停下来了，再解锁，停车后再使进路解锁才是安全的。延时解锁流程如图4.30所示。 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(18):http://www.751com.cn/shuxue/lunwen_767.html