/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
-#include "mc_private.h"
#include <unistd.h>
#include <sys/wait.h>
+#include "mc_comm_pattern.h"
+#include "mc_safety.h"
+#include "mc_liveness.h"
+#include "mc_private.h"
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
"Logging specific to state equaity detection mechanisms");
*/
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;
xbt_automaton_state_t automaton_state,
xbt_dynar_t atomic_propositions)
{
+ 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 = MC_take_snapshot(pair_num);
- pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+ 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;
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 {
+ 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) {
- 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) {
+ 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 {
+ 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;
- xbt_dynar_foreach(visited_states, cursor2, state_test) {
- if (state_test->num < min2) {
+ xbt_dynar_foreach(visited_states, cursor2, state_test){
+ if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
index2 = cursor2;
min2 = state_test->num;
}
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++;
}
unsigned int cursor2 = 0;
unsigned int index2 = 0;
xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
- if (pair_test->num < min2) {
+ if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
index2 = cursor2;
min2 = pair_test->num;
}
