## 5 SMT-Based BMC of \(\mathsf{ELTLKD_{q}}\) Properties
### SMT Encoding of Transition Relation of FTTCS with Two Trains
#### 5.5.2. Global Action Transition Relation  
The global transition relation \(\mathcal{T}_{\Sigma}\) describes how the entire system transitions from one global state \(\overline{\mathbf{w}}=(\overline{\mathbf{w}}_{T_{1}},\overline{\mathbf{w}}_{T_ {2}},C)\) to the next global state \(\overline{\mathbf{w}}^{\prime}=(\overline{\mathbf{w}}^{\prime}_{T_{1}}, \overline{\mathbf{w}}^{\prime}_{T_{2}},C^{\prime})\) under some action \(\overline{a}\). \[\mathcal{T}_{\Sigma}(\overline{\mathbf{w}},\overline{a},\overline{\mathbf{w}}^{ \prime})=\mathcal{T}_{T_{1}}(\overline{\mathbf{w}},\overline{a},\overline{ \mathbf{w}}^{\prime})\vee\mathcal{T}_{T_{2}}(\overline{\mathbf{w}},\overline{ a},\overline{\mathbf{w}}^{\prime})\vee\mathcal{T}_{C}(\overline{\mathbf{w}}, \overline{a},\overline{\mathbf{w}}^{\prime})\]  
The action transitions for train \(T_{1}\) are defined as follows: \(\mathcal{T}_{T_{1}}(\overline{\mathbf{w}},\overline{a},\overline{\mathbf{w}}^ {\prime})=\)  
\[ \begin{split}&\left(s_{1}=\mathtt{away}\wedge C=0\wedge \overline{a}=\mathtt{start}_{1}\wedge s^{\prime}_{1}=\mathtt{try}\wedge x^{ \prime}_{1}=0\wedge s^{\prime}_{2}=s_{2}\wedge C^{\prime}=1\right)\vee\\ &\left(s_{1}=\mathtt{try}\wedge x_{1}<\Delta\wedge\overline{a}= \mathtt{approach}_{1}\wedge s^{\prime}_{1}=\mathtt{wait}\wedge x^{\prime}_{1}= 0\wedge s^{\prime}_{2}=s_{2}\wedge C^{\prime}=1\right)\vee\\ &\left(s_{1}=\mathtt{wait}\wedge x_{1}>\delta\wedge\overline{a}= \mathtt{in}_{1}\wedge s^{\prime}_{1}=\mathtt{tunnel}\wedge x^{\prime}_{1}=x_{ 1}\wedge s^{\prime}_{2}=s_{2}\wedge C^{\prime}=1\right)\vee\\ &\left(s_{1}=\mathtt{tunnel}\wedge\overline{a}=\mathtt{out}_{1} \wedge s^{\prime}_{1}=\mathtt{away}\wedge x^{\prime}_{1}=x_{1}\wedge s^{ \prime}_{2}=s_{2}\wedge C^{\prime}=0\right)\end{split} \]  
This part of the transition relation captures how the system changes when train \(T_{1}\) moves, including updates to the global state:  
* Train \(T_{1}\) starts and updates the controller: \[(s_{1}=\mathtt{away}\wedge C=0\wedge\overline{a}=\mathtt{start}_{1})\Rightarrow (\overline{\mathbf{w}}^{\prime}_{T_{1}}=(\mathtt{try},0),\overline{\mathbf{w }}^{\prime}_{T_{2}}=\overline{\mathbf{w}}_{T_{2}},C^{\prime}=1)\] This transition means that if \(T_{1}\) is in the \"away\" state, and the controller is free (\(C=0\)), train \(T_{1}\) starts, moving to the \"try\" state, and resets its clock (\(x_{1}=0\)), while the controller updates to indicate that \(T_{1}\) is attempting to enter the tunnel (\(C^{\prime}=1\)). * Train \(T_{1}\) approaches the tunnel: \[(s_{1}=\mathtt{try}\wedge x_{1}<\Delta\wedge\overline{a}=\mathtt{approach}_{1}) \Rightarrow(\overline{\mathbf{w}}^{\prime}_{T_{1}}=(\mathtt{wait},0),\overline{ \mathbf{w}}^{\prime}_{T_{2}}=\overline{\mathbf{w}}_{T_{2}},C^{\prime}=1)\] This transition occurs when \(T_{1}\) is in the \"try\" state and its clock is less than \(\Delta\). Upon taking the action \"approach_1\", \(T_{1}\) moves to the \"wait\" state and resets its clock. * Train \(T_{1}\) enters the tunnel: \[(s_{1}=\mathtt{wait}\wedge x_{1}>\delta\wedge\overline{a}=\mathtt{in}_{1}) \Rightarrow(\overline{\mathbf{w}}^{\prime}_{T_{1}}=(\mathtt{tunnel},x_{1}), \overline{\mathbf{w}}^{\prime}_{T_{2}}=\overline{\mathbf{w}}_{T_{2}},C^{ \prime}=1)\] Train \(T_{1}\) enters the tunnel when it has waited for a minimum time \(\delta\). It transitions to the \"tunnel\" state while maintaining its current clock. * Train \(T_{1}\) exits the tunnel and resets the controller: \[(s_{1}=\mathtt{tunnel}\wedge\overline{a}=\mathtt{out}_{1})\Rightarrow( \overline{\mathbf{w}}^{\prime}_{T_{1}}=(\mathtt{away},x_{1}),\overline{ \mathbf{w}}^{\prime}_{T_{2}}=\overline{\mathbf{w}}_{T_{2}},C^{\prime}=0)\] After exiting the tunnel, \(T_{1}\) returns to the \"away\" state and the controller is reset to 0.