xbt_free(prop_ato);
MC_UNSET_RAW_MEM;
return 1;
+ }else{
+ XBT_DEBUG("Different snapshot");
}
+ }else{
+ XBT_DEBUG("Different values of propositional symbols");
}
+ }else{
+ XBT_DEBUG("Different automaton state");
}
}
xbt_free(prop_ato);
MC_UNSET_RAW_MEM;
return 1;
+ }else{
+ XBT_DEBUG("Different snapshot");
}
+ }else{
+ XBT_DEBUG("Different values of propositional symbols");
}
+ }else{
+ XBT_DEBUG("Different automaton state");
}
-
-
+
region_diff = 0;
}
return 1;
+ }else{
+ XBT_DEBUG("Different snapshot");
}
+ }else{
+ XBT_DEBUG("Different values of propositional symbols");
}
+ }else{
+ XBT_DEBUG("Different automaton state");
}
+ }else{
+ XBT_DEBUG("Different value of search_cycle");
}
}
xbt_free(prop_ato);
MC_UNSET_RAW_MEM;
return 1;
+ }else{
+ XBT_DEBUG("Different snapshot");
}
+ }else{
+ XBT_DEBUG("Different values of propositional symbols");
}
+ }else{
+ XBT_DEBUG("Different automaton state");
}
+ }else{
+ XBT_DEBUG("Different value of search_cycle");
}
-
+
region_diff = 0;
}
}
default :
return -1;
+ break;
}
}
int value;
mc_state_t next_graph_state = NULL;
- smx_req_t req = NULL;
+ smx_simcall_t req = NULL;
char *req_str;
xbt_transition_t transition_succ;
MC_state_set_executed_request(current_pair->graph_state, req, value);
/* Answer the request */
- SIMIX_request_pre(req, value);
+ SIMIX_simcall_pre(req, value);
/* Wait for requests (schedules processes) */
MC_wait_for_requests();