ator starts a bit-state exploration: MSC Test1 loaded. Root of behavior tree set to current system state Reports cleared Bit state exploration started. After less than one second, the Validator has finished: Bit state exploration statistics * No of reports: 4. Generated states: 69. Truncated paths: 0. Unique system states: 62. Size of hash table: 8000000 (1000000 bytes) No of bits set in hash table: 124 Symbol coverage : 78.03 MSC Test1 verified The Report Viewer appears, as in Figure 7.41, showing four reports. There is one scenario satisfying the MSC and two scenarios violating the MSC. There are two violations because the MSC testl does not contain any possible behavior expected from the system. To view the corresponding MSC trace, double-click on one box in the Report Viewer. Report Viewer 4 reports 1 Deadlock 2 MSCViolation 1 MSCVerification MSC Test1 verified Depth: 47 Figure 7.41 The Report Viewer showing that the MSC is satisfied The textual command Define-MSC-Verification-Algorithm can be used to change the algo- rithm used by the Verify MSC command. The default is BitState, the other alternative is TreeSearch. 220 Validation of Communications Systems with SDL 7.3.10 Bit-state simulation with observer processes You will use the observer process created in Chapter 5, shown in Figure 5.36. This observer detects if the variable uData in process dispatch in block DLCa contains 55. A. In the Organizer, select V76test, choose Edit > Connect, choose To an existing file, press the folder-shaped icon and connect to the file v76test_obs.ssy. B. In the Organizer, select obs, choose Edit > Connect, choose To an existing file, press the folder-shaped icon, select the file obs.sbk, check Expand substructure and press Connect. C. In the Organizer, press the save button. The Organizer should now look like Figure 7.42. Organizer - v76.sdt File Edit View Generate Tools Help V76test v76test_obs.ssy DLCa: V76_DLC DLCb : V76_DLC dataLink nw datalink.sbk AtoB toPeer BtoA : toPeer toPeer topeer.spt nw obs.sbk nw obs1.spr Syste