aze model To illustrate the notions of safety and liveness, lets consider the simple maze represented in Figure 7.69(a): you enter by the top and you try to reach the exit; suppose you are not allowed to backtrack. ENTRY ENTRY input enter input enter right output exit right Figure 7.69 (a) A maze and (b) a state machine modeling it Figure 7.69(b) shows a state machine modeling the maze: from state ENTRY the left path leads to state s11. From s11 the left path leads to state EXIT and SO on. To simulate the state machine, we have translated it into the SDL model shown in Figures 7.70 and 7.71. system maze block block1 SIGNAL enter, block1 exit; proc1 _exit enter enter Figure 7.70 System maze and block blockl 258 Validation of Communications Systems with SDL process proc1 ENTRY 'Where ? enter 'Where ?' 'Left' 'Right' ) 'Left' ) ( 'Right' ) Figure 7.71 Process procl modeling the maze We have also created an MSC named OK represented in Figure 7.72, to observe the SDL model: after the input of signal enter, meaning that someone has entered the maze, the MSC waits for the output of signal exit, meaning that the person has found the exit. The MSC Simulation Property of this MSC is set to verify (in the MSC Editor) to detect errors and successes. inst_1_proc1 proc1 enter Figure 7.72 MSC to observe the maze model If we run an exhaustive simulation in depth mode (breadth does not detect livelocks) of the model maze observed by the MSC OK, we get the following results: Number of SCC : 6 Number of transitory SCC : 4 Number of sink SCC : 1 5 intra-scc edges, 5 inter-scc edges Number of states : 9 Number of transitions : 10 Maximum depth reached : 5 duration : 0 mn 0 S Number of exceptions : 0 Number of deadlocks : 1 Number of stop conditions : 0 Number of errors : 0 Number of success : 1 Exhaustive Simulation 259 The Simulator has discovered no errors, one success (generated in the file maze.ok.sl.scn), one deadlock (generated in the file maze.d1.scn) and one livelock (sink see3 (generated in the file maze.sc3.scn). By loading