+ // Parallell implementation
+ /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
+ if(res != -1){
+ if(!raw_mem_set)
+ MC_SET_STD_HEAP;
+ return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
+ } */
+
+ cursor = min;
+ while (cursor <= max) {
+ pair_test =
+ (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, cursor,
+ mc_visited_pair_t);
+ if (xbt_automaton_state_compare
+ (pair_test->automaton_state, pair->automaton_state) == 0) {
+ if (xbt_automaton_propositional_symbols_compare_value
+ (pair_test->atomic_propositions,
+ pair->atomic_propositions) == 0) {
+ if (snapshot_compare(pair_test, pair) == 0) {
+ XBT_INFO("Pair %d already reached (equal to pair %d) !",
+ pair->num, pair_test->num);
+
+ xbt_fifo_shift(mc_stack);
+ if (dot_output != NULL)
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
+ initial_global_state->prev_pair, pair_test->num,
+ initial_global_state->prev_req);
+
+ if (!raw_mem_set)
+ MC_SET_STD_HEAP;
+
+ return NULL;
+ }
+ }
+ }
+ cursor++;
+ }
+ xbt_dynar_insert_at(acceptance_pairs, min, &pair);
+ } else {
+ pair_test =
+ (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index,
+ mc_visited_pair_t);
+ if (pair_test->nb_processes < pair->nb_processes) {
+ xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
+ } else {
+ if (pair_test->heap_bytes_used < pair->heap_bytes_used)
+ xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
+ else
+ xbt_dynar_insert_at(acceptance_pairs, index, &pair);
+ }
+ }