lator (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_v5.pr. C. In process DLC, partition part2, insert a comma followed by L_DataReq in the input containing L_ReleaseReq previously added, as illustrated in Figure 7.50. D. Save the SDL model. 230 Validation of Communications Systems with SDL waitUAdisc V76frame (V76para) L_ReleaseReq, L_DataReq V76para ! present ( UA, DM DLCstopped(me) Figure 7.50 After adding input L_DataReq 7.4.3.4 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. 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 not discovered any exceptions, 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 : 49405 Maximum depth reached : 16 Maximum breadth reached : 6164 duration : 0 mn 1 S Number of exceptions : 0 Number of deadlocks : 0 Number of stop conditions : 0 In the 20 000 explored global states and 49405 explored transitions of the SDL model, we are sure that we have no exceptions and no deadlocks. However, the global states not yet explored by the Simulator may contain errors. 7.4.4 Seventeen seconds to explore 87174 global states To prove that the SDL model is correct, we will try to explore all its reachable states. We first use the following reduced configuration: one signal maximum in each queue, maximum two instances for each process DLC, and signals never lost in the block dataLink. Exhaustive Simulation 231 7.4.4.1 Start the Simulator A. 