- 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();
- }
-}
-
-static void MC_assert_pair(int prop){
- if (MC_is_active() && !prop) {
- XBT_INFO("**************************");
- XBT_INFO("*** PROPERTY NOT VALID ***");
- XBT_INFO("**************************");
- //XBT_INFO("Counter-example execution trace:");
- MC_show_stack_liveness(mc_stack_liveness);
- //MC_dump_snapshot_stack(mc_snapshot_stack);
- MC_print_statistics(mc_stats);
- xbt_abort();
- }
-}
-
-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;
-
-}
-
-/************ MC_ignore ***********/
-
-void heap_ignore_region_free(mc_heap_ignore_region_t r){
- xbt_free(r);
-}
-
-void heap_ignore_region_free_voidp(void *r){
- heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
-}
-
-void MC_ignore_heap(void *address, size_t size){
-
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);