X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/81615c1df39f604adb86057b601734f198be9b31..7f0516d66943c1fa8f64946cf159eb37bc7ef41f:/src/mc/checker/LivenessChecker.cpp diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index 6456c08f78..c4a214ae0b 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2011-2021. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2011-2022. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -60,7 +60,7 @@ Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) std::shared_ptr> LivenessChecker::get_proposition_values() const { - auto values = api::get().automaton_propositional_symbol_evaluate(); + auto values = api::get().automaton_propositional_symbol_evaluate(); return std::make_shared>(std::move(values)); } @@ -122,27 +122,12 @@ void LivenessChecker::replay() std::shared_ptr state = pair->graph_state; if (pair->exploration_started) { - int req_num = state->transition_.times_considered_; - const s_smx_simcall* saved_req = &state->executed_req_; - - smx_simcall_t req = nullptr; - - /* because we got a copy of the executed request, we have to fetch the - real one, pointed by the request field of the issuer process */ - const smx_actor_t issuer = api::get().simcall_get_issuer(saved_req); - req = &issuer->simcall_; - - /* Debug information */ - XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, api::get().request_to_string(req, req_num).c_str(), - state.get()); - - api::get().execute(state->transition_, req); + state->get_transition()->replay(); + XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_cstring(), state.get()); } /* Update statistics */ visited_pairs_count_++; - api::get().mc_inc_executed_trans(); - depth++; } XBT_DEBUG("**** End Replay ****"); @@ -202,7 +187,7 @@ RecordTrace LivenessChecker::get_record_trace() // override { RecordTrace res; for (std::shared_ptr const& pair : exploration_stack_) - res.push_back(pair->graph_state->get_transition()); + res.push_back(*pair->graph_state->get_transition()); return res; } @@ -210,7 +195,7 @@ void LivenessChecker::log_state() // override { XBT_INFO("Expanded pairs = %lu", expanded_pairs_count_); XBT_INFO("Visited pairs = %lu", visited_pairs_count_); - XBT_INFO("Executed transitions = %lu", api::get().mc_get_executed_trans()); + XBT_INFO("Executed transitions = %lu", Transition::get_executed_transitions()); } void LivenessChecker::show_acceptance_cycle(std::size_t depth) @@ -230,10 +215,9 @@ std::vector LivenessChecker::get_textual_trace() // override { std::vector trace; for (std::shared_ptr const& pair : exploration_stack_) { - int req_num = pair->graph_state->transition_.times_considered_; smx_simcall_t req = &pair->graph_state->executed_req_; if (req->call_ != simix::Simcall::NONE) - trace.push_back(api::get().request_to_string(req, req_num)); + trace.push_back(pair->graph_state->get_transition()->to_string()); } return trace; } @@ -242,10 +226,9 @@ std::shared_ptr LivenessChecker::create_pair(const Pair* current_pair, xbt std::shared_ptr> propositions) { ++expanded_pairs_count_; - ++expanded_states_count_; auto next_pair = std::make_shared(expanded_pairs_count_); next_pair->automaton_state = state; - next_pair->graph_state = std::make_shared(expanded_states_count_); + next_pair->graph_state = std::make_shared(); next_pair->atomic_propositions = std::move(propositions); if (current_pair) next_pair->depth = current_pair->depth + 1; @@ -255,7 +238,7 @@ std::shared_ptr LivenessChecker::create_pair(const Pair* current_pair, xbt for (auto& act : api::get().get_actors()) { auto actor = act.copy.get_buffer(); if (get_session().actor_is_enabled(actor->get_pid())) - next_pair->graph_state->mark_todo(actor); + next_pair->graph_state->mark_todo(actor->get_pid()); } next_pair->requests = next_pair->graph_state->count_todo(); @@ -352,8 +335,13 @@ void LivenessChecker::run() } } - smx_simcall_t req = api::get().mc_state_choose_request(current_pair->graph_state.get()); - int req_num = current_pair->graph_state->transition_.times_considered_; + int next = current_pair->graph_state->next_transition(); + + current_pair->graph_state->execute_next(next); + + aid_t aid = current_pair->graph_state->get_transition()->aid_; + int req_num = current_pair->graph_state->get_transition()->times_considered_; + XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_cstring()); if (dot_output != nullptr) { if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) { @@ -362,26 +350,15 @@ void LivenessChecker::run() this->previous_request_.clear(); } this->previous_pair_ = current_pair->num; - this->previous_request_ = api::get().request_get_dot_output(req, req_num); + this->previous_request_ = api::get().request_get_dot_output(aid, req_num); if (current_pair->search_cycle) fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num); fflush(dot_output); } - XBT_DEBUG("Execute: %s", api::get().request_to_string(req, req_num).c_str()); - - /* Update stats */ - api::get().mc_inc_executed_trans(); - if (not current_pair->exploration_started) visited_pairs_count_++; - /* Answer the request */ - api::get().handle_simcall(current_pair->graph_state->transition_); - - /* Wait for requests (schedules processes) */ - api::get().mc_wait_for_requests(); - current_pair->requests--; current_pair->exploration_started = true; @@ -392,7 +369,7 @@ void LivenessChecker::run() // (application_state, automaton_state) pair to the exploration stack: for (int i = api::get().get_dynar_length(current_pair->automaton_state->out) - 1; i >= 0; i--) { auto transition_succ_label = api::get().get_automaton_transition_label(current_pair->automaton_state->out, i); - auto transition_succ_dst = api::get().get_automaton_transition_dst(current_pair->automaton_state->out, i); + auto transition_succ_dst = api::get().get_automaton_transition_dst(current_pair->automaton_state->out, i); if (evaluate_label(transition_succ_label, *prop_values)) exploration_stack_.push_back(this->create_pair(current_pair.get(), transition_succ_dst, prop_values)); }