1 /* Copyright (c) 2008-2013. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
7 #include "mc_private.h"
9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
10 "Logging specific to MC DPOR exploration");
12 /********** Global variables **********/
14 xbt_dynar_t visited_states;
15 xbt_dict_t first_enabled_state;
16 xbt_dynar_t initial_communications_pattern;
17 xbt_dynar_t communications_pattern;
20 /********** Static functions ***********/
22 static void comm_pattern_free(mc_comm_pattern_t p){
29 static void comm_pattern_free_voidp( void *p){
30 comm_pattern_free((mc_comm_pattern_t) * (void **)p);
33 static mc_comm_pattern_t get_comm_pattern_from_idx(xbt_dynar_t pattern, unsigned int *idx, e_smx_comm_type_t type, unsigned long proc){
34 mc_comm_pattern_t current_comm;
35 while(*idx < xbt_dynar_length(pattern)){
36 current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t);
37 if(current_comm->type == type && type == SIMIX_COMM_SEND){
38 if(current_comm->src_proc == proc)
40 }else if(current_comm->type == type && type == SIMIX_COMM_RECEIVE){
41 if(current_comm->dst_proc == proc)
49 static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2){
50 if(strcmp(comm1->rdv, comm2->rdv) != 0)
52 if(comm1->src_proc != comm2->src_proc)
54 if(comm1->dst_proc != comm2->dst_proc)
56 if(comm1->data_size != comm2->data_size)
58 if(memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
63 static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){
64 unsigned int cursor = 0, send_index = 0, recv_index = 0;
65 mc_comm_pattern_t comm1, comm2;
66 int comm_comparison = 0;
67 int current_process = 0;
68 while(current_process < simix_process_maxpid){
69 while(cursor < xbt_dynar_length(initial_pattern)){
70 comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(initial_pattern, cursor, mc_comm_pattern_t);
71 if(comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process){
72 comm2 = get_comm_pattern_from_idx(pattern, &send_index, comm1->type, current_process);
73 comm_comparison = compare_comm_pattern(comm1, comm2);
74 if(comm_comparison == 1){
75 initial_state_safety->send_deterministic = 0;
76 initial_state_safety->comm_deterministic = 0;
80 }else if(comm1->type == SIMIX_COMM_RECEIVE && comm1->dst_proc == current_process){
81 comm2 = get_comm_pattern_from_idx(pattern, &recv_index, comm1->type, current_process);
82 comm_comparison = compare_comm_pattern(comm1, comm2);
83 if(comm_comparison == 1){
84 initial_state_safety->comm_deterministic = 0;
95 // XBT_DEBUG("Communication-deterministic : %d, Send-deterministic : %d", initial_state_safety->comm_deterministic, initial_state_safety->send_deterministic);
98 static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
99 mc_comm_pattern_t current_pattern;
100 unsigned int cursor = 0;
101 xbt_dynar_foreach(list, cursor, current_pattern){
102 if(current_pattern->comm == pattern->comm){
103 if(!current_pattern->completed){
104 current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
105 current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
106 current_pattern->data_size = pattern->comm->comm.src_buff_size;
107 current_pattern->data = xbt_malloc0(current_pattern->data_size);
108 current_pattern->matched_comm = pattern->num;
109 memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size);
110 current_pattern->completed = 1;
111 return current_pattern->num;
118 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
119 mc_comm_pattern_t pattern = NULL;
120 pattern = xbt_new0(s_mc_comm_pattern_t, 1);
121 pattern->num = ++nb_comm_pattern;
122 pattern->completed = 0;
123 if(call == 1){ // ISEND
124 pattern->comm = simcall_comm_isend__get__result(request);
125 pattern->type = SIMIX_COMM_SEND;
126 if(pattern->comm->comm.dst_proc != NULL){
128 pattern->matched_comm = complete_comm_pattern(list, pattern);
129 pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
130 pattern->completed = 1;
132 pattern->src_proc = pattern->comm->comm.src_proc->pid;
133 pattern->data_size = pattern->comm->comm.src_buff_size;
134 pattern->data=xbt_malloc0(pattern->data_size);
135 memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
137 pattern->comm = simcall_comm_irecv__get__result(request);
138 pattern->type = SIMIX_COMM_RECEIVE;
139 if(pattern->comm->comm.src_proc != NULL){
140 pattern->matched_comm = complete_comm_pattern(list, pattern);
141 pattern->src_proc = pattern->comm->comm.src_proc->pid;
142 pattern->completed = 1;
143 pattern->data_size = pattern->comm->comm.src_buff_size;
144 pattern->data=xbt_malloc0(pattern->data_size);
145 memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
147 pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
149 if(pattern->comm->comm.rdv != NULL)
150 pattern->rdv = strdup(pattern->comm->comm.rdv->name);
152 pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
153 xbt_dynar_push(list, &pattern);
156 static void print_communications_pattern(xbt_dynar_t comms_pattern){
157 unsigned int cursor = 0;
158 mc_comm_pattern_t current_comm;
159 xbt_dynar_foreach(comms_pattern, cursor, current_comm){
160 // fprintf(stderr, "%s (%d - comm %p, src : %lu, dst %lu, rdv name %s, data %p, matched with %d)\n", current_comm->type == SIMIX_COMM_SEND ? "iSend" : "iRecv", current_comm->num, current_comm->comm, current_comm->src_proc, current_comm->dst_proc, current_comm->rdv, current_comm->data, current_comm->matched_comm);
164 static void visited_state_free(mc_visited_state_t state){
166 MC_free_snapshot(state->system_state);
171 static void visited_state_free_voidp(void *s){
172 visited_state_free((mc_visited_state_t) * (void **) s);
175 /** \brief Save the current state
177 * \return Snapshot of the current state.
179 static mc_visited_state_t visited_state_new(){
181 mc_visited_state_t new_state = NULL;
182 new_state = xbt_new0(s_mc_visited_state_t, 1);
183 new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
184 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
185 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
186 new_state->num = mc_stats->expanded_states;
187 new_state->other_num = -1;
193 /** \brief Find a suitable subrange of candidate duplicates for a given state
195 * \param all_ pairs dynamic array of states with candidate duplicates of the current state;
196 * \param pair current state;
197 * \param min (output) index of the beginning of the the subrange
198 * \param max (output) index of the enf of the subrange
200 * Given a suitably ordered array of state, this function extracts a subrange
201 * (with index *min <= i <= *max) with candidate duplicates of the given state.
202 * This function uses only fast discriminating criterions and does not use the
203 * full state comparison algorithms.
205 * The states in all_pairs MUST be ordered using a (given) weak order
206 * (based on nb_processes and heap_bytes_used).
207 * The subrange is the subrange of "equivalence" of the given state.
209 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
211 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
215 int cursor = 0, previous_cursor, next_cursor;
216 mc_visited_state_t state_test;
218 int end = xbt_dynar_length(all_states) - 1;
221 cursor = (start + end) / 2;
222 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
223 if(state_test->nb_processes < state->nb_processes){
225 }else if(state_test->nb_processes > state->nb_processes){
228 if(state_test->heap_bytes_used < state->heap_bytes_used){
230 }else if(state_test->heap_bytes_used > state->heap_bytes_used){
233 *min = *max = cursor;
234 previous_cursor = cursor - 1;
235 while(previous_cursor >= 0){
236 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
237 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
239 *min = previous_cursor;
242 next_cursor = cursor + 1;
243 while(next_cursor < xbt_dynar_length(all_states)){
244 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
245 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
263 /** \brief Take a snapshot the current state and process it.
265 * \return number of the duplicate state or -1 (not visited)
267 static int is_visited_state(){
269 if(_sg_mc_visited == 0)
272 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
276 mc_visited_state_t new_state = visited_state_new();
278 if(xbt_dynar_is_empty(visited_states)){
280 xbt_dynar_push(visited_states, &new_state);
289 int min = -1, max = -1, index;
291 mc_visited_state_t state_test;
294 index = get_search_interval(visited_states, new_state, &min, &max);
296 if(min != -1 && max != -1){
298 // Parallell implementation
299 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
301 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
302 if(state_test->other_num == -1)
303 new_state->other_num = state_test->num;
305 new_state->other_num = state_test->other_num;
306 if(dot_output == NULL)
307 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
309 XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
310 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
311 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
314 return new_state->other_num;
318 while(cursor <= max){
319 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
320 if(snapshot_compare(state_test, new_state) == 0){
321 // The state has been visited:
323 if(state_test->other_num == -1)
324 new_state->other_num = state_test->num;
326 new_state->other_num = state_test->other_num;
327 if(dot_output == NULL)
328 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
330 XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
332 // Replace the old state with the new one (why?):
333 xbt_dynar_remove_at(visited_states, cursor, NULL);
334 xbt_dynar_insert_at(visited_states, cursor, &new_state);
338 return new_state->other_num;
343 // The state has not been visited, add it to the list:
344 xbt_dynar_insert_at(visited_states, min, &new_state);
348 // The state has not been visited: insert the state in the dynamic array.
349 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
350 if(state_test->nb_processes < new_state->nb_processes){
351 xbt_dynar_insert_at(visited_states, index+1, &new_state);
353 if(state_test->heap_bytes_used < new_state->heap_bytes_used)
354 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
356 xbt_dynar_insert_at(visited_states, index, &new_state);
361 // We have reached the maximum number of stored states;
362 if(xbt_dynar_length(visited_states) > _sg_mc_visited){
364 // Find the (index of the) older state:
365 int min2 = mc_stats->expanded_states;
366 unsigned int cursor2 = 0;
367 unsigned int index2 = 0;
368 xbt_dynar_foreach(visited_states, cursor2, state_test){
369 if(state_test->num < min2){
371 min2 = state_test->num;
376 xbt_dynar_remove_at(visited_states, index2, NULL);
388 * \brief Initialize the DPOR exploration algorithm
393 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
395 mc_state_t initial_state = NULL;
396 smx_process_t process;
398 /* Create the initial state and push it into the exploration stack */
401 if(_sg_mc_visited > 0)
402 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
404 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
406 initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
407 communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
410 initial_state = MC_state_new();
414 XBT_DEBUG("**************************************************");
415 XBT_DEBUG("Initial state");
417 /* Wait for requests (schedules processes) */
418 MC_wait_for_requests();
420 MC_ignore_heap(simix_global->process_to_run->data, 0);
421 MC_ignore_heap(simix_global->process_that_ran->data, 0);
425 /* Get an enabled process and insert it in the interleave set of the initial state */
426 xbt_swag_foreach(process, simix_global->process_list){
427 if(MC_process_is_enabled(process)){
428 MC_state_interleave_process(initial_state, process);
429 if(mc_reduce_kind != e_mc_reduce_none)
434 xbt_fifo_unshift(mc_stack_safety, initial_state);
436 /* To ensure the soundness of DPOR, we have to keep a list of
437 processes which are still enabled at each step of the exploration.
438 If max depth is reached, we interleave them in the state in which they have
439 been enabled for the first time. */
440 xbt_swag_foreach(process, simix_global->process_list){
441 if(MC_process_is_enabled(process)){
442 char *key = bprintf("%lu", process->pid);
443 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
444 xbt_dict_set(first_enabled_state, key, data, NULL);
459 /** \brief Model-check the application using a DFS exploration
460 * with DPOR (Dynamic Partial Order Reductions)
465 char *req_str = NULL;
467 smx_simcall_t req = NULL, prev_req = NULL;
468 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
469 smx_process_t process = NULL;
470 xbt_fifo_item_t item = NULL;
471 mc_state_t state_test = NULL;
473 int visited_state = -1;
475 int comm_pattern = 0;
476 int interleave_size = 0;
478 while (xbt_fifo_size(mc_stack_safety) > 0) {
480 /* Get current state */
482 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
484 XBT_DEBUG("**************************************************");
485 XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
486 xbt_fifo_size(mc_stack_safety), state, state->num,
487 MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
489 interleave_size = MC_state_interleave_size(state);
491 /* Update statistics */
492 mc_stats->visited_states++;
494 /* If there are processes to interleave and the maximum depth has not been reached
495 then perform one step of the exploration algorithm */
496 if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
497 (req = MC_state_get_request(state, &value)) && visited_state == -1) {
499 /* Debug information */
500 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
501 req_str = MC_request_to_string(req, value);
502 XBT_DEBUG("Execute: %s", req_str);
507 if(dot_output != NULL)
508 req_str = MC_request_get_dot_output(req, value);
511 MC_state_set_executed_request(state, req, value);
512 mc_stats->executed_transitions++;
515 char *key = bprintf("%lu", req->issuer->pid);
516 xbt_dict_remove(first_enabled_state, key);
520 if(req->call == SIMCALL_COMM_ISEND)
522 else if(req->call == SIMCALL_COMM_IRECV)
525 /* Answer the request */
526 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
529 if(comm_pattern != 0){
530 if(!initial_state_safety->initial_communications_pattern_done)
531 get_comm_pattern(initial_communications_pattern, req, comm_pattern);
533 get_comm_pattern(communications_pattern, req, comm_pattern);
539 /* Wait for requests (schedules processes) */
540 MC_wait_for_requests();
542 /* Create the new expanded state */
545 next_state = MC_state_new();
547 if((visited_state = is_visited_state()) == -1){
549 /* Get an enabled process and insert it in the interleave set of the next state */
550 xbt_swag_foreach(process, simix_global->process_list){
551 if(MC_process_is_enabled(process)){
552 MC_state_interleave_process(next_state, process);
553 if(mc_reduce_kind != e_mc_reduce_none)
558 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
559 next_state->system_state = MC_take_snapshot(next_state->num);
562 if(dot_output != NULL)
563 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
567 if(dot_output != NULL)
568 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
572 xbt_fifo_unshift(mc_stack_safety, next_state);
574 /* Insert in dict all enabled processes, if not included yet */
575 xbt_swag_foreach(process, simix_global->process_list){
576 if(MC_process_is_enabled(process)){
577 char *key = bprintf("%lu", process->pid);
578 if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
579 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
580 xbt_dict_set(first_enabled_state, key, data, NULL);
586 if(dot_output != NULL)
591 /* Let's loop again */
593 /* The interleave set is empty or the maximum depth is reached, let's back-track */
596 if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
598 if(user_max_depth_reached && visited_state == -1)
599 XBT_DEBUG("User max depth reached !");
600 else if(visited_state == -1)
601 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
605 /* Interleave enabled processes in the state in which they have been enabled for the first time */
606 xbt_swag_foreach(process, simix_global->process_list){
607 if(MC_process_is_enabled(process)){
608 char *key = bprintf("%lu", process->pid);
609 enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
611 int cursor = xbt_fifo_size(mc_stack_safety);
612 xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
613 if(cursor-- == enabled){
614 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
615 XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
616 MC_state_interleave_process(state_test, process);
626 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
632 if(!initial_state_safety->initial_communications_pattern_done){
633 print_communications_pattern(initial_communications_pattern);
635 if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
636 print_communications_pattern(communications_pattern);
637 deterministic_pattern(initial_communications_pattern, communications_pattern);
640 initial_state_safety->initial_communications_pattern_done = 1;
644 /* Trash the current state, no longer needed */
646 xbt_fifo_shift(mc_stack_safety);
647 MC_state_delete(state);
648 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
651 /* Check for deadlocks */
652 if(MC_deadlock_check()){
653 MC_show_deadlock(NULL);
658 /* Traverse the stack backwards until a state with a non empty interleave
659 set is found, deleting all the states that have it empty in the way.
660 For each deleted state, check if the request that has generated it
661 (from it's predecesor state), depends on any other previous request
662 executed before it. If it does then add it to the interleave set of the
663 state that executed that previous request. */
665 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
666 if(mc_reduce_kind != e_mc_reduce_none){
667 req = MC_state_get_internal_request(state);
668 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
669 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
670 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
671 XBT_DEBUG("Dependent Transitions:");
672 prev_req = MC_state_get_executed_request(prev_state, &value);
673 req_str = MC_request_to_string(prev_req, value);
674 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
676 prev_req = MC_state_get_executed_request(state, &value);
677 req_str = MC_request_to_string(prev_req, value);
678 XBT_DEBUG("%s (state=%d)", req_str, state->num);
682 if(!MC_state_process_is_done(prev_state, req->issuer))
683 MC_state_interleave_process(prev_state, req->issuer);
685 XBT_DEBUG("Process %p is in done set", req->issuer);
689 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
691 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
696 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", req->call, req->issuer->pid, state->num, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid, prev_state->num);
702 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
703 /* We found a back-tracking point, let's loop */
704 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
705 if(_sg_mc_checkpoint){
706 if(state->system_state != NULL){
707 MC_restore_snapshot(state->system_state);
708 xbt_fifo_unshift(mc_stack_safety, state);
711 pos = xbt_fifo_size(mc_stack_safety);
712 item = xbt_fifo_get_first_item(mc_stack_safety);
714 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
715 if(restore_state->system_state != NULL){
718 item = xbt_fifo_get_next_item(item);
722 MC_restore_snapshot(restore_state->system_state);
723 xbt_fifo_unshift(mc_stack_safety, state);
725 MC_replay(mc_stack_safety, pos);
728 xbt_fifo_unshift(mc_stack_safety, state);
730 MC_replay(mc_stack_safety, -1);
732 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
735 req = MC_state_get_internal_request(state);
736 if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
737 // fprintf(stderr, "Remove state with isend or irecv\n");
738 if(!xbt_dynar_is_empty(communications_pattern))
739 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
741 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
742 MC_state_delete(state);
748 MC_print_statistics(mc_stats);