 them. 7.5.2 ObjectGeode: supertrace The supertrace exploration mode in ObjectGeode Simulator is equivalent to bit-state [Holz91] in Tau SDL Suite Validator. A presentation of bit-state is given in Section 7.1.2. To use supertrace, you must do Execute > Verify, select Supertrace, and enter the size of the bits array (the hash table) in the field States Limit, as shown in Figure 7.68. Verify Options Mode: Breadth Depth Supertrace Liveness Scenarios: Exploration: States Limit: 8000000 Deadlock limit: Depth Limit: Figure 7.68 The top of the Verify Options window in supertrace mode In this example, we have set the size of the bits array to 8 million bits, enough to contain 8 million states. We have run the count SDL model, presented in Section 7.2.2, supposed to have 10000 unique states. As the size of the bits array is 800 times greater than the number of states, the collision risk is very low. ObjectGeode found only 830 unique states, whereas Tau SDL Suite Validator using the same model with the same tool configuration found 10000 unique states. This is because ObjectGeode uses only one hashing function, and Tau uses two hashing functions: if one function gives the same hash-code for two different states, the other function has a chance to give two different hash-codes, and therefore to distinguish that the states are not identical. Exhaustive Simulation 257 7.5.3 ObjectGeode: liveness 7.5.3.1 Safety and liveness properties After the end of an exhaustive simulation (in modes breadth or depth) with observers, if you get the following results: Number of errors : 0 Number of success : 350 it proves that the SDL model does not contain any error and that it can reach the success states defined by the observers. This is a safety property. To prove that the SDL model always reaches a success state (a liveness property), you must use an exhaustive simulation mode called liveness: this mode, a variant of the depth mode, detects the loops in the states graph that do not lead to a success state of the observers. 7.5.3.2 The m