 save of signal L_ReleaseReq are specified. Therefore, this signal has been discarded. The discarded L_ReleaseReq signal is shown in Figure 7.47. 7.4.2.3 Correct the exception After examining the error, we decide that it is better losing L_ReleaseReq than saving it. Therefore, you will add a dummy input of signal L_ReleaseReq in state waitUAdisc of process 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_v4.pr. C. In process DLC, partition part2, select the input v76frame under the state waitUAdisc, and add an input containing L_ReleaseReq followed by nextstate dash, as illustrated in Figure 7.48. waitUAdisc V76frame (V76para) L_ReleaseReq V76para ! present ( UA, DM DLCstopped(me) Figure 7.48 After adding input L_ReleaseReq D. Save the SDL model. 7.4.3 One second to detect missing input L_DataReq 7.4.3.1 Run again the exhaustive simulation 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. 228 Validation of Communications Systems with SDL 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 Execute > Verify: enter 20 000 for States Limit, press Verify and confirm the verification startup. This time, the exhaustive simulation has discovered 1 exception instead of 77, as indicated in the results: (8192 states 19791 trans. 0 seconds, depth=13, breadth=1929) (16384 states 40370 trans. 1 seconds, depth=15, breadth=3964) verify stopped by states limit Number of states : 20000 Number of transitions : 49401 Maximum depth reached : 16 Maximum breadth reached : 6163 duration : 0 mn 1 S Number of exceptions : 1 Number of deadlocks : 0 Number of stop conditions : 0 It proves that the model has been improved again by the previous correction. Note that we do not know if the SDL model still provides the re