## 4 Simulation and Analysis of HCPN Based TSP Model
### State Space Analysis  
In this section, we describe the properties of the proposed HCPN models in detail. Two full state spaces are generated based on the current initial marking, and the statistics obtained by full state space analysis are illustrated in Table 3, which can be used to analyze the boundness and liveness of the TSP control model with transit vehicle go-straight or turn-left through the crossing zone. In order to verify the correctness and validation of these two strategies, and to save space, the partial state spaces are employed in Figure 4. Arcs in Figure 4 are listed in Appendix B. Compared with the state space of the normal four-phase traffic light control model, the number of nodes and arcs in the state spaces and the Scc graph both increase greatly because the proposed model represents the interactions between transit and traffic controller, and enumerates all the possible responses made by the traffic controller. These functions are exactly what traditional TSP control strategies cannot provide. In Figure 4a, node1 represents the initial state of the TSP control system, we see that node1 has three enabled binding elements:  
Arc1:1\(\rightarrow\)2 (phase1'enter_all_in_red:{c=R})  
Arc2:1\(\rightarrow\)3 (green_extension'Init1:{s=\"Bus Request GE\", n=10})  
Arc3:1\(\rightarrow\)4 (red_truncation'Init2:{s=\"Bus Request RT\", n=10})  
These arcs lead to the markings represented by nodes2, node3, and node4, respectively. Node3 and node4 represent that an approaching transit vehicle is detected at the initial state; actually, the transit priority request issued at this time will be neglected. Node2 represents the model entering the all-in-red state. Nodes2, node5, and node9 have two enabled binding elements:  
Arc4:2\(\rightarrow\)5 (phase1'c1:{EGtick=2, ELtick=2, NGtick=2, NLtick=2})  
Arc11:5\(\rightarrow\)9 (phase1'c1:{EGtick=1, ELtick=1, NGtick=1, NLtick=1})  
We illustrate the countdown of the time stamp in the all-in-red state. The markings represented by nodes7, node11, and node15 are identical to the node4 so that the transition Init2 in red_truncation fires. Similarly, the markings represented by nodes6, node10, and node14 are identical to the node3 so that the transition Init1 in green_extension fires. We found that the sequence of states that really make sense is {node1, node2, node5, node9, node13,... }. Figure 4b shows the partial state spaces concerning the green extension strategy. Note that in a real transit signal priority control system, no one knows when an approaching transit vehicle is detected. Meanwhile, we know that once a transit vehicle is detected, the response of the TSP control \begin{table}
\begin{tabular}{l c c c c c c c c c} \hline \hline \multirow{2}{*}{**Model**} & \multicolumn{2}{c}{**State Spaces**} & \multicolumn{2}{c}{**Scc Graph**} & \multicolumn{2}{c}{**Boundness**} & \multirow{2}{*}{**Dead**} & \multirow{2}{*}{**Live**} & \multirow{2}{*}{**Faimess**} \\ \cline{2-2} \cline{5-5}  & **Nodes** & & & & & & & & \\ \hline Normal & 132 & 132 & 1 & 0 & 1 & 0 & None & All & All \\ TSP & 1188 & 1986 & 664 & 1458 & 1 & 0 & None & Part & Part \\ \hline \hline \end{tabular} Part: transitions in phase1, phase2, phase3, and phase4 submodules.  
\end{table} 
Table 3: Statistics of simulations of Hierarchical Colored Petri nets (HCPN) model. TSP: transit signal priority. system to the priority request is a deterministic process. There are five groups of nodes and arcs,i.e., {node110, node117, node95, Arc208, Arc221}, {node116, node123, node101, Arc219, Arc232}, {node122, node129, node107, Arc230, Arc243}, {node128, node135, node113, Arc241, Arc254}, and {node134, node141, node119, Arc252, Arc265} that indicate the state change of the TSP control system when the priority request is received in the east-westward go-straight green time of 10 to 15 s. In Figure 4b, node98 is reachable from node13, but is not reachable from node14 and node15. Figure 4c demonstrates the partial state spaces concerning the red truncation strategy.