车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(16)
在图4.17信号控制模块我一开始没有设置mid8这样一个中间位置，理论上在信号超时未开放时，会收到一个timeout2命令，然后进入故障修理，根据模拟仿真后发现，这样的话，由于在SetTimer_signal模块中设置了t2的时间超时规定，模拟仿真下来发现这样会在SignalFail位置出现死循环，但是经过试验，发现删掉SetTimer_signal模块中的t2>=15这条判定后死循环就消失了，说明t2>=15这条判定在这里与收到timeout2命令有一定冲突，于是我再SignalFail位置和Repair位置当中设置了一个mid8中间位置，这样当到了SignalFail位置后，有一定的时间来让计时器t2计时，当过了15秒后来到mid8位置，并发送timeout2命令，这样就能顺利接收到命令，消除死循环。
4.3.3 信号开放和保持模拟仿真
图4.19 信号正常开放和保持过程的消息序列
首先信号控制模块收到opensignal命令后，启动计时器open_T，将其置0，然后将进路状态设置为3，到达mid2位置，然后发出SetTimer_Sig命令，启动SetTimer_signal模块，模块收到命令后将t2置0，启动t2计时器。然后来到SignalContr位置。接着判断Canopen是否为1，open_T是否大于3秒，判断符合后将open_T清零，SigStatus置1，表示信号已经开放，到SignalOpen位置，然后发出reset_Sign命令，把SetTimer_signal模块重置，因为在规定时间内已经开放信号。发出命令后来到mid3位置，接着就将进路状态设置为4，并保持信号，到了SignalHold位置。然后发送FirstFree_App命令来查看监控轨状态，通过Mid4位置，这时ZC模块收到这个命令后会发送一个ZCInfor命令，并告诉监控轨状态是1还是0，也就是是有车占用还是空闲，然后到OpenCondiCheck。本次模拟仿真监控轨状态为1，也就是监察到有车占用了，然后判断CanClose是否为1，表示可以关闭，并且人工解锁ManualUnlock为0，都符合后则将SigStatus置0，表示信号关闭，并发送HoldEnd命令，表示信号保持结束，切到进路解锁模块。
图4.20 信号故障处理消息序列
图4.20为信号故障处理时的消息序列，首先收到opensignal的命令，启动计时器open_T，将其置0，然后将进路状态设置为3，到达mid2位置，然后发出SetTimer_Sig命令，启动SetTimer_signal模块，模块收到命令后将t2置0，启动t2计时器，此时t2超过了规定的时间，发出timeout2报警，到了SignalFail信号开放失败的位置，收到timeout2报警后进入Repair修理模式，修理完毕后发出SetTimer_Sig重置SetTimer_signal模块，将Open_T计时器清零，将变量CanOpen置1，回到SignalContr位置。
图4.21 信号保持时收到延时解锁的消息序列
图4.21为在信号保持时，收到延时解锁，则要信号关闭。前面的模拟仿真与图4.16的模拟仿真都一样，只是到了信号保持SignalHold位置，由于这里人工解锁ManualUnlock=1，ATS模块会发送TimeUnlockApp命令来启动延时解锁模块，延时解锁模块根据各种判定后发送关闭信号CloseSignal命令，信号控制模块SignalHold位置收到这个命令后到mid5位置，当信号关闭后会发送CloseOver！命令，发送后到Close位置，最后将变脸SigStatus设置为0，表示信号关闭，回到初始状态。
图4.22 信号保持后进路第一区段空闲检测的消息序列
图4.22为信号开放后检测进路第一区段空闲与否，然后根据进路第一区段的状态来动作，前面的模拟仿真与图4.16的模拟仿真都一样，到了信号保持SignalHold位置，发送FirstFree_App命令，进入mid4位置，ZC模块收到后会告诉FirstSecStatus第一区段的状态，这里首先检测出来为0，表示没有车进入，ZC模块发送ZCInfor命令给信号控制模块，收到ZCInfor命令后进入OpenCondiCheck状态，然后因为FirstSecStatus=0，所以判定后又回到了SignalHold位置，直到检测到FirstSecStatus=1，则OpenCondiCheck位置不会回到SignalHold，而是根据判定，FirstSecStatus是否等于1，是否能关闭，人工解锁是否为0，这里判定都满足，然后将变量SigStatus设置为0，表示信号关闭，发出HoldEnd命令，表示信号保持结束，进入区段解锁模块。
下一篇：投资者情绪与股票收益率的关系研究