图4.1  进路选排模块流程图
检查进路的监控区段是对于多列车进路选排的一个重要条件，如果此时进路内有车，进路正处於解锁状态，只要监控区段空闲且未锁闭，那么就可以为下一辆列车排出进路。
4.1.2    进路选排模型
 
图4.2  进路选排的时间自动机模型
进路选排是建立进路时的第一步。当列车到达接近区段后，ATS会向联锁发送进路办理的申请，联锁收到ATS发过来的申请以后，会给ATS发送一个应答，然后根据进路号和联锁表对进路进行选排处理。这个时候联锁就会检查进路的监控轨道是否空闲、是否处于未锁闭的状态，还要检查照查条件是否满足，同时还要检查道岔位置是否在所需要的位置，如果道岔位置不在所需位置时则发出命令道岔动作的指令，直到一致性检查通过才能进入下一个阶段。进路选排的时间自动机模型RouteSearch如图4.2。
从表4.1可以看到模型的主要位置和通道，在进路选排时，还要对进路的一些条件进行检查，看看这些条件是否符合，符合了才可以办理进路等等，比如说这里我们用函数RouteTable（RouteID）来判断进路的合法性，所办理的进路需要形成一个进路表，RouteID是需要办理的进路ID，通过这个函数来看办理进路的ID是否是正确的ID。这里我们设置的ID为固定的，也就是说是针对一条进路的联锁关系。
表4.1  进路选排模型主要位置、通道说明表
位置集合    通道集合
主要位置    说明    通道    说明
Idle    初始位置    Route_App    办理进路命令
Commandproc    办理进路命令处理    App_Reply    办理进路命令应答
StatusCheck    检查进路当前状态    FirstFree_App    监控轨检查申请
FirstSecCheck    监控轨空闲检测    ZCInfor    ZC给监控轨状态信息
ConditionCheck    各种照查条件检查    SearchSucc    进路选排成功
RS_search    进路选排    SwitchCommd    道岔动作命令
JudgeSwitch    道岔位置检查    Accord    道岔在期望位置
WaitSwitch    等待道岔动作完毕    Disaccord    道岔不在期望位置
Route_App？为办理进路的命令，收到这个命令后选排模型会发送一个App_reply！命令，来表示我已经收到了请求。routestatus表示进路状态，只有当routestatus=0时才能办理进路，1-5分别表示进路控制的五个阶段。FirstSecStatus表示监控轨是否空闲，FirstSecStatus=1表示有占用，为0则为空闲。函数conditioncheck（）是照查条件的检查，变量ConditionFill来决定照查条件是否满足，当ConditionFill=1时为满足照查条件，为0则为不满足照查条件。而函数AccordCheck（）则是对进路的道岔进行检查，变量SwitchPos表示道岔是否在规定的位置，SwitchPos置1为道岔已经在规定位置，如果为0，则要发送Switchcommd命令，让道岔转动到规定的位置。变量Swit_Lock用来表示道岔是否锁闭，Switch_lock=1时道岔锁闭，不能进行任何动作。变量FS_Lock表示监控区段锁闭，只有监控区段空闲并且没有锁闭的时候才可以再次办理进路。时钟变量clock_Sear对一些状态做了时钟约束，只有当时间条件符合才能转移到下一个状态。Disaccord与Accord是道岔动作以后用来表示其位置是否与规定位置一致，如果一致则发送SearchSucc！，进入下一步锁闭阶段。如果不一致则发送Disaccord，回到初始位置，重新办理进路。 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(11):http://www.751com.cn/shuxue/lunwen_767.html