- mc_pair_reached_t new_pair = NULL;
- new_pair = xbt_new0(s_mc_pair_reached_t, 1);
- new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
- new_pair->automaton_state = st;
- new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
- new_pair->system_state = MC_take_snapshot_liveness();
-
- /* Get values of propositional symbols */
- int res;
- int_f_void_t f;
- unsigned int cursor = 0;
- xbt_propositional_symbol_t ps = NULL;
- xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
- f = (int_f_void_t)ps->function;
- res = (*f)();
- xbt_dynar_push_as(new_pair->prop_ato, int, res);
- }
-
- MC_UNSET_RAW_MEM;
-
- if(xbt_dynar_is_empty(reached_pairs) || !compare){
-
- MC_SET_RAW_MEM;
- /* New pair reached */
- xbt_dynar_push(reached_pairs, &new_pair);
- MC_UNSET_RAW_MEM;
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
-
- return 0;
-
- }else{
-
- MC_SET_RAW_MEM;
-
- cursor = 0;
- mc_pair_reached_t pair_test = NULL;
-
- xbt_dynar_foreach(reached_pairs, cursor, pair_test){
- XBT_INFO("Pair reached #%d", pair_test->nb);
- if(automaton_state_compare(pair_test->automaton_state, st) == 0){
- if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
- if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
-
- if(raw_mem_set)
- MC_SET_RAW_MEM;
- else
- MC_UNSET_RAW_MEM;
-
- return 1;
- }
- }else{
- XBT_INFO("Different values of propositional symbols");
+ MC_SET_MC_HEAP;
+
+ mc_visited_pair_t pair = NULL;
+ pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
+ pair->acceptance_pair = 1;
+
+ if (xbt_dynar_is_empty(acceptance_pairs)) {
+
+ xbt_dynar_push(acceptance_pairs, &pair);
+
+ } else {
+
+ int min = -1, max = -1, index;
+ //int res;
+ mc_visited_pair_t pair_test;
+ int cursor;
+
+ index = get_search_interval(acceptance_pairs, pair, &min, &max);
+
+ if (min != -1 && max != -1) { // Acceptance pair with same number of processes and same heap bytes used exists
+
+ // 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;
+ }
+ }