int _sg_do_model_check = 0;
int _sg_mc_checkpoint = 0;
+ int _sg_mc_sparse_checkpoint = 0;
+ int _sg_mc_soft_dirty = 1;
char *_sg_mc_property_file = NULL;
int _sg_mc_timeout = 0;
int _sg_mc_hash = 0;
_sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
}
+ void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
+ xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ }
+ _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
+ }
+
+ void _mc_cfg_cb_soft_dirty(const char *name, int pos) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
+ xbt_die("You are specifying a soft dirty value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ }
+ _sg_mc_soft_dirty = xbt_cfg_get_boolean(_sg_cfg_set, name);
+ }
+
void _mc_cfg_cb_property(const char *name, int pos)
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
+ mc_reduce_kind = e_mc_reduce_none;
}
void _mc_cfg_cb_send_determinism(const char *name, int pos)
("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
_sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
+ mc_reduce_kind = e_mc_reduce_none;
}
/* MC global data structures */
}
+ mc_model_checker_t mc_model_checker = NULL;
+
void MC_init()
{
-
int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
mc_time = xbt_new0(double, simix_process_maxpid);
MC_SET_MC_HEAP;
+ mc_model_checker = xbt_new0(s_mc_model_checker_t, 1);
+ mc_model_checker->pages = mc_pages_store_new();
+ mc_model_checker->fd_clear_refs = -1;
+ mc_model_checker->fd_pagemap = -1;
+
mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
/* Initialize statistics */
MC_ignore_local_variable("ctx", "*");
MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
- MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
+ MC_ignore_local_variable("next_cont"
+ "ext", "smx_ctx_sysv_suspend_serial");
MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
/* Ignore local variable about time used for tracing */
MC_ignore_local_variable("start_time", "*");
+ MC_ignore_global_variable("mc_model_checker");
+
+ // Mot of those things could be moved into mc_model_checker:
MC_ignore_global_variable("compared_pointers");
MC_ignore_global_variable("mc_comp_times");
MC_ignore_global_variable("mc_snapshot_comparison_time");
MC_ignore_global_variable("maestro_stack_start");
MC_ignore_global_variable("maestro_stack_end");
MC_ignore_global_variable("smx_total_comms");
+ MC_ignore_global_variable("communications_pattern");
+ MC_ignore_global_variable("initial_communications_pattern");
+ MC_ignore_global_variable("incomplete_communications_pattern");
+ if (MC_is_active()) {
+ MC_ignore_global_variable("mc_diff_info");
+ }
+
MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
smx_process_t process;
{
int raw_mem = (mmalloc_get_current_heap() == mc_heap);
- int value, i = 1, count = 1;
+ int value, i = 1, count = 1, call = 0, j;
char *req_str;
smx_simcall_t req = NULL, saved_req = NULL;
xbt_fifo_item_t item, start_item;
mc_state_t state;
smx_process_t process = NULL;
- int comm_pattern = 0;
smx_action_t current_comm;
XBT_DEBUG("**** Begin Replay ****");
MC_SET_MC_HEAP;
- if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) {
+ if (mc_reduce_kind == e_mc_reduce_dpor) {
xbt_dict_reset(first_enabled_state);
xbt_swag_foreach(process, simix_global->process_list) {
if (MC_process_is_enabled(process)) {
}
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- xbt_dynar_reset(communications_pattern);
- xbt_dynar_reset(incomplete_communications_pattern);
+ for (j=0; j<simix_process_maxpid; j++) {
+ xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(communications_pattern, j, xbt_dynar_t));
+ }
+ for (j=0; j<simix_process_maxpid; j++) {
+ xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
+ }
}
MC_SET_STD_HEAP;
state = (mc_state_t) xbt_fifo_get_item_content(item);
saved_req = MC_state_get_executed_request(state, &value);
- if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) {
+ if (mc_reduce_kind == e_mc_reduce_dpor) {
MC_SET_MC_HEAP;
char *key = bprintf("%lu", saved_req->issuer->pid);
xbt_dict_remove(first_enabled_state, key);
/* TODO : handle test and testany simcalls */
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
if (req->call == SIMCALL_COMM_ISEND)
- comm_pattern = 1;
+ call = 1;
else if (req->call == SIMCALL_COMM_IRECV)
- comm_pattern = 2;
+ call = 2;
else if (req->call == SIMCALL_COMM_WAIT)
- comm_pattern = 3;
+ call = 3;
else if (req->call == SIMCALL_COMM_WAITANY)
- comm_pattern = 4;
+ call = 4;
}
SIMIX_simcall_pre(req, value);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
MC_SET_MC_HEAP;
- if (comm_pattern == 1 || comm_pattern == 2) {
- get_comm_pattern(communications_pattern, req, comm_pattern);
- } else if (comm_pattern == 3 /* || comm_pattern == 4 */ ) {
+ if (call == 1) { /* Send */
+ get_comm_pattern(communications_pattern, req, call);
+ } else if (call == 2) { /* Recv */
+ get_comm_pattern(communications_pattern, req, call);
+ } else if (call == 3) { /* Wait */
current_comm = simcall_comm_wait__get__comm(req);
- if (current_comm->comm.refcount == 1) { /* First wait only must be considered */
+ if (current_comm->comm.refcount == 1) /* First wait only must be considered */
complete_comm_pattern(communications_pattern, current_comm);
- }
- } else if (comm_pattern == 4 /* || comm_pattern == 4 */ ) {
- current_comm =
- xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value,
- smx_action_t);
- if (current_comm->comm.refcount == 1) { /* First wait only must be considered */
+ } else if (call == 4) { /* WaitAny */
+ current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
+ if (current_comm->comm.refcount == 1) /* First wait only must be considered */
complete_comm_pattern(communications_pattern, current_comm);
- }
}
MC_SET_STD_HEAP;
- comm_pattern = 0;
+ call = 0;
}
count++;
- if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) {
+ if (mc_reduce_kind == e_mc_reduce_dpor) {
MC_SET_MC_HEAP;
/* Insert in dict all enabled processes */
xbt_swag_foreach(process, simix_global->process_list) {
#include "simgrid_config.h"
#include <stdio.h>
+ #include <stdbool.h>
#ifndef WIN32
#include <sys/mman.h>
#endif
#include "msg/datatypes.h"
#include "xbt/strbuff.h"
#include "xbt/parmap.h"
+ #include "mc_mmu.h"
+ #include "mc_page_store.h"
+
+ SG_BEGIN_DECL()
typedef struct s_dw_frame s_dw_frame_t, *dw_frame_t;
typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function_index_item_t;
void *data;
// Size of the data region:
size_t size;
+ // For per-page snapshots, this is an array to the number of
+ size_t* page_numbers;
} s_mc_mem_region_t, *mc_mem_region_t;
+ static inline __attribute__ ((always_inline))
+ bool mc_region_contain(mc_mem_region_t region, void* p)
+ {
+ return p >= region->start_addr &&
+ p < (void*)((char*) region->start_addr + region->size);
+ }
+
/** Ignored data
*
* Some parts of the snapshot are ignored by zeroing them out: the real
xbt_dynar_t ignored_data;
} s_mc_snapshot_t, *mc_snapshot_t;
+ mc_mem_region_t mc_get_snapshot_region(void* addr, mc_snapshot_t snapshot);
+
+ static inline __attribute__ ((always_inline))
+ mc_mem_region_t mc_get_region_hinted(void* addr, mc_snapshot_t snapshot, mc_mem_region_t region)
+ {
+ if (mc_region_contain(region, addr))
+ return region;
+ else
+ return mc_get_snapshot_region(addr, snapshot);
+ }
+
/** Information about a given stack frame
*
*/
typedef struct s_mc_snapshot_stack{
xbt_dynar_t local_variables;
- void *stack_pointer;
- void *real_address;
xbt_dynar_t stack_frames; // mc_stack_frame_t
}s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
size_t size;
}s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t;
- inline static void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) {
- if(snapshot==NULL)
- xbt_die("snapshot is NULL");
- xbt_mheap_t heap = (xbt_mheap_t)snapshot->regions[0]->data;
- return heap->breakval;
- }
+ static void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot);
mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall);
mc_snapshot_t MC_take_snapshot(int num_state);
void MC_restore_snapshot(mc_snapshot_t);
void MC_free_snapshot(mc_snapshot_t);
- /** \brief Translate a pointer from process address space to snapshot address space
- *
- * The address space contains snapshot of the main/application memory:
- * this function finds the address in a given snaphot for a given
- * real/application address.
- *
- * For read only memory regions and other regions which are not int the
- * snapshot, the address is not changed.
- *
- * \param addr Application address
- * \param snapshot The snapshot of interest (if NULL no translation is done)
- * \return Translated address in the snapshot address space
- * */
- void* mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot);
+ int mc_important_snapshot(mc_snapshot_t snapshot);
- /** \brief Translate a pointer from the snapshot address space to the application address space
- *
- * This is the inverse of mc_translate_address.
+ size_t* mc_take_page_snapshot_region(void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages);
+ void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
+ void mc_restore_page_snapshot_region(mc_mem_region_t region, size_t page_count, uint64_t* pagemap, mc_mem_region_t reference_region);
+
+ mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, size_t size, mc_mem_region_t ref_reg);
+ void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg);
+ void mc_softdirty_reset();
+
+ static inline __attribute__((always_inline))
+ bool mc_snapshot_region_linear(mc_mem_region_t region) {
+ return !region || !region->data;
+ }
+
+ void* mc_snapshot_read_fragmented(void* addr, mc_mem_region_t region, void* target, size_t size);
+
+ void* mc_snapshot_read(void* addr, mc_snapshot_t snapshot, void* target, size_t size);
+ int mc_snapshot_region_memcp(
+ void* addr1, mc_mem_region_t region1,
+ void* addr2, mc_mem_region_t region2, size_t size);
+ int mc_snapshot_memcp(
+ void* addr1, mc_snapshot_t snapshot1,
+ void* addr2, mc_snapshot_t snapshot2, size_t size);
+
+ static void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot);
+
+ /** @brief State of the model-checker (global variables for the model checker)
*
- * \param addr Address in the snapshot address space
- * \param snapsot Snapshot of interest (if NULL no translation is done)
- * \return Translated address in the application address space
+ * Each part of the state of the model chercker represented as a global
+ * variable prevents some sharing between snapshots and must be ignored.
+ * By moving as much state as possible in this structure allocated
+ * on the model-chercker heap, we avoid those issues.
*/
- uintptr_t mc_untranslate_address(void* addr, mc_snapshot_t snapshot);
+ typedef struct s_mc_model_checker {
+ // This is the parent snapshot of the current state:
+ mc_snapshot_t parent_snapshot;
+ mc_pages_store_t pages;
+ int fd_clear_refs;
+ int fd_pagemap;
+ } s_mc_model_checker_t, *mc_model_checker_t;
+
+ extern mc_model_checker_t mc_model_checker;
extern xbt_dynar_t mc_checkpoint_ignore;
}s_mc_visited_state_t, *mc_visited_state_t;
extern xbt_dynar_t visited_states;
-int is_visited_state(void);
+mc_visited_state_t is_visited_state(void);
void visited_state_free(mc_visited_state_t state);
void visited_state_free_voidp(void *s);
};
void* mc_member_resolve(const void* base, dw_type_t type, dw_type_t member, mc_snapshot_t snapshot);
- void* mc_member_snapshot_resolve(const void* base, dw_type_t type, dw_type_t member, mc_snapshot_t snapshot);
typedef struct s_dw_variable{
Dwarf_Off dwarf_offset; /* Global offset of the field. */
void *data;
}s_mc_comm_pattern_t, *mc_comm_pattern_t;
+extern xbt_dynar_t initial_communications_pattern;
extern xbt_dynar_t communications_pattern;
extern xbt_dynar_t incomplete_communications_pattern;
* */
uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks);
+ /* *********** Snapshot *********** */
+
+ static inline __attribute__((always_inline))
+ void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region)
+ {
+ size_t pageno = mc_page_number(region->start_addr, (void*) addr);
+ size_t snapshot_pageno = region->page_numbers[pageno];
+ const void* snapshot_page = mc_page_store_get_page(mc_model_checker->pages, snapshot_pageno);
+ return (char*) snapshot_page + mc_page_offset((void*) addr);
+ }
+
+ /** \brief Translate a pointer from process address space to snapshot address space
+ *
+ * The address space contains snapshot of the main/application memory:
+ * this function finds the address in a given snaphot for a given
+ * real/application address.
+ *
+ * For read only memory regions and other regions which are not int the
+ * snapshot, the address is not changed.
+ *
+ * \param addr Application address
+ * \param snapshot The snapshot of interest (if NULL no translation is done)
+ * \return Translated address in the snapshot address space
+ * */
+ static inline __attribute__((always_inline))
+ void* mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot)
+ {
+
+ // If not in a process state/clone:
+ if (!snapshot) {
+ return (uintptr_t *) addr;
+ }
+
+ mc_mem_region_t region = mc_get_snapshot_region((void*) addr, snapshot);
+
+ xbt_assert(mc_region_contain(region, (void*) addr), "Trying to read out of the region boundary.");
+
+ if (!region) {
+ return (void *) addr;
+ }
+
+ // Flat snapshot:
+ else if (region->data) {
+ uintptr_t offset = addr - (uintptr_t) region->start_addr;
+ return (void *) ((uintptr_t) region->data + offset);
+ }
+
+ // Per-page snapshot:
+ else if (region->page_numbers) {
+ return mc_translate_address_region(addr, region);
+ }
+
+ else {
+ xbt_die("No data for this memory region");
+ }
+ }
+
+ static inline __attribute__ ((always_inline))
+ void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) {
+ if(snapshot==NULL)
+ xbt_die("snapshot is NULL");
+ void** addr = &((xbt_mheap_t)std_heap)->breakval;
+ return mc_snapshot_read_pointer(addr, snapshot);
+ }
+
+ static inline __attribute__ ((always_inline))
+ void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot)
+ {
+ void* res;
+ return *(void**) mc_snapshot_read(addr, snapshot, &res, sizeof(void*));
+ }
+
+ /** @brief Read memory from a snapshot region
+ *
+ * @param addr Process (non-snapshot) address of the data
+ * @param region Snapshot memory region where the data is located
+ * @param target Buffer to store the value
+ * @param size Size of the data to read in bytes
+ * @return Pointer where the data is located (target buffer of original location)
+ */
+ static inline __attribute__((always_inline))
+ void* mc_snapshot_read_region(void* addr, mc_mem_region_t region, void* target, size_t size)
+ {
+ uintptr_t offset = (uintptr_t) addr - (uintptr_t) region->start_addr;
+
+ xbt_assert(addr >= region->start_addr && (char*) addr+size < (char*)region->start_addr+region->size,
+ "Trying to read out of the region boundary.");
+
+ // Linear memory region:
+ if (region->data) {
+ return (void*) ((uintptr_t) region->data + offset);
+ }
+
+ // Fragmented memory region:
+ else if (region->page_numbers) {
+ void* end = (char*) addr + size - 1;
+ if( mc_same_page(addr, end) ) {
+ // The memory is contained in a single page:
+ return mc_translate_address_region((uintptr_t) addr, region);
+ } else {
+ // The memory spans several pages:
+ return mc_snapshot_read_fragmented(addr, region, target, size);
+ }
+ }
+
+ else {
+ xbt_die("No data available for this region");
+ }
+ }
+
+
+ SG_END_DECL()
+
#endif
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;
- 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;
}
