ears. B. Select Execute > Verify: in front of test1, set Success Limit to 1 and check the halt box, as illustrated in Figure 7.65; the simulation will stop after finding one scenario identical to the MSC testl. C. Press Verify and confirm the verification startup. One second later, the exhaustive simulation stops: mode breadth error limit test1 2 success limit test1 1 , halt error cut test1 = true define verify_stats true verify stopped by a success state Number of states : 65 Number of transitions : 80 Maximum depth reached : 37 Maximum breadth reached : 4 duration : 0 mn 0 S Exhaustive Simulation 253 Verify Options Mode: Breadth Depth Supertrace Liveness Scenarios: Exploration: States Limit: Deadlock limit: Depth Limit: Exception limit: Optimization: Compose Unit: Stop limit: Compress Unit: Scc sink limit: Observers Errors Successes Observers Error Success limit on limit on error limit on limit on success scn_observer test1 Verify Apply Cancel Figure 7.65 Setting success limit for MSC testl Number of exceptions : 4 Number of deadlocks : 0 Number of stop conditions : 0 Number of errors : 132 Number of success : 1 The Simulator has found one success scenario and stopped, as required. In addition, it has discovered 132 errors: an error here is a scenario that is different from the expected MSC testl. As testl describes only one of the many possible execution scenarios, it is normal to get SO many errors. To get no error here, you should create an MSC (using operators) describing all the possible behaviors of the system: this is extremely difficult on an actual system. The success scenario discovered is contained in the file: v76.s1.scn. It could be loaded into the Simulator and replayed. 7.4.11 Exhaustive simulation with GOAL observers More details on GOAL observers are provided in Chapter 5. You will simulate the V.76 SDL model observed by the GOAL observer obs_ex2.obs, built in Chapter 5. If necessary, this file could contain more than one observer. 254 Validation of Communications Systems with SDL 7.4.11.1 Comp