 the file maze.ok.sl.scn into the Simulator and replaying it, the MSC trace shown in Figure 7.73 has been generated: it matches the expected signal sequence represented in Figure 7.72. The states reached are displayed: entry, s11 and exit. ok_success1 inst_1_proc1 proc1(1) entry enter Figure 7.73 The success scenario detected By loading the file maze.sc3.scn into the Simulator and replaying it, the MSC trace shown in Figure 7.74 has been generated: it shows the path leading to the livelock: states entry and s12. Once state s12 is reached, it is impossible to exit from the loop between states s12 and s121 (as in the real maze). livelock1 inst_1_proc1 proc1 (1) entry enter Figure 7.74 The scenario detected, leading to the livelock The deadlock detected is normal because there is no transition to exit from state exit (Figure 7.75). Now, lets try the liveness mode: choose Execute > Verify and select Liveness as shown in Figure 7.76. We get the following results: Number of states : 9 Number of transitions : 10 3 Strongly connected component. 260 Validation of Communications Systems with SDL ENTRY input enter input enter left right livelock output exit right deadlock Figure 7.75 The deadlock and livelock detected Verify Options Mode: Breadth Depth Supertrace Liveness Scenarios: Exploration: States Limit: Deadlock limit: Depth Limit: Figure 7.76 The top of the Verify Options window in liveness mode Number of sub-exploration : 2 Maximum depth reached : 5 duration : 0 mn 0 S Number of exceptions : 0 Number of deadlocks : 1 Number of stop conditions : 0 Transitions coverage rate : 100.00 (0 transitions not covered) States coverage rate : 100.00 (0 states not covered) Basic blocks coverage rate : 100.00 (0 basic blocks not covered) Number of errors : 0 Number of non -success loops: 2 The Simulator has discovered two nonsuccess loops, generated in the files maze.ll.scn and maze.l2.scn. By loading the file maze.12.scn into the Simulator and replaying it, the MSC trace shown in Figure 7.77 has been generated: this nonsuccess l