#include <cstring>
+#include <algorithm>
+#include <memory>
+
#include <unistd.h>
#include <sys/wait.h>
#include <xbt/automaton.h>
#include <xbt/dynar.h>
+#include <xbt/dynar.hpp>
#include <xbt/fifo.h>
#include <xbt/log.h>
#include <xbt/sysdep.h>
static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* pair)
{
- simgrid::mc::VisitedPair* new_pair = new VisitedPair(
- pair->num, pair->automaton_state, pair->atomic_propositions.get(),
- pair->graph_state);
+ auto acceptance_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(::acceptance_pairs);
+ auto new_pair =
+ std::unique_ptr<simgrid::mc::VisitedPair>(new VisitedPair(
+ pair->num, pair->automaton_state, pair->atomic_propositions.get(),
+ pair->graph_state));
new_pair->acceptance_pair = 1;
- if (xbt_dynar_is_empty(acceptance_pairs))
- xbt_dynar_push(acceptance_pairs, &new_pair);
- else {
-
- int min = -1, max = -1, index;
- //int res;
- simgrid::mc::VisitedPair* pair_test;
- int cursor;
-
- index = simgrid::mc::get_search_interval(
- (simgrid::mc::VisitedPair**) xbt_dynar_get_ptr(acceptance_pairs, 0),
- xbt_dynar_length(acceptance_pairs),
- new_pair, &min, &max);
-
- if (min != -1 && max != -1) { // Acceptance pair with same number of processes and same heap bytes used exists
-
- cursor = min;
- if(pair->search_cycle == 1){
- while (cursor <= max) {
- pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(acceptance_pairs, cursor, simgrid::mc::VisitedPair*);
- if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
- if (xbt_automaton_propositional_symbols_compare_value(
- pair_test->atomic_propositions.get(),
- new_pair->atomic_propositions.get()) == 0) {
- if (snapshot_compare(pair_test, new_pair) == 0) {
- XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
- xbt_fifo_shift(mc_stack);
- if (dot_output != nullptr)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
- return nullptr;
- }
- }
+ auto res = std::equal_range(acceptance_pairs.begin(), acceptance_pairs.end(),
+ new_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+
+ if (pair->search_cycle == 1)
+ for (auto i = res.first; i != res.second; ++i) {
+ simgrid::mc::VisitedPair* pair_test = *i;
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
+ if (xbt_automaton_propositional_symbols_compare_value(
+ pair_test->atomic_propositions.get(),
+ new_pair->atomic_propositions.get()) == 0) {
+ if (snapshot_compare(pair_test, new_pair.get()) == 0) {
+ XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
+ xbt_fifo_shift(mc_stack);
+ if (dot_output != nullptr)
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
+ return nullptr;
}
- cursor++;
}
}
- xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
- } else {
- pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(acceptance_pairs, index, simgrid::mc::VisitedPair*);
- if (pair_test->nb_processes < new_pair->nb_processes)
- xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
- else if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
- xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
- else
- xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
}
- }
- return new_pair;
+
+ auto new_raw_pair = new_pair.release();
+ xbt_dynar_insert_at(
+ ::acceptance_pairs, res.first - acceptance_pairs.begin(), &new_raw_pair);
+ return new_raw_pair;
}
static void remove_acceptance_pair(int pair_num)
else
new_visited_pair = visited_pair;
- if (xbt_dynar_is_empty(visited_pairs)) {
- xbt_dynar_push(visited_pairs, &new_visited_pair);
- return -1;
- }
-
- int min = -1, max = -1, index;
- //int res;
- simgrid::mc::VisitedPair* pair_test;
- int cursor;
-
- index = get_search_interval(
- (simgrid::mc::VisitedPair**) xbt_dynar_get_ptr(visited_pairs, 0),
- xbt_dynar_length(visited_pairs), new_visited_pair, &min, &max);
-
- if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
- cursor = min;
- while (cursor <= max) {
- pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
- if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
- if (xbt_automaton_propositional_symbols_compare_value(
- pair_test->atomic_propositions.get(),
- new_visited_pair->atomic_propositions.get()) == 0) {
- if (snapshot_compare(pair_test, new_visited_pair) == 0) {
- if (pair_test->other_num == -1)
- new_visited_pair->other_num = pair_test->num;
- else
- new_visited_pair->other_num = pair_test->other_num;
- if (dot_output == nullptr)
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
- else
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
- xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
- xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
- pair_test->visited_removed = 1;
- if (!pair_test->acceptance_pair
- || pair_test->acceptance_removed == 1)
- delete pair_test;
- return new_visited_pair->other_num;
- }
- }
+ auto visited_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(simgrid::mc::visited_pairs);
+
+ auto range = std::equal_range(visited_pairs.begin(), visited_pairs.end(),
+ new_visited_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+
+ for (auto i = range.first; i != range.second; ++i) {
+ simgrid::mc::VisitedPair* pair_test = *i;
+ std::size_t cursor = i - visited_pairs.begin();
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
+ if (xbt_automaton_propositional_symbols_compare_value(
+ pair_test->atomic_propositions.get(),
+ new_visited_pair->atomic_propositions.get()) == 0) {
+ if (snapshot_compare(pair_test, new_visited_pair) == 0) {
+ if (pair_test->other_num == -1)
+ new_visited_pair->other_num = pair_test->num;
+ else
+ new_visited_pair->other_num = pair_test->other_num;
+ if (dot_output == nullptr)
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
+ else
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
+ xbt_dynar_remove_at(simgrid::mc::visited_pairs, cursor, &pair_test);
+ xbt_dynar_insert_at(simgrid::mc::visited_pairs, cursor, &new_visited_pair);
+ pair_test->visited_removed = 1;
+ if (!pair_test->acceptance_pair
+ || pair_test->acceptance_removed == 1)
+ delete pair_test;
+ return new_visited_pair->other_num;
}
- cursor++;
}
- xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
- } else {
- pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*);
- if (pair_test->nb_processes < new_visited_pair->nb_processes)
- xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
- else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
- xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
- else
- xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
}
+ }
- if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
- int min2 = mc_stats->expanded_pairs;
- unsigned int cursor2 = 0;
- unsigned int index2 = 0;
- xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
- if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
- && pair_test->num < min2) {
- index2 = cursor2;
- min2 = pair_test->num;
- }
+ xbt_dynar_insert_at(simgrid::mc::visited_pairs, range.first - visited_pairs.begin(), &new_visited_pair);
+
+ if ((ssize_t) visited_pairs.size() > _sg_mc_visited) {
+ int min2 = mc_stats->expanded_pairs;
+ unsigned int index2 = 0;
+ for (std::size_t i = 0; i != (std::size_t) visited_pairs.size(); ++i) {
+ simgrid::mc::VisitedPair* pair_test = visited_pairs[i];
+ if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
+ && pair_test->num < min2) {
+ index2 = i;
+ min2 = pair_test->num;
}
- xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
- pair_test->visited_removed = 1;
- if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
- delete pair_test;
}
+ simgrid::mc::VisitedPair* pair_test = nullptr;
+ xbt_dynar_remove_at(simgrid::mc::visited_pairs, index2, &pair_test);
+ pair_test->visited_removed = 1;
+ if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
+ delete pair_test;
+ }
+
return -1;
}
