al event (error or success). It means that even if the exploration is not finished because the states graph is too large, the simulation can produce results. There is no need to wait till the end of the computation of a state graph before you start checking properties on it. Exhaustive Simulation 185 In addition, as the simulators can be tuned to stop after discovering one error, the simulation campaigns are very fast. 7.2 SIMPLE EXAMPLES To illustrate how the exhaustive simulation actually works, we have first run it on two very simple SDL examples: the ping TCP/IP command and a model with counters. 7.2.1 Exhaustive simulation of the ping TCP/IP command We have created an SDL model with very few global states: the ping model has only eight global states; therefore, its states graph fits in less than one page. 7.2.1.1 The ping TCP/IP command model We have created a simplified SDL model of the ping command. Ping is generally part of TCP/IP implementations, available, for example, in Unix or Windows. This command is generally used to test if a certain host is present on a network and responding. The ping command, executed on a client computer, transmits an echo request to the server computer. The server answers with an echo reply. The following example shows the use of ping on a Windows NT client to test if the server named nepal is responding (similar results can be obtained in Unix): :\>ping nepal Pinging nepal [196.200.100.99] with 32 data octets: Reply from 196.200.100.99 : octets=32 time<10ms TTL=128 In the following example, some firewalls certainly prevent the ping command from reaching the server www.airfrance.com: C:\>ping www.airfrance.com Pinging double6.airfrance.com [193.57.244.15] with 32 data octets: Waiting delay exceeded. The SDL model of ping contains two blocks, client and server, as depicted in Figure 7.5, connected through the channel IP. The signal names are self-explanatory. Each block contains one process, named, respectively, client and server, as shown in Figure 7.6. Figure 7.7 shows the c