art the exhaustive simulation: the Simulator displays the current options and starts the exhaustive simulation: mode breadth deadlock limit 2 exception limit 2 stop limit 2 define stop_cut true define states limit 20000 define depth_limit 0 define verify_stats true Then, after every 8192 global model states, the Simulator displays a line showing the simula- tion progression: number of (unique) global states, number of transitions executed, time elapsed since the beginning of simulation, maximum depth reached in the states graph and maximum breadth reached in the states graph. (8192 states 11676 trans. 1 seconds, depth=34, breadth=934) (16384 states 23502 trans. 2 seconds, depth=40, breadth=1615) (24576 states 35716 trans. 4 seconds, depth=44, breadth=2086) (65536 states 99823 trans. 12 seconds, depth=58, breadth=3269) (73728 states 113177 trans. 14 seconds, depth=61, breadth=3269) (81920 states 126678 trans. 15 seconds, depth=65, breadth=3269) After 17 seconds, the exhaustive simulation stops and the Simulator displays the results: Number of states : 87174 Number of transitions : 135912 Maximum depth reached : 79 Maximum breadth reached : 3269 duration : 0 mn 17 S Number of exceptions : 0 Number of deadlocks : 0 Number of stop conditions : 0 Transitions coverage rate : 100.00 (0 transitions not covered) States coverage rate : 100.00 (0 states not covered) Basic blocks coverage rate : 92.98 (4 basic blocks not covered) The simulation has covered all the 87174 reachable states of the reduced configuration of our SDL model. Obtaining such a coverage of the behavior would take weeks of interac- tive simulation. No exceptions or deadlocks have been found. Exhaustive Simulation 235 7.4.5 Add faults in block dataLink : detect output to Null Now to test more features in the SDL model, we use a larger model configuration: again one signal maximum in each queue and maximum two instances for each process DLC, but now signals can be lost in the block dataLink. To limit the number of states, we restrict the number of retransm