: 24847 Reports: 5 Depth: 300 Symbol coverage: 93.60 Time: 10:07:07 Transitions: 60000 States: 37274 Reports: 5 Depth: 138 Symbol coverage: 93.60 Time: 10:07:07 204 Validation of Communications Systems with SDL Transitions: 6940000 States: 4329979 Reports: 5 Depth: 215 Symbol coverage: 93.60 Time: 10:09:13 Transitions: 6960000 States: 4342489 Reports: 5 Depth: 92 Symbol coverage: 93.60 Time: 10:09:13 Transitions: 6980000 States: 4354917 Reports: 5 Depth: 172 Symbol coverage: 93.60 Time: 10:09:13 Bit state exploration statistics No of reports: 5. Generated states: 6985039. Truncated paths: 0. Unique system states: 4358006. Size of hash table: 2000000000 (250000000 bytes) No of bits set in hash table: 8675533 Collision risk: 0 % Max depth: 6530 Current depth: -1 Min state size: 212 Max state size: 584 Symbol coverage : 93.60 After only 2 min and 6 S, the bit-state simulation is terminated. 4358006 unique global states have been explored (you may get a different number), and the memory usage has been almost constant and equal to 255 MB only: the bits array plus a few megabytes. As the maximum depth indicated is equal to 6530, the search depth limit used, 15000, was enough. Because the hash table used could store up to 250 millions X 8 = 2 billions of bits, the collision risk is evaluated at 0%. H. The Report Viewer appears. Double-click on the Output box to unfold it, as shown in Figure 7.25. I. The first box from the left shows that signal V76frame has been transmitted to a Null Pid by process dispatch in block DLCa. J. Double-click on this box: the MSC Editor displays the trace of the scenario leading to the error; this trace is shown in Figure 7.26. A attempts to establish DLC number 0; as the response L_EstabResp from B is too late, A has received an L_ReleaseInd, meaning failure of DLC establishment; the L_EstabResp from B finally arrives (E1 in the MSC), dispatch in B creates an instance of DLC, which transmits a v76frame containing a UA; reaching dispatch in A, the v76frame should have been transmitted to the