th SDL C. Select Tools > SDL & MSC Simulator. D. In the ObjectGeode Launcher, remove any file other than v76.pr, press the Build button, then, if there are no errors, press the Execute button. The Simulator starts. E. If the Simulator has not executed automatically the four start transitions (step should be equal to 4), the file v76.startup is missing or incorrect (see Chapter 4). The exhaustive simulation starts from the current SDL model state, here Step 4. F. Check that the feed commands (loaded by the file v76.startup) have been executed. See Chapter 4 if typing the Simulator command list feed does not give the following result: > list feed feed dlcbsu l_releasereq(0) feed dlcbsu setparmresp( feed dlcbsu l_estabresp ( ( ) feed dlcasu l_datareq (1 , 39) feed dlcasu l_datareq (0 86) feed dlcasu l_releasereq (1) feed dlcasu l_setparmreq ( ) feed dlcasu l_estabreq( (1) feed dlcasu l_estabreq(0) 7.4.1.2 Run the exhaustive simulation A. In the Simulator, select Execute > Verify: the Verify Options window appears, as shown in Figure 7.44. Do NOT use the Simulator button Verify B. In the Exploration part, enter 20000 for States Limit (you could also type the equivalent Simulator textual command define states_limit 20000). C. Press the button Verify and confirm the verification startup: the Simulator displays the current options and starts the exhaustive simulation: mode breadth define edges_dump " define states_dump deadlock limit 2 exception limit 2 stop limit 2 define stop_cut true define states_limit 20000 define depth_limit 0 define verify_stats true As expected, the exhaustive simulation stops after the exploration of 20000 global SDL model states. Only one second has been necessary to discover 568 exceptions, as indicated in the results: (8192 states 19364 trans. 0 sec, depth=13, breadth=1897) (16384 states 39243 trans. 1 sec, depth=15, breadth=3873) verify stopped by states limit Exhaustive Simulation 223 Verify Options Mode: Breadth Depth Supertrace Liveness Scenarios: Exploration: States Limit: Deadlock limi