H. Press Verify and confirm the verification startup. As expected, the exhaustive simulation stops after finding two exceptions in the SDL model, as indicated in the results: (8192 states 12209 trans. 1 S., depth=23, breadth=1502) (16384 states 25489 trans. 3 S., depth=26, breadth=2863) (122880 states 194497 trans. 21 S., depth=37, breadth=18248) (131072 states 207854 trans. 22 S., depth=37, breadth=18248) verify stopped by an exception state Number of states : 131367 Number of transitions : 208355 Maximum depth reached : 37 Maximum breadth reached : 18248 duration : 0 mn 22 S Number of exceptions : 2 Number of deadlocks : 0 7.4.6.2 Replay the exception scenario Again, the Simulator has generated two files containing the exception scenarios: v76.x1.scn and v76.x2.scn. A. In the Simulator, select File > Scenario > Load, and open v76.x1.scn. B. Press on Start MSC. C. Press the button Redo: All. The Simulator replays the scenario, reaches the exception, and displays: Unexpected signal l_datareq in dlca!dlc (2) line 1037 of v76.pr 39 transitions executed end of scenario execution The Editor displays the MSC trace of the exception scenario, shown in Figure 7.57. 242 Validation of Communications Systems with SDL bug_exh5 <nddica.dispatch inst_1_atobinst_1_btoa dlcb.dispatch dlca/ datalink/ datalink/ dlcb/ dispatch(1) atob(1) btoa(1) dispatch( (1) inst_1_dlca.dlc I_estabreq(1 dlca/dlc(1) v76frame( sabme (. 1.) ) t320(12.0) v76frame( sabme : (.1.) ) I_estabind(1) inst_1_dlcb.dlc _estabresp dlcb/dlc(1) v76framed v76frame(ua:(.1.) (ua:(.1.) ) v76frame( (.1.) ) I_estabconf( 1 I_setparmreq v76frame( xidcmd : 0 v76frame xidcmd : 0 ) I_setparmind I_releasereq( I_releasereg v76frame( disc : (. v76frame( disc : . . . 1 . ) ) l_estabreq( 0) inst_2_dlca.dlc dlca/dlc(2) 76frame( sabme : ( t320(12.0) v76frame( xidresp I setparmresp v76frame( disc : (.1.) v76frame( ua (.1.) dicstopped (1) v76frame(ua:(.1.)) v76frame(_ua:(.1.)) dicstopped 1) _releaseind( 1 releaseind( 1 I_datareq( 0,86 I_datareq( 0,86 Figure 7.57 MSC trace of the exce