n stored in memory: if the global state is new, it is stored. When all possible transitions have been executed from every state, the simulation is terminated. Two Simulator variables (define states_dump 'sta.wri' and define edges_dump 'edg.wri enable the generation of two textual files, one containing the transitions of the reachable states graph (here edg.wri) and the other containing the contents of each model's global state (here sta.wri). We have used those files to manually draw the reachable states graph of our SDL model, shown in Figure 7.9. The exhaustive simulation is started from the global state S1: process client is in state ready, its input queue is empty process server is in state idle, its input queue is empty. A. From global state S1, process client inputs the external signal PING (which was not present in the queue due to the feed ObjectGeode feature), outputs signal echo_req, starts timer T1 and enters state wait. The next global state is S2. From global state S2, process server inputs signal echo_req, and stops in the decision 'Alive ?'. The next global state is S3. C. From global state S3, the Simulator selects the answer 'Yes' after the decision 'Alive ?'. Process server outputs signal echo_reply. The next global state is S4. D. From global state S4, process client in state wait inputs echo_reply, stops timer T1 and outputs signal REPLY with parameter 'Host is alive'. The next global state is S1. E. The Simulator recognizes that S1 has already been explored, thus will not loop forever. It backtracks to global state S3, from where a transition has not been executed. F. From global state S3, the Simulator selects the answer 'No' after the decision 'Alive ?'. Process server does not output signal echo_reply. The next global state is S5. 188 Validation of Communications Systems with SDL client server state=ready state=idle input echo_reply input PING state=wait echo_req state=idle T1 active input echo_req substate, state=wait decision T1 active 'Alive ?' output echo_reply state=wait echo_reply st