int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
void *ref_test;
- if (_sg_mc_safety) {
- nb_processes = ((mc_visited_state_t) ref)->nb_processes;
- heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
- } else if (_sg_mc_liveness) {
+ if (_sg_mc_liveness) {
nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
} else {
- xbt_die("Both liveness and safety are disabled.");
+ nb_processes = ((mc_visited_state_t) ref)->nb_processes;
+ heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
}
int start = 0;
while (start <= end) {
cursor = (start + end) / 2;
- if (_sg_mc_safety) {
+ if (_sg_mc_liveness) {
ref_test =
- (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
- mc_visited_state_t);
- nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
- heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
- } else if (_sg_mc_liveness) {
- ref_test =
- (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
+ (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
} else {
- nb_processes_test = 0;
- heap_bytes_used_test = 0;
- xbt_die("Both liveness and safety are disabled.");
+ ref_test =
+ (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
+ mc_visited_state_t);
+ nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
+ heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
}
if (nb_processes_test < nb_processes) {
start = cursor + 1;
*min = *max = cursor;
previous_cursor = cursor - 1;
while (previous_cursor >= 0) {
- if (_sg_mc_safety) {
+ if (_sg_mc_liveness) {
+ ref_test =
+ (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
+ mc_visited_pair_t);
+ nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
+ heap_bytes_used_test =
+ ((mc_visited_pair_t) ref_test)->heap_bytes_used;
+ } else {
ref_test =
(mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
mc_visited_state_t);
nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
heap_bytes_used_test =
((mc_visited_state_t) ref_test)->heap_bytes_used;
- } else if (_sg_mc_liveness) {
- ref_test =
- (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
- mc_visited_pair_t);
- nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
- heap_bytes_used_test =
- ((mc_visited_pair_t) ref_test)->heap_bytes_used;
}
if (nb_processes_test != nb_processes
|| heap_bytes_used_test != heap_bytes_used)
}
next_cursor = cursor + 1;
while (next_cursor < xbt_dynar_length(list)) {
- if (_sg_mc_safety) {
- ref_test =
- (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
- mc_visited_state_t);
- nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
- heap_bytes_used_test =
- ((mc_visited_state_t) ref_test)->heap_bytes_used;
- } else if (_sg_mc_liveness) {
+ if (_sg_mc_liveness) {
ref_test =
(mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
mc_visited_pair_t);
nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
heap_bytes_used_test =
((mc_visited_pair_t) ref_test)->heap_bytes_used;
+ } else {
+ ref_test =
+ (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
+ mc_visited_state_t);
+ nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
+ heap_bytes_used_test =
+ ((mc_visited_state_t) ref_test)->heap_bytes_used;
}
if (nb_processes_test != nb_processes
|| heap_bytes_used_test != heap_bytes_used)
/**
* \brief Checks whether a given state has already been visited by the algorithm.
*/
-int is_visited_state()
+
+mc_visited_state_t is_visited_state()
{
if (_sg_mc_visited == 0)
- return -1;
+ return NULL;
+
+ /* If comm determinism verification, we cannot stop the exploration if some
+ communications are not finished (at least, data are transfered). These communications
+ 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) {
+ if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)))
+ return NULL;
+ current_process++;
+ }
+ }
int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
if (!mc_mem_set)
MC_SET_STD_HEAP;
- return -1;
+ return NULL;
} else {
("State %d already visited ! (equal to state %d (state %d in dot_output))",
new_state->num, state_test->num, new_state->other_num);
- // Replace the old state with the new one (why?):
+ /* Replace the old state with the new one (with a bigger num)
+ (when the max number of visited states is reached, the oldest
+ one is removed according to its number (= with the min number) */
xbt_dynar_remove_at(visited_states, cursor, NULL);
xbt_dynar_insert_at(visited_states, cursor, &new_state);
if (!mc_mem_set)
MC_SET_STD_HEAP;
- return new_state->other_num;
+ return state_test;
}
cursor++;
}
- // The state has not been visited, add it to the list:
+ // The state has not been visited: insert the state in the dynamic array.
xbt_dynar_insert_at(visited_states, min, &new_state);
} else {
// We have reached the maximum number of stored states;
if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
- // Find the (index of the) older state:
+ // Find the (index of the) older state (with the smallest num):
int min2 = mc_stats->expanded_states;
unsigned int cursor2 = 0;
unsigned int index2 = 0;
if (!mc_mem_set)
MC_SET_STD_HEAP;
- return -1;
+ return NULL;
}
}
pair_test =
(mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
mc_visited_pair_t);
- //if(pair_test->acceptance_pair == 0){ /* Acceptance pair have been already checked before */
if (xbt_automaton_state_compare
(pair_test->automaton_state, new_pair->automaton_state) == 0) {
if (xbt_automaton_propositional_symbols_compare_value
return new_pair->other_num;
}
}
- //}
}
cursor++;
}
