Better handling of test any

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index 36e7138..f67d703 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -54,6 +54,8 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
   std::map<aid_t, Transition> sleep_set_;
 
 public:
+  bool is_opened = false;
+
   explicit State(RemoteApp& remote_app);
   explicit State(RemoteApp& remote_app, std::shared_ptr<State> parent_state);
   /* Returns a positive number if there is another transition to pick, or -1 if not */

diff --git a/src/mc/api/strategy/BasicStrategy.hpp b/src/mc/api/strategy/BasicStrategy.hpp
index ca5b3ed..276d1ff 100644 (file)
--- a/src/mc/api/strategy/BasicStrategy.hpp
+++ b/src/mc/api/strategy/BasicStrategy.hpp
@@ -7,6 +7,8 @@
 #define SIMGRID_MC_BASICSTRATEGY_HPP
 
 #include "src/mc/transition/Transition.hpp"
+#include "src/mc/transition/TransitionAny.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
 
 namespace simgrid::mc {
 
@@ -27,14 +29,23 @@ public:
         return std::make_pair(aid, 0.0);
 
       double dist;
+
+      TestAnyTransition* transition =
+          static_cast<TestAnyTransition*>(actor.get_transition(actor.get_times_considered()));
+
       auto iterator = penalties_.find(aid);
       if (iterator != penalties_.end())
         dist = (*iterator).second;
       else
         dist = 0;
+
+      if (not transition->result())
+        dist += 5000;
+
       if (dist < min.second)
         min = std::make_pair(aid, dist);
     }
+
     if (min.first == -1)
       return std::make_pair(-1, -1000);
     return min;
@@ -45,9 +56,15 @@ public:
   void execute_next(aid_t aid, RemoteApp& app) override
   {
     auto actor = actors_to_run_.at(aid);
-    if (actor.get_transition(actor.get_times_considered())->type_ == Transition::Type::TESTANY)
-      penalties_[aid] = penalties_[aid] + 1.0;
-    return;
+    if (actor.get_transition(actor.get_times_considered())->type_ == Transition::Type::TESTANY) {
+      TestAnyTransition* transition =
+          static_cast<TestAnyTransition*>(actor.get_transition(actor.get_times_considered()));
+      if (not transition->result()) {
+        penalties_[aid] = penalties_[aid] + 1.0;
+        return;
+      }
+    }
+    penalties_[aid] = 0;
   }
 
   void consider_best() override

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 1067e97..93c34fc 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -174,9 +174,10 @@ void DFSExplorer::run()
 
     // If there are processes to interleave and the maximum depth has not been
     // reached then perform one step of the exploration algorithm.
-    XBT_VERB("Execute %ld: %.60s (stack depth: %zu, state: %ld, %zu interleaves out of %zu enabled)",
+    XBT_VERB("Execute %ld: %.60s (stack depth: %zu, state: %ld, %zu interleaves out of %zu enabled, %zu alternatives "
+             "to explore after)",
              state->get_transition()->aid_, state->get_transition()->to_string().c_str(), stack_.size(),
-             state->get_num(), state->count_todo(), state->get_actor_count());
+             state->get_num(), state->count_todo(), state->get_actor_count(), opened_states_.size());
 
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
     std::shared_ptr<State> next_state = std::make_shared<State>(get_remote_app(), state);
@@ -212,7 +213,10 @@ 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()));
+              if (not tmp_stack.back()->is_opened) {
+                opened_states_.push(std::shared_ptr<State>(tmp_stack.back()));
+                tmp_stack.back()->is_opened = true;
+              }
             } else
               XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
           } else {
@@ -220,8 +224,10 @@ void DFSExplorer::run()
                       "transition as todo",
                       issuer_id);
             // If we ended up marking at least a transition, explore it at some point
-            if (prev_state->consider_all() > 0)
+            if (prev_state->consider_all() > 0 and not tmp_stack.back()->is_opened) {
               opened_states_.push(std::shared_ptr<State>(tmp_stack.back()));
+              tmp_stack.back()->is_opened = true;
+            }
           }
           break;
         } else {
@@ -235,8 +241,10 @@ 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)
+    if (stack_.back()->count_todo_multiples() > 0 and not stack_.back()->is_opened) {
       opened_states_.push(std::shared_ptr<State>(stack_.back()));
+      stack_.back()->is_opened = true;
+    }
 
     if (_sg_mc_termination)
       this->check_non_termination(next_state.get());
@@ -307,10 +315,13 @@ void DFSExplorer::backtrack()
   get_remote_app().restore_initial_state();
   on_restore_initial_state_signal(get_remote_app());
   /* Traverse the stack from the state at position start and re-execute the transitions */
-  for (auto& state : backtracking_point->get_recipe()) {
-    state->replay(get_remote_app());
-    on_transition_replay_signal(state, get_remote_app());
+  long i = 1;
+  for (auto& transition : backtracking_point->get_recipe()) {
+    transition->replay(get_remote_app());
+    on_transition_replay_signal(transition, get_remote_app());
+    XBT_DEBUG("[Backtracking in progress] executing state #%ld/#%ld", i, backtracking_point->get_num());
     visited_states_count_++;
+    i++;
   }
   this->restore_stack(backtracking_point);
 }

diff --git a/src/mc/transition/TransitionAny.cpp b/src/mc/transition/TransitionAny.cpp
index 0f10bb1..a80a800 100644 (file)
--- a/src/mc/transition/TransitionAny.cpp
+++ b/src/mc/transition/TransitionAny.cpp
@@ -31,9 +31,11 @@ TestAnyTransition::TestAnyTransition(aid_t issuer, int times_considered, std::st
 }
 std::string TestAnyTransition::to_string(bool verbose) const
 {
-  auto res = xbt::string_printf("TestAny{ ");
-  for (auto const* t : transitions_)
+  auto res = xbt::string_printf("TestAny(%s){ ", this->result() ? "TRUE" : "FALSE");
+  for (auto const* t : transitions_) {
     res += t->to_string(verbose);
+    res += "; ";
+  }
   res += " }";
   return res;
 }

diff --git a/src/mc/transition/TransitionAny.hpp b/src/mc/transition/TransitionAny.hpp
index df5954e..b064811 100644 (file)
--- a/src/mc/transition/TransitionAny.hpp
+++ b/src/mc/transition/TransitionAny.hpp
@@ -8,6 +8,7 @@
 
 #include "src/kernel/actor/SimcallObserver.hpp"
 #include "src/mc/transition/Transition.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
 
 #include <sstream>
 #include <string>
@@ -23,6 +24,15 @@ public:
   bool depends(const Transition* other) const override;
 
   Transition* get_current_transition() const { return transitions_.at(times_considered_); }
+  bool result() const
+  {
+    for (Transition* transition : transitions_) {
+      CommTestTransition* tested_transition = static_cast<CommTestTransition*>(transition);
+      if (tested_transition->get_sender() != -1 and tested_transition->get_receiver() != -1)
+        return true;
+    }
+    return false;
+  }
 };
 
 class WaitAnyTransition : public Transition {