+
+
+void MC_exit(void)
+{
+ xbt_free(mc_time);
+ MC_memory_exit();
+ //xbt_abort();
+}
+
+int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
+
+ return simcall->mc_value;
+}
+
+
+int MC_random(int min, int max)
+{
+ /*FIXME: return mc_current_state->executed_transition->random.value;*/
+ return simcall_mc_random(min, max);
+}
+
+/**
+ * \brief Schedules all the process that are ready to run
+ */
+void MC_wait_for_requests(void)
+{
+ smx_process_t process;
+ smx_simcall_t req;
+ unsigned int iter;
+
+ while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
+ SIMIX_process_runall();
+ xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
+ req = &process->simcall;
+ if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
+ SIMIX_simcall_pre(req, 0);
+ }
+ }
+}
+
+int MC_deadlock_check()
+{
+ int deadlock = FALSE;
+ smx_process_t process;
+ if(xbt_swag_size(simix_global->process_list)){
+ deadlock = TRUE;
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(process->simcall.call != SIMCALL_NONE
+ && MC_request_is_enabled(&process->simcall)){
+ deadlock = FALSE;
+ break;
+ }
+ }
+ }
+ return deadlock;
+}
+
+/**
+ * \brief Re-executes from the state at position start all the transitions indicated by
+ * a given model-checker stack.
+ * \param stack The stack with the transitions to execute.
+ * \param start Start index to begin the re-execution.
+ */
+void MC_replay(xbt_fifo_t stack, int start)
+{
+ int raw_mem = (mmalloc_get_current_heap() == raw_heap);
+
+ int value, i = 1, count = 1;
+ char *req_str;
+ smx_simcall_t req = NULL, saved_req = NULL;
+ xbt_fifo_item_t item, start_item;
+ mc_state_t state;
+ smx_process_t process = NULL;
+
+ XBT_DEBUG("**** Begin Replay ****");
+
+ if(start == -1){
+ /* Restore the initial state */
+ MC_restore_snapshot(initial_state_safety->snapshot);
+ /* At the moment of taking the snapshot the raw heap was set, so restoring
+ * it will set it back again, we have to unset it to continue */
+ MC_UNSET_RAW_MEM;
+ }
+
+ start_item = xbt_fifo_get_last_item(stack);
+ if(start != -1){
+ while (i != start){
+ start_item = xbt_fifo_get_prev_item(start_item);
+ i++;
+ }
+ }
+
+ MC_SET_RAW_MEM;
+ xbt_dict_reset(first_enabled_state);
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ char *key = bprintf("%lu", process->pid);
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ xbt_free(key);
+ }
+ }
+ MC_UNSET_RAW_MEM;
+
+
+ /* Traverse the stack from the state at position start and re-execute the transitions */
+ for (item = start_item;
+ item != xbt_fifo_get_first_item(stack);
+ item = xbt_fifo_get_prev_item(item)) {
+
+ state = (mc_state_t) xbt_fifo_get_item_content(item);
+ saved_req = MC_state_get_executed_request(state, &value);
+
+ MC_SET_RAW_MEM;
+ char *key = bprintf("%lu", saved_req->issuer->pid);
+ xbt_dict_remove(first_enabled_state, key);
+ xbt_free(key);
+ MC_UNSET_RAW_MEM;
+
+ if(saved_req){
+ /* because we got a copy of the executed request, we have to fetch the
+ real one, pointed by the request field of the issuer process */
+ req = &saved_req->issuer->simcall;
+
+ /* Debug information */
+ if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+ req_str = MC_request_to_string(req, value);
+ XBT_DEBUG("Replay: %s (%p)", req_str, state);
+ xbt_free(req_str);
+ }
+ }
+
+ SIMIX_simcall_pre(req, value);
+ MC_wait_for_requests();
+
+ count++;
+
+ MC_SET_RAW_MEM;
+ /* Insert in dict all enabled processes */
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
+ char *key = bprintf("%lu", process->pid);
+ if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ }
+ xbt_free(key);
+ }
+ }
+ MC_UNSET_RAW_MEM;
+
+ /* Update statistics */
+ mc_stats->visited_states++;
+ mc_stats->executed_transitions++;
+
+ }
+
+ XBT_DEBUG("**** End Replay ****");
+
+ if(raw_mem)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+
+
+}
+
+void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
+{
+
+ initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ int value;
+ char *req_str;
+ smx_simcall_t req = NULL, saved_req = NULL;
+ xbt_fifo_item_t item;
+ mc_state_t state;
+ mc_pair_t pair;
+ int depth = 1;
+
+ XBT_DEBUG("**** Begin Replay ****");
+
+ /* Restore the initial state */
+ MC_restore_snapshot(initial_state_liveness->snapshot);
+
+ /* At the moment of taking the snapshot the raw heap was set, so restoring
+ * it will set it back again, we have to unset it to continue */
+ if(!initial_state_liveness->raw_mem_set)
+ MC_UNSET_RAW_MEM;
+
+ if(all_stack){
+
+ item = xbt_fifo_get_last_item(stack);
+
+ while(depth <= xbt_fifo_size(stack)){
+
+ pair = (mc_pair_t) xbt_fifo_get_item_content(item);
+ state = (mc_state_t) pair->graph_state;
+
+ if(pair->requests > 0){
+
+ saved_req = MC_state_get_executed_request(state, &value);
+ //XBT_DEBUG("SavedReq->call %u", saved_req->call);
+
+ if(saved_req != NULL){
+ /* because we got a copy of the executed request, we have to fetch the
+ real one, pointed by the request field of the issuer process */
+ req = &saved_req->issuer->simcall;
+ //XBT_DEBUG("Req->call %u", req->call);
+
+ /* Debug information */
+ if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+ req_str = MC_request_to_string(req, value);
+ XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+ xbt_free(req_str);
+ }
+
+ }
+
+ SIMIX_simcall_pre(req, value);
+ MC_wait_for_requests();
+ }
+
+ depth++;
+
+ /* Update statistics */
+ mc_stats->visited_pairs++;
+ mc_stats->executed_transitions++;
+
+ item = xbt_fifo_get_prev_item(item);
+ }
+
+ }else{
+
+ /* Traverse the stack from the initial state and re-execute the transitions */
+ for (item = xbt_fifo_get_last_item(stack);
+ item != xbt_fifo_get_first_item(stack);
+ item = xbt_fifo_get_prev_item(item)) {
+
+ pair = (mc_pair_t) xbt_fifo_get_item_content(item);
+ state = (mc_state_t) pair->graph_state;
+
+ if(pair->requests > 0){
+
+ saved_req = MC_state_get_executed_request(state, &value);
+ //XBT_DEBUG("SavedReq->call %u", saved_req->call);
+
+ if(saved_req != NULL){
+ /* because we got a copy of the executed request, we have to fetch the
+ real one, pointed by the request field of the issuer process */
+ req = &saved_req->issuer->simcall;
+ //XBT_DEBUG("Req->call %u", req->call);
+
+ /* Debug information */
+ if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+ req_str = MC_request_to_string(req, value);
+ XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+ xbt_free(req_str);
+ }
+
+ }
+
+ SIMIX_simcall_pre(req, value);
+ MC_wait_for_requests();
+ }
+
+ depth++;
+
+ /* Update statistics */
+ mc_stats->visited_pairs++;
+ mc_stats->executed_transitions++;
+ }
+ }
+
+ XBT_DEBUG("**** End Replay ****");
+
+ if(initial_state_liveness->raw_mem_set)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+
+}
+
+/**
+ * \brief Dumps the contents of a model-checker's stack and shows the actual
+ * execution trace
+ * \param stack The stack to dump
+ */
+void MC_dump_stack_safety(xbt_fifo_t stack)
+{
+
+ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_show_stack_safety(stack);
+
+ if(!_sg_mc_checkpoint){
+
+ mc_state_t state;
+
+ MC_SET_RAW_MEM;
+ while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
+ MC_state_delete(state);
+ MC_UNSET_RAW_MEM;
+
+ }
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+
+}
+
+
+void MC_show_stack_safety(xbt_fifo_t stack)
+{
+
+ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
+
+ int value;
+ mc_state_t state;
+ xbt_fifo_item_t item;
+ smx_simcall_t req;
+ char *req_str = NULL;
+
+ for (item = xbt_fifo_get_last_item(stack);
+ (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
+ : (NULL)); item = xbt_fifo_get_prev_item(item)) {
+ req = MC_state_get_executed_request(state, &value);
+ if(req){
+ req_str = MC_request_to_string(req, value);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
+ }
+ }
+
+ if(!raw_mem_set)
+ MC_UNSET_RAW_MEM;
+}
+
+void MC_show_deadlock(smx_simcall_t req)
+{
+ /*char *req_str = NULL;*/
+ XBT_INFO("**************************");
+ XBT_INFO("*** DEAD-LOCK DETECTED ***");
+ XBT_INFO("**************************");
+ XBT_INFO("Locked request:");
+ /*req_str = MC_request_to_string(req);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);*/
+ XBT_INFO("Counter-example execution trace:");
+ MC_dump_stack_safety(mc_stack_safety);
+ MC_print_statistics(mc_stats);
+}
+
+
+void MC_show_stack_liveness(xbt_fifo_t stack){
+ int value;
+ mc_pair_t pair;
+ xbt_fifo_item_t item;
+ smx_simcall_t req;
+ char *req_str = NULL;
+
+ for (item = xbt_fifo_get_last_item(stack);
+ (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
+ : (NULL)); item = xbt_fifo_get_prev_item(item)) {
+ req = MC_state_get_executed_request(pair->graph_state, &value);
+ if(req){
+ if(pair->requests>0){
+ req_str = MC_request_to_string(req, value);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
+ }else{
+ XBT_INFO("End of system requests but evolution in Büchi automaton");
+ }
+ }
+ }
+}
+
+void MC_dump_stack_liveness(xbt_fifo_t stack){
+
+ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ mc_pair_t pair;
+
+ MC_SET_RAW_MEM;
+ while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
+ MC_pair_delete(pair);
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+}
+
+
+void MC_print_statistics(mc_stats_t stats)
+{
+ if(stats->expanded_pairs == 0){
+ XBT_INFO("Expanded states = %lu", stats->expanded_states);
+ XBT_INFO("Visited states = %lu", stats->visited_states);
+ }else{
+ XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
+ XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
+ }
+ XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
+ MC_SET_RAW_MEM;
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
+ fprintf(dot_output, "}\n");
+ fclose(dot_output);
+ }
+ MC_UNSET_RAW_MEM;
+}
+
+void MC_assert(int prop)
+{
+ if (MC_is_active() && !prop){
+ XBT_INFO("**************************");
+ XBT_INFO("*** PROPERTY NOT VALID ***");
+ XBT_INFO("**************************");
+ XBT_INFO("Counter-example execution trace:");
+ MC_dump_stack_safety(mc_stack_safety);
+ MC_print_statistics(mc_stats);
+ xbt_abort();
+ }
+}
+
+void MC_cut(void){
+ user_max_depth_reached = 1;
+}
+
+void MC_process_clock_add(smx_process_t process, double amount)
+{
+ mc_time[process->pid] += amount;
+}
+
+double MC_process_clock_get(smx_process_t process)
+{
+ if(mc_time){
+ if(process != NULL)
+ return mc_time[process->pid];
+ else
+ return -1;
+ }else{
+ return 0;
+ }
+}
+
+void MC_automaton_load(const char *file){
+
+ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
+
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+
+ xbt_automaton_load(_mc_property_automaton,file);
+
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+}
+
+void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
+
+ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
+
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+
+ xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
+
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+}
+
+
+