me VIA dlcDL ready waitEstabResp (DM :(. DLCpeer).)) VIA dlcDL ready Figure 7.63 The input L_ReleaseReq added to dispatch A. Exit from the Simulator (answering No to the question). Do not exit from the Editor. B. In Windows (or Unix), make a copy of the file v76.pr into v76_v8.pr. C. Add the missing parts in process dispatch, as depicted in Figures 7.63 and 7.64. D. Save the SDL model. 248 Validation of Communications Systems with SDL process dispatch(1, 1) waitUA V76frame DLCstopped (V76para) (DLCnum) V76para ! present L_Releaselnd(DLCnum) DLCs(DLCnum):= NULL DLCs(V76para DLCs(V76para UA!DLCi) DM!DLCi) ( Null ) Null ) V76frame(V76plara) V76frame(V 6para) TO DLCs(V76p.ra TO DLCs W76para ! UA ! DLCi) ! DM ! DLCi) ready ready ready Figure 7.64 The answer DM added to dispatch 7.4.8 Eleven minutes, 2.8 million states, no error 7.4.8.1 Run again the exhaustive simulation We simply rerun the exhaustive simulation to check that no error has been introduced and to see if the basic block previously numbered 15 is covered. A. In the SDL Editor, unload all files except v76.pr. B. If the ObjectGeode Launcher is not running, in the Editor select Tools > SDL & MSC Sim- ulator. C. In the ObjectGeode Launcher, remove any file other than v76.pr, press the Build button, then, if there are no errors, press the Execute button. D. In the Simulator, select Edit > Configuration and set Reasonable environment to on (box checked) and Loose time progression to off (box not checked). E. Select Edit > Filter Conditions and check that the filters are the same as in Section 7.4.5.2 (especially the signal loss is no longer filtered). F. Select Execute > Verify: press Verify and confirm the verification startup. The exhaustive simulation starts: mode breadth deadlock limit 2 exception limit 2 , halt stop limit 2 define stop_cut true define states_limit 0 Exhaustive Simulation 249 define depth_limit 0 define verify_stats true (8192 states 12178 trans. 1s., depth=22, breadth=1607) (16384 states 25318 trans. 2 S., depth=25, breadth=3084) (1368064 