#include "mc_safety.h"
#include "mc_liveness.h"
#include "mc_private.h"
+#include "mc_process.h"
+#include "mc_smx.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
"Logging specific to state equaity detection mechanisms");
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);
+
+ if (MC_process_is_self(&mc_model_checker->process)) {
+ new_state->nb_processes = xbt_swag_size(simix_global->process_list);
+ } else {
+ MC_process_smx_refresh(&mc_model_checker->process);
+ new_state->nb_processes = xbt_dynar_length(mc_model_checker->process.smx_process_infos);
+ }
+
new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
new_state->num = mc_stats->expanded_states;
new_state->other_num = -1;
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;