e hash-code of each model state instead of the whole state itself. Figure 7.4 illustrates (partially) the idea of this algorithm. After executing an SDL transi- tion (1), rather than comparing the obtained state and storing it if it is new, bit-state computes h, the hash-code of the state (2) (the hash-code is a kind of checksum). For example, if h = 4, the fourth element in an array of bits is examined: as it contains 0, it means that the state has never been explored (3). We set the fourth element to 1 in the array (4). After execution of another transition (5), the hash-code is computed (6): as the corresponding bit in the array already contains 1, it means that the state has already been explored (or that two different states have the same hash-code) (7). 1. Execution of an 5. Execution of an SDL transition SDL transition state state 2. Computation of the 6. Computation of the hash code of the state hash code of the state h:= hash (state) h:= hash (state) 8. Etc. 3. Bit 4 in table = 0 4. Set bit 4 in table to 1 7. Bit 2 in table = 1 means new state means state already explored or collision Figure 7.4 Bit-state exploration of the states graph This algorithm is implemented in ObjectGeode Simulator (named Supertrace) and in Tau SDL Suite Validator. To reduce the collision risk, the number of states to explore must be around 100 times smaller than the size of the array of bits. For example, for a system with 16 millions of states, the memory usage is only: 16 millions X 100/8 = 200 MB. In addition, two hash-coding functions can be used instead of one. Bit-state is very efficient, but note that it does not perform a true exhaustive simulation, because it is impossible to guarantee that a hash-coding function will not sometimes give the same result for two different states. 7.1.3 On-the-fly validation During the exploration of a state graph, after each execution of an SDL transition, the simulators check that no error occurred (receiver dead, no deadlock etc.) and that the observers, if any, do not detect any speci