X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/26aa45fc9c9dde4d372797ba159a75baf9e7856b..992bc1ec57d376cf14b124ea21b58b30f1e162f9:/src/mc/explo/DFSExplorer.cpp diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 286c3f70e2..d7e0f1e7a9 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -24,8 +24,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc, "DFS exploration algorithm of the model-checker"); -namespace simgrid { -namespace mc { +namespace simgrid::mc { xbt::signal DFSExplorer::on_exploration_start_signal; xbt::signal DFSExplorer::on_backtracking_signal; @@ -42,8 +41,8 @@ xbt::signal DFSExplorer::on_log_state_signal; void DFSExplorer::check_non_termination(const State* current_state) { for (auto state = stack_.rbegin(); state != stack_.rend(); ++state) - if (Api::get().snapshot_equal((*state)->system_state_.get(), current_state->system_state_.get())) { - XBT_INFO("Non-progressive cycle: state %ld -> state %ld", (*state)->num_, current_state->num_); + if (Api::get().snapshot_equal((*state)->get_system_state(), current_state->get_system_state())) { + XBT_INFO("Non-progressive cycle: state %ld -> state %ld", (*state)->get_num(), current_state->get_num()); XBT_INFO("******************************************"); XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); XBT_INFO("******************************************"); @@ -96,7 +95,8 @@ void DFSExplorer::run() State* state = stack_.back().get(); XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration depth=%zu (state:%ld; %zu interleaves)", stack_.size(), state->num_, state->count_todo()); + XBT_DEBUG("Exploration depth=%zu (state:%ld; %zu interleaves)", stack_.size(), state->get_num(), + state->count_todo()); Api::get().mc_inc_visited_states(); @@ -126,13 +126,13 @@ void DFSExplorer::run() int next = state->next_transition(); if (next < 0) { // If there is no more transition in the current state, backtrack. - XBT_DEBUG("There remains %zu actors, but none to interleave (depth %zu).", - mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1); + XBT_DEBUG("There remains %d actors, but none to interleave (depth %zu).", state->get_actor_count(), + stack_.size() + 1); - if (mc_model_checker->get_remote_process().actors().empty()) { + if (state->get_actor_count() == 0) { mc_model_checker->finalize_app(); XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(), - state->num_, stack_.size()); + state->get_num(), stack_.size()); } this->backtrack(); continue; @@ -145,14 +145,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)", state->get_transition()->aid_, - state->get_transition()->to_string().c_str(), stack_.size(), state->num_, state->count_todo()); - - std::string req_str; - if (dot_output != nullptr) - req_str = state->get_transition()->dot_string(); + state->get_transition()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo()); /* Create the new expanded state (copy the state of MCed into our MCer data) */ - auto next_state = std::make_unique(); + auto next_state = std::make_unique(get_session()); on_state_creation_signal(next_state.get()); if (_sg_mc_termination) @@ -160,28 +156,27 @@ void DFSExplorer::run() /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */ if (_sg_mc_max_visited_states > 0) - visited_state_ = visited_states_.addVisitedState(next_state->num_, next_state.get(), true); + visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(), true); /* If this is a new state (or if we don't care about state-equality reduction) */ if (visited_state_ == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ - auto actors = Api::get().get_actors(); - for (auto& remoteActor : actors) { - auto actor = remoteActor.copy.get_buffer(); - if (get_session().actor_is_enabled(actor->get_pid())) { - next_state->mark_todo(actor->get_pid()); + for (auto const& [aid, _] : next_state->get_actors_list()) { + if (next_state->is_actor_enabled(aid)) { + next_state->mark_todo(aid); if (reductionMode_ == ReductionMode::dpor) break; // With DPOR, we take the first enabled transition } } if (dot_output != nullptr) - std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->num_, next_state->num_, req_str.c_str()); + std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), next_state->get_num(), + state->get_transition()->dot_string().c_str()); } else if (dot_output != nullptr) - std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->num_, + std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num, - req_str.c_str()); + state->get_transition()->dot_string().c_str()); stack_.push_back(std::move(next_state)); } @@ -216,32 +211,32 @@ void DFSExplorer::backtrack() break; } else if (prev_state->get_transition()->depends(state->get_transition())) { XBT_VERB("Dependent Transitions:"); - XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->num_); - XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->num_); + XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num()); + XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num()); - if (not prev_state->actor_states_[issuer_id].is_done()) + if (not prev_state->is_done(issuer_id)) prev_state->mark_todo(issuer_id); else XBT_DEBUG("Actor %ld is in done set", issuer_id); break; } else { XBT_VERB("INDEPENDENT Transitions:"); - XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->num_); - XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->num_); + XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num()); + XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num()); } } } if (state->count_todo() && stack_.size() < (std::size_t)_sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ - XBT_DEBUG("Back-tracking to state %ld at depth %zu", state->num_, stack_.size() + 1); + XBT_DEBUG("Back-tracking to state %ld at depth %zu", state->get_num(), stack_.size() + 1); stack_.push_back( std::move(state)); // Put it back on the stack from which it was removed earlier in this while loop this->restore_state(); - XBT_DEBUG("Back-tracking to state %ld at depth %zu done", stack_.back()->num_, stack_.size()); + XBT_DEBUG("Back-tracking to state %ld at depth %zu done", stack_.back()->get_num(), stack_.size()); break; } else { - XBT_DEBUG("Delete state %ld at depth %zu", state->num_, stack_.size() + 1); + XBT_DEBUG("Delete state %ld at depth %zu", state->get_num(), stack_.size() + 1); } } } @@ -250,8 +245,8 @@ void DFSExplorer::restore_state() { /* If asked to rollback on a state that has a snapshot, restore it */ State* last_state = stack_.back().get(); - if (last_state->system_state_) { - Api::get().restore_state(last_state->system_state_); + if (const auto* system_state = last_state->get_system_state()) { + Api::get().restore_state(system_state); on_restore_system_state_signal(last_state); return; } @@ -290,16 +285,14 @@ DFSExplorer::DFSExplorer(Session* session) : Exploration(session) XBT_DEBUG("Starting the DFS exploration"); - auto initial_state = std::make_unique(); + auto initial_state = std::make_unique(get_session()); XBT_DEBUG("**************************************************"); /* Get an enabled actor and insert it in the interleave set of the initial state */ - auto actors = Api::get().get_actors(); - XBT_DEBUG("Initial state. %zu actors to consider", actors.size()); - for (auto& actor : actors) { - aid_t aid = actor.copy.get_buffer()->get_pid(); - if (get_session().actor_is_enabled(aid)) { + XBT_DEBUG("Initial state. %d actors to consider", initial_state->get_actor_count()); + for (auto const& [aid, _] : initial_state->get_actors_list()) { + if (initial_state->is_actor_enabled(aid)) { initial_state->mark_todo(aid); if (reductionMode_ == ReductionMode::dpor) { XBT_DEBUG("Actor %ld is TODO, DPOR is ON so let's go for this one.", aid); @@ -317,5 +310,4 @@ Exploration* create_dfs_exploration(Session* session) return new DFSExplorer(session); } -} // namespace mc -} // namespace simgrid +} // namespace simgrid::mc