+ XBT_INFO("Counter-example execution trace:");
+ MC_show_stack_safety_stateful(mc_stack_safety_stateful);
+}
+
+void MC_dump_stack_safety_stateful(xbt_fifo_t stack)
+{
+ //mc_state_ws_t state;
+
+ MC_show_stack_safety_stateful(stack);
+
+ /*MC_SET_RAW_MEM;
+ while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
+ MC_state_delete(state);
+ MC_UNSET_RAW_MEM;*/
+}
+
+
+void MC_show_stack_safety_stateful(xbt_fifo_t stack)
+{
+ int value;
+ mc_state_ws_t state;
+ xbt_fifo_item_t item;
+ smx_req_t req;
+ char *req_str = NULL;
+
+ for (item = xbt_fifo_get_last_item(stack);
+ (item ? (state = (mc_state_ws_t) (xbt_fifo_get_item_content(item)))
+ : (NULL)); item = xbt_fifo_get_prev_item(item)) {
+ req = MC_state_get_executed_request(state->graph_state, &value);
+ if(req){
+ req_str = MC_request_to_string(req, value);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
+ }
+ }
+}
+
+void MC_show_stack_liveness_stateful(xbt_fifo_t stack){
+ int value;
+ mc_pair_t pair;
+ xbt_fifo_item_t item;
+ smx_req_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){
+ req_str = MC_request_to_string(req, value);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
+ }
+ }
+}
+
+void MC_dump_stack_liveness_stateful(xbt_fifo_t stack){
+ 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;
+}
+
+void MC_show_stack_liveness_stateless(xbt_fifo_t stack){
+ int value;
+ mc_pair_stateless_t pair;
+ xbt_fifo_item_t item;
+ smx_req_t req;
+ char *req_str = NULL;
+
+ for (item = xbt_fifo_get_last_item(stack);
+ (item ? (pair = (mc_pair_stateless_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){
+ req_str = MC_request_to_string(req, value);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
+ }
+ }
+}
+
+void MC_dump_stack_liveness_stateless(xbt_fifo_t stack){
+ mc_pair_stateless_t pair;
+
+ MC_SET_RAW_MEM;
+ while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
+ MC_pair_stateless_delete(pair);
+ MC_UNSET_RAW_MEM;