这里在SwitchControl模型中，我一开始没有在SwitchChange位置到SwitchFail位置设置FailRelease==0这个判断，当道岔转换超时后，回到初始状态，并且将FailRelease赋值为1，然后重新办理进路后道岔转换到规定位置后，在SwitchChange位置就会有一个问题，往ChangeOver方向的判定是FailRelease==1是满足的，而对于往SwitchFail位置的判定SwitchPos==0由于刚到位置，还没有将其表示成1，所以也满足的，他就会有两种选择，两边都可以，很有可能道岔到了规定位置还是往SwitchFail位置。所以这里添加了一个FailRelease==0，这样就保证了不会出现两种可能，只要道岔到了规定位置，就一定会往ChangeOver位置走。时钟Timer_Swic的时间自动机模型如图4.6。
 
图4.6  道岔控制时钟的模型
4.1.3    进路选排模拟仿真
 
图4.7  进路选排的消息序列
如图4.7的消息序列所示，首先在进路状态routestatus=0时，ATS会发送一个Route_App！的命令，选排模型收到了这个命令以后会回复一个App_Reply！命令，然后通过函数RouteTable（RouteID）来判断要办进路的合法性，判断完毕后来到StatusCheck状态检查，查看进路状态是如何，这里routestatus=0，因此进入条件检查，如果routestatus=1则要进入监控轨检查。这里还有个函数conditioncheck（），它是照查条件的检查，变量ConditionFill来决定照查条件是否满足，当ConditionFill=1时为满足照查条件，为0则为不满足照查条件。这里为1，满足，然后来到RS_search，对道岔位置进行检查，通过变量SwitchPos，这里刚开始SwitchPos=0，表示道岔并没有在规定的位置，这时会发送SwitchCommd命令，来启动道岔转换模块。道岔转换模块接收到这个命令后发送SetTimer_S！命令，来启动定时器，看道岔是否在规定的时间内到达规定的位置，转换成功后，此时状态为ChangeOver，道岔转换成功后发送reset_S！命令，来重置计时器，表示没有超时，道岔模块动作完毕后会发送Accord！命令，回到选排，选排前面在WaitSwitch状态，在等待道岔扳到规定位置，等到了之后收到Accord？命令则回到JudgeSwitch状态，此时再次判断SwitchPos为1还是为0，此时由于已经完成道岔转换，SwitchPos=1，发送SearchSucc！命令，选排到这结束，进入下一阶段进路锁闭。
 
图4.8  道岔故障处理消息序列
图4.8为道岔发生故障或者超时时的序列图，当道岔控制模块收到SwitchCommd命令后，发送SetTimer_S命令启动计时器，然后等待道岔扳到规定位置，但是由于可能当中有大石头挡住无法到达规定位置，或者由于地面摩擦力太大道岔没有在规定的时间内扳到规定的位置，这个时候我们就认为故障了，模型中设置了超时时间为13秒，所以，超过13秒没有扳到规定位置SwitchPos=0，则来到SwitchFail转换失败状态，将FailRelease置1，表示没有成功转换道岔，然后因为超过13秒，计时器已经发送了timeout1命令，收到后来到error这个位置，然后将switch_clock清零，并发送Disaccord表示不一致，进路选排收到这个命令后就回到了初始状态，等待重新办理进路选排，道岔控制模块也回到了初始状态。
 
图4.9  照查条件不满足时处理消息序列
图4.9为照查条件不满足时的处理消息序列，办理进路选排收到Route_App命令，回复了App_Reply命令，然后照查条件检查，检查后不满足，则回到初始状态，并且将routestatus置0，重新办理进路选排。
 
图4.10  进路状态不为0时监控轨状态不满足时消息序列
 
图4.11  进路状态不为0时监控轨状态满足时消息序列
图4.10与图4.11分别为进路状态不为0时，监控轨状态满足时的处理和不满足时的处理，首先进路选排后到statuscheck位置，然后判断routestatus的状态，当他不为0时，则要发送监控轨检查申请FirstFree_App，然后他会回复过来一个ZCInfor，ZC给监控轨状态信息，如果状态不满足则如图4.10，将会回到初始位置，重新进路选排。而监控轨状态信息满足时则会进入ConditionCheck状态，并进行照查条件检查，如果满足再接下去查看道岔位置。 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(13):http://www.751com.cn/shuxue/lunwen_767.html