state of each process instance is composed of the state of the state machine, the value of each variable and timer and the value of the predefined expressions self, offspring, sender and parent. The state of each input queue is composed of the name of each signal present and of the value of each parameter of each signal. Exhaustive Simulation 183 state sD process P1(1) state= s1 X= True queue= sig1 (45) process P2(1) state= s6 n= 15 SDL model states graph queue= empty Figure 7.2 Contents of each state of an SDL model To avoid infinite state graphs, the value of Now, the SDL time, is not stored, but special algorithms allow timers to work. 7.1.1.3 Breadth-first and depth-first exploration To explore a graph, there are two main possibilities: either to explore one level completely before exploring the next level or to go down through all the levels and then return to finish the unexecuted transitions. Figure 7.3 shows the two exploration modes, with numbers indicating the exploration order: on the left part, from state sA, breadth-first explores sB, then returns to sA, explores sC, returns to sA and finally explores sD. Now that all transitions from sA have been executed, the exploration goes one level down. From sB, sE and sF are reached; from sC, there are no transitions; from sD, sG is reached. The exploration goes one level down: the only transition is from sF back to sC. The exploration is finished. On the right part of Figure 7.3, from state sA, depth-first explores sB and sE. No transition exists from sE, the exploration backtracks to sB, explores sF and sC. No transition exists from sC, the exploration backtracks to sA. From sA, sC is reached, the exploration backtracks to sA, and explores sD and sG. The exploration is finished. Global SDL state SDL transition breadth-first depth-first Figure 7.3 Breadth-first and depth-first exploration 184 Validation of Communications Systems with SDL 7.1.2 Bit-state simulation To reduce memory usage during the graph exploration, the bit-state algorithm [Holz91] stores th