para) TO DLCs(V76para TO DLCs(V76para I DLCi) DISC ! DLCi) L_Setparmind DLCs(V76para DLCs(V76para waitParmResp UA DLCi) DM DLCi) L_SetparmRésp V76frame ( Null ) V76frame V76frame(V76para) V76frame(V76para) (XIDresp : 0) TO DLCs(V76para TO DLCs(V76para VIA dlcDL UA ! DLCi) DM ! DLCi) ready Figure 7.54 Process dispatch partition part1_1 240 Validation of Communications Systems with SDL process dispatch(1, 1) waitEstabResp DLCpeer:= V76para ! SABME ! DLCi Saves L_EstabResp V76frame V76frame DLCs(DLCpeer) Creates ( Null ) instance of (DLCpeer, False) process DLC L Establnd L_Releaselnd Stores into the DLCs(DLCpeer) (DLCpeer) (DLCpeer) table the PIDof the := OFFSPRING instance just created. V76frame waitEstabResp (DM :(. DLCpeer.)) ready VIA dlcDL Figure 7.55 Process dispatch partition part1_2 process dispatch(1, 1) waitUA V76frame DLCstopped (V76para) (DLCnum) V76para ! present L_Releaselnd(DLCnum) DLCs(DLCnum):=NULL DLCs(V76para UA DLCi) ( Null ) ready V76frame(V76para) TO DLCs(V76para ! UA ! DLCi) ready Figure 7.56 Process dispatch partition part2 7.4.6 Twenty-two seconds to detect missing save of L_DataReq 7.4.6.1 Run again the exhaustive simulation To save time, we will set the simulator to stop after discovering two exceptions, rather than finishing the whole reachable states exploration. 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. Exhaustive Simulation 241 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. Check that the Simulator has executed automatically the four start transitions. F. 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). G. Select Execute > Verify