From d8fba529aba8e352c57974ff6b111808d087d3a0 Mon Sep 17 00:00:00 2001 From: mlaurent Date: Mon, 3 Apr 2023 14:12:56 +0200 Subject: [PATCH] Better handling of test any --- src/mc/api/State.hpp | 2 ++ src/mc/api/strategy/BasicStrategy.hpp | 23 ++++++++++++++++++++--- src/mc/explo/DFSExplorer.cpp | 27 +++++++++++++++++++-------- src/mc/transition/TransitionAny.cpp | 6 ++++-- src/mc/transition/TransitionAny.hpp | 10 ++++++++++ 5 files changed, 55 insertions(+), 13 deletions(-) diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 36e7138498..f67d703514 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -54,6 +54,8 @@ class XBT_PRIVATE State : public xbt::Extendable { std::map sleep_set_; public: + bool is_opened = false; + explicit State(RemoteApp& remote_app); explicit State(RemoteApp& remote_app, std::shared_ptr 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 ca5b3ed353..276d1ffbc3 100644 --- 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(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(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 1067e970de..93c34fc5b7 100644 --- 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 next_state = std::make_shared(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(tmp_stack.back())); + if (not tmp_stack.back()->is_opened) { + opened_states_.push(std::shared_ptr(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(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(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 0f10bb1080..a80a800c12 100644 --- 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 df5954e6ba..b0648119b1 100644 --- 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 #include @@ -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(transition); + if (tested_transition->get_sender() != -1 and tested_transition->get_receiver() != -1) + return true; + } + return false; + } }; class WaitAnyTransition : public Transition { -- 2.20.1