Use a multiset to handle opened states, and ensures a reproductible order on differen...

From cppreference: The order of the elements that compare equivalent is the order of insertion and does not change.
 (since C++11)

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index eb3b8e7..93848b0 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -218,7 +218,7 @@ void DFSExplorer::run()
           if (prev_state->is_actor_enabled(issuer_id)) {
             if (not prev_state->is_actor_done(issuer_id)) {
               prev_state->consider_one(issuer_id);
-              opened_states_.push(std::shared_ptr<State>(tmp_stack.back()));
+              opened_states_.emplace(tmp_stack.back());
             } else
               XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
           } else {
@@ -227,7 +227,7 @@ void DFSExplorer::run()
                       issuer_id);
             // If we ended up marking at least a transition, explore it at some point
             if (prev_state->consider_all() > 0)
-              opened_states_.push(std::shared_ptr<State>(tmp_stack.back()));
+              opened_states_.emplace(tmp_stack.back());
           }
           break;
         } else {
@@ -242,7 +242,7 @@ void DFSExplorer::run()
     // Before leaving that state, if the transition we just took can be taken multiple times, we
     // need to give it to the opened states
     if (stack_.back()->count_todo_multiples() > 0)
-      opened_states_.push(std::shared_ptr<State>(stack_.back()));
+      opened_states_.emplace(stack_.back());
 
     if (_sg_mc_termination)
       this->check_non_termination(next_state.get());
@@ -292,8 +292,8 @@ void DFSExplorer::backtrack()
     return;
   }
 
-  std::shared_ptr<State> backtracking_point = opened_states_.top(); // Take the point with smallest distance
-  opened_states_.pop();
+  // Take the point with smallest distance
+  auto backtracking_point = opened_states_.extract(begin(opened_states_)).value();
 
   // if the smallest distance corresponded to no enable actor, remove this and let the
   // exploration ask again for a backtrack
@@ -361,7 +361,7 @@ DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool ne
     stack_.back()->consider_all();
   }
   if (stack_.back()->count_todo_multiples() > 1)
-    opened_states_.push(std::shared_ptr<State>(stack_.back()));
+    opened_states_.emplace(stack_.back());
 }
 
 Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor)

diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp
index 3e8a45b..dae59bb 100644 (file)
--- a/src/mc/explo/DFSExplorer.hpp
+++ b/src/mc/explo/DFSExplorer.hpp
@@ -15,6 +15,7 @@
 
 #include <list>
 #include <memory>
+#include <set>
 #include <string>
 #include <vector>
 
@@ -26,9 +27,9 @@ typedef std::list<std::shared_ptr<State>> stack_t;
  * regarding the chosen guide in the last state. */
 class OpenedStatesCompare {
 public:
-  bool operator()(std::shared_ptr<State> const& lhs, std::shared_ptr<State> const& rhs)
+  bool operator()(std::shared_ptr<State> const& lhs, std::shared_ptr<State> const& rhs) const
   {
-    return lhs->next_transition_guided().second < rhs->next_transition_guided().second;
+    return lhs->next_transition_guided().second > rhs->next_transition_guided().second;
   }
 };
 
@@ -113,7 +114,7 @@ private:
 
   /** Opened states are states that still contains todo actors.
    *  When backtracking, we pick a state from it*/
-  std::priority_queue<std::shared_ptr<State>, std::vector<std::shared_ptr<State>>, OpenedStatesCompare> opened_states_;
+  std::multiset<std::shared_ptr<State>, OpenedStatesCompare> opened_states_;
 
   /** Change current stack_ value to correspond to the one we would have
    *  had if we executed transition to get to state. This is required when