|
@@ -141,11 +141,11 @@ public class OSExplorer {
|
|
|
// Check if we already visited this state, in which case, recover that state, otherwise save the state in the map
|
|
|
if(statesMap.containsKey(os.hashCode())) {
|
|
|
OutState m_os = statesMap.get(os.hashCode());
|
|
|
- if(m_os.equals(os)) {
|
|
|
+ if(m_os.equals(os)) { // Check that we're not getting a collision
|
|
|
os = m_os; // Use the state extracted from the map
|
|
|
} else {
|
|
|
logger.error("Found an hash collision between state " + os + " and the state already in map " + m_os);
|
|
|
- throw new DuPALAnalyzerException("hash collision between two different OutStates")
|
|
|
+ throw new DuPALAnalyzerException("hash collision between two different OutStates");
|
|
|
}
|
|
|
} else statesMap.put(os.hashCode(), os);
|
|
|
|