a inst_dlcb inst_dlca inst_dlcb |_releasereq( 0) I_releasereq( 0) I_releaseind( 0) _releaseind( releaseind( 0) I_releaseind( 0) Figure 7.80 The MSC to observe the disconnection Compile the SDL model plus the MSC, and launch the Simulator. Replay the scenario cnx1.scn. Set Reasonable environment to on and Loose time progression to off. Delete all the feeds except the L_ReleaseReq(0) on side A. Run the liveness simulation. After one second, it stops and you get three nonsuccess loops. Source v76_feed.wri to restore the feeds, and start the MSC trace. Load and replay the generated scenario v76.11.scn: you see that after a UA response is lost by dataLink, process DLC side A is stuck in state waitUAdisc. To correct the protocol, a timer could be added, or the disconnected state could be entered before receiving the response of the peer. 7.6 STRATEGY TO MASTER EXHAUSTIVE SIMULATION 7.6.1 Which simulation modes should be used In Tau SDL Suite Validator, use the bit-state mode, working better than supertrace in Object- Geode, rather than exhaustive. Exhaustive Simulation 263 In ObjectGeode, use the true exhaustive simulation modes (breadth, depth or liveness) rather than supertrace (named bit-state in Tau SDL Suite Validator). 7.6.2 If simulation never terminates You will certainly be faced with SDL models whose simulation in exhaustive or bit-state modes never terminates, because the model has too many global states. In exhaustive mode, when you see that the RAM memory of your computer is full, you can stop the simulation, because it becomes extremely slow. In bit-state, the memory is allocated at the beginning (the size of the bits array plus a few extra megabytes) and no longer increases. 7.6.2.1 Tau SDL Suite Validator Lets suppose we use the bit-state exploration mode. 1. Do not activate the Advanced mode, where all kinds of events have the same priority. 2. Use the command Define-Max-Input-Port-Length to limit the number of signals in each process input queue to one (the default is two). 3. For each dynamically cre