Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
MC: this bug was disabling state equality detection
authorMartin Quinson <martin.quinson@loria.fr>
Mon, 10 Apr 2017 23:26:26 +0000 (01:26 +0200)
committerMartin Quinson <martin.quinson@loria.fr>
Mon, 10 Apr 2017 23:28:37 +0000 (01:28 +0200)
The variable is an integer being the maximal amount of state that we
save at the same time (typically 1000). I'm not sure which int value
is equal to "true", but I guess it's not 1000.

src/mc/checker/SafetyChecker.cpp

index ca58cfc..643c734 100644 (file)
@@ -158,7 +158,7 @@ void SafetyChecker::run()
       this->checkNonTermination(next_state.get());
 
     /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
-    if (_sg_mc_max_visited_states == true)
+    if (_sg_mc_max_visited_states > 0)
       visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
 
     /* If this is a new state (or if we don't care about state-equality reduction) */