n of E L_EstabConf), followed by 4 x4x2x5x4x5x2x5 32 000 for the XID exchange, followed by4x4x4x2x5=640 for the data transfer, followed by 4x4x5x2x5x4x5x2x6x4x3x4=9216000 for the connec- tion release. Therefore, the probability to simulate the expected behavior testl in this configuration can be estimated at: 1/77 760 X 32 000 x 640 x 9216000 = 1/14.677.000.000.000.000.000. 178 Validation of Communications Systems with SDL As certain choices are equivalent, the probability is not SO low, but certainly too small to verify the MSC, even performing years of random simulation. This is why we must guide the simulation to reduce the number of possibilities at each simulation step, as explained in the next section. 6.3.3.2 MSC-driven random simulation In a way similar to Tau SDL Suite Validator, we will perform a simulation guided by the MSC testl. A. Quit the Simulator and the ObjectGeode Launcher. B. With a text editor, check that the file v76.startup contains a comment delimiter -- as below in front of the feed source line: source v76_feed.wri C. In the SDL Editor, check that the only files loaded are v76.pr and testl.msc. D. In the SDL Editor, select the MSC testl and choose Edit > MSC Simulation Properties: in the Goal part, select the option Verify. Press OK and save the MSC. E. Select Tools > SDL & MSC Simulator. F. In the ObjectGeode Launcher, remove any file other than v76.pr and testl.msc, press the Build button, then press the Execute button. G. Check that the current simulation step is 4 (otherwise your startup file has not been executed). If not, execute the 4 start transitions. H. Press the button Traces: Off. I. Press the button MSC-driven: Activate: this adds the filter condition filter error(observation), which removes the transitions leading to a violation of the observer MSC. J. Choose Edit > Configuration, select the box Reasonable environment and deselect the box Loose time progression. K. Select Edit > Filter Conditions and add successively: trans atob (1) : decision_lose_the_frame ('Yes') trans bt