 Sons, Ltd ISBN: 0-470-85286-0 182 Validation of Communications Systems with SDL called the reachable states. The global states and the transitions between them are an oriented graph, called the states graph. 7.1.1.1 All the states must be stored Figure 7.1 illustrates how exhaustive exploration works. Note that not all the required data structures are described. To execute all the behaviors of an SDL model, an SDL transition from a certain global state of the model is executed (1). The obtained global state of the SDL model is compared with each previously stored state (2). If none are identical to it, the new state sD is stored (3). From sD, an SDL transition is executed (4). Again, the obtained global state is compared with each previously stored state (5). If it is identical to sC (6), an edge is stored from sD to sC (7). The exploration stops when all the transitions from all the states have been executed. 3. No, it is a new 6. Yes, it is identical state sD, store it to state sC 1. Execution of an SDL transition state 4. Execution of an 7. Store an edge SDL transition from sD to sC 2. Is the state identical to sA, sB or sC? state 5. Is the state identical to sA, sB, sC or sD? Figure 7.1 Exhaustive exploration of the states graph Because all the global states of the SDL model must be stored in RAM (otherwise the com- parison would be too slow), exhaustive exploration could require a huge amount of memory. Fortunately, exhaustive algorithms do not need to store each whole SDL state, but, example, cut each state in slices and store only the slices that have changed after a transition. In an SDL system, when a transition is executed, most of the times the only parts that change are the sender process and the receiver process instances; for a system with, for example, 10 process instances, only 2 instances will change between 2 states. 7.1.1.2 What is a global state As shown in Figure 7.2, each global state is a snapshot of the SDL model. It contains the state of each process instance and of its input queue. The 