X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2ab3abe53dde0026da7545fb7a80f29caf22a39b..7619465098bac161b3cfbf0f220ee29a8cb45720:/src/mc/mc_visited.cpp diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp index d26d7aef7e..d6de75ac4d 100644 --- a/src/mc/mc_visited.cpp +++ b/src/mc/mc_visited.cpp @@ -10,7 +10,6 @@ #include #include -#include #include #include #include @@ -19,7 +18,6 @@ #include "src/mc/mc_comm_pattern.h" #include "src/mc/mc_safety.h" -#include "src/mc/LivenessChecker.hpp" #include "src/mc/mc_private.h" #include "src/mc/Process.hpp" #include "src/mc/mc_smx.h" @@ -32,18 +30,6 @@ namespace mc { std::vector> visited_states; -static int is_exploration_stack_state(simgrid::mc::VisitedState* state){ - xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack); - while (item) { - if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){ - ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0; - return 1; - } - item = xbt_fifo_get_next_item(item); - } - return 0; -} - /** * \brief Save the current state * \return Snapshot of the current state. @@ -65,55 +51,6 @@ VisitedState::VisitedState() VisitedState::~VisitedState() { - if(!is_exploration_stack_state(this)) - delete this->system_state; -} - -VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state) -{ - simgrid::mc::Process* process = &(mc_model_checker->process()); - - this->graph_state = graph_state; - if(this->graph_state->system_state == nullptr) - this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num); - this->heap_bytes_used = mmalloc_get_bytes_used_remote( - process->get_heap()->heaplimit, - process->get_malloc_info()); - - this->nb_processes = - mc_model_checker->process().simix_processes().size(); - - this->automaton_state = automaton_state; - this->num = pair_num; - this->other_num = -1; - this->acceptance_removed = 0; - this->visited_removed = 0; - this->acceptance_pair = 0; - this->atomic_propositions = simgrid::xbt::unique_ptr( - xbt_dynar_new(sizeof(int), nullptr)); - - unsigned int cursor = 0; - int value; - xbt_dynar_foreach(atomic_propositions, cursor, value) - xbt_dynar_push_as(this->atomic_propositions.get(), int, value); -} - -static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair){ - xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack); - while (item) { - if (((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->num == pair->num){ - ((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->visited_pair_removed = 1; - return 1; - } - item = xbt_fifo_get_next_item(item); - } - return 0; -} - -VisitedPair::~VisitedPair() -{ - if( !is_exploration_stack_pair(this)) - MC_state_delete(this->graph_state, 1); } static void prune_visited_states() @@ -131,56 +68,62 @@ static void prune_visited_states() } } +static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2) +{ + simgrid::mc::Snapshot* s1 = state1->system_state.get(); + simgrid::mc::Snapshot* s2 = state2->system_state.get(); + int num1 = state1->num; + int num2 = state2->num; + return snapshot_compare(num1, s1, num2, s2); +} + /** * \brief Checks whether a given state has already been visited by the algorithm. */ -std::unique_ptr is_visited_state(mc_state_t graph_state, bool compare_snpashots) +std::unique_ptr is_visited_state(simgrid::mc::State* graph_state, bool compare_snpashots) { - - std::unique_ptr new_state = std::unique_ptr(new VisitedState()); graph_state->system_state = new_state->system_state; graph_state->in_visited_states = 1; - XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num); + XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", + new_state->system_state.get(), new_state->num, graph_state->num); auto range = std::equal_range(visited_states.begin(), visited_states.end(), new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap()); - if (compare_snpashots) { - - for (auto i = range.first; i != range.second; ++i) { - auto& visited_state = *i; - if (snapshot_compare(visited_state.get(), new_state.get()) == 0) { - // The state has been visited: - - std::unique_ptr old_state = - std::move(visited_state); - - if (old_state->other_num == -1) - new_state->other_num = old_state->num; - else - new_state->other_num = old_state->other_num; - - if (dot_output == nullptr) - XBT_DEBUG("State %d already visited ! (equal to state %d)", - new_state->num, old_state->num); - else - XBT_DEBUG( - "State %d already visited ! (equal to state %d (state %d in dot_output))", - new_state->num, old_state->num, new_state->other_num); - - /* Replace the old state with the new one (with a bigger num) - (when the max number of visited states is reached, the oldest - one is removed according to its number (= with the min number) */ - XBT_DEBUG("Replace visited state %d with the new visited state %d", - old_state->num, new_state->num); - - visited_state = std::move(new_state); - return std::move(old_state); - } - } + if (compare_snpashots) + for (auto i = range.first; i != range.second; ++i) { + auto& visited_state = *i; + if (snapshot_compare(visited_state.get(), new_state.get()) == 0) { + // The state has been visited: + + std::unique_ptr old_state = + std::move(visited_state); + + if (old_state->other_num == -1) + new_state->other_num = old_state->num; + else + new_state->other_num = old_state->other_num; + + if (dot_output == nullptr) + XBT_DEBUG("State %d already visited ! (equal to state %d)", + new_state->num, old_state->num); + else + XBT_DEBUG( + "State %d already visited ! (equal to state %d (state %d in dot_output))", + new_state->num, old_state->num, new_state->other_num); + + /* Replace the old state with the new one (with a bigger num) + (when the max number of visited states is reached, the oldest + one is removed according to its number (= with the min number) */ + XBT_DEBUG("Replace visited state %d with the new visited state %d", + old_state->num, new_state->num); + + visited_state = std::move(new_state); + return std::move(old_state); } + } XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size()); visited_states.insert(range.first, std::move(new_state));