xbt_dynar_t visited_states;
static int is_exploration_stack_state(mc_visited_state_t state){
- xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+ xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
while (item) {
if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
return 1;
}
- item = xbt_fifo_get_prev_item(item);
+ item = xbt_fifo_get_next_item(item);
}
return 0;
}
*/
static mc_visited_state_t visited_state_new()
{
+ mc_process_t process = &(mc_model_checker->process);
mc_visited_state_t new_state = NULL;
new_state = xbt_new0(s_mc_visited_state_t, 1);
- new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+ new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
+ MC_process_get_heap(process)->heaplimit,
+ MC_process_get_malloc_info(process));
new_state->nb_processes = xbt_swag_size(simix_global->process_list);
new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
new_state->num = mc_stats->expanded_states;
return new_state;
}
-mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_snapshot_t system_state)
+mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
{
+ mc_process_t process = &(mc_model_checker->process);
mc_visited_pair_t pair = NULL;
pair = xbt_new0(s_mc_visited_pair_t, 1);
- pair->graph_state = MC_state_new();
- pair->graph_state->system_state = (system_state == NULL) ? MC_take_snapshot(pair_num) : system_state;
- pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+ pair->graph_state = graph_state;
+ if(pair->graph_state->system_state == NULL)
+ pair->graph_state->system_state = MC_take_snapshot(pair_num);
+ pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
+ MC_process_get_heap(process)->heaplimit,
+ MC_process_get_malloc_info(process));
pair->nb_processes = xbt_swag_size(simix_global->process_list);
pair->automaton_state = automaton_state;
pair->num = pair_num;
pair->acceptance_removed = 0;
pair->visited_removed = 0;
pair->acceptance_pair = 0;
- pair->in_exploration_stack = 1;
pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
unsigned int cursor = 0;
int value;
}
static int is_exploration_stack_pair(mc_visited_pair_t pair){
- xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+ xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
while (item) {
if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
return 1;
}
- item = xbt_fifo_get_prev_item(item);
+ item = xbt_fifo_get_next_item(item);
}
return 0;
}
void MC_visited_pair_delete(mc_visited_pair_t p)
{
p->automaton_state = NULL;
- MC_state_delete(p->graph_state, !is_exploration_stack_pair(p));
+ if( !is_exploration_stack_pair(p))
+ MC_state_delete(p->graph_state, 1);
xbt_dynar_free(&(p->atomic_propositions));
xbt_free(p);
p = NULL;
int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
{
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
int cursor = 0, previous_cursor, next_cursor;
int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
*max = next_cursor;
next_cursor++;
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
return -1;
}
}
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
return cursor;
}
are incomplete and they cannot be analyzed and compared with the initial pattern. */
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
int current_process = 1;
- while (current_process < simix_process_maxpid) {
+ while (current_process < MC_smx_get_maxpid()) {
if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
partial_comm = 1;
}
}
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
mc_visited_state_t new_state = visited_state_new();
graph_state->system_state = new_state->system_state;
if (xbt_dynar_is_empty(visited_states)) {
xbt_dynar_push(visited_states, &new_state);
-
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
return NULL;
} else {
xbt_dynar_insert_at(visited_states, cursor, &new_state);
XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
return state_test;
}
cursor++;
XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
return NULL;
-
}
}
if (_sg_mc_visited == 0)
return -1;
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
mc_visited_pair_t new_visited_pair = NULL;
if (visited_pair == NULL) {
- new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state->system_state);
+ new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
} else {
new_visited_pair = visited_pair;
}
} else {
MC_visited_pair_delete(pair_test);
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
return new_visited_pair->other_num;
}
}
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
return -1;
}
