From ccb2167210583f3eb1249db10916cfd7389cb0df Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 29 Mar 2016 10:59:06 +0200 Subject: [PATCH] [mc] Making a State a class --- src/mc/CommunicationDeterminismChecker.cpp | 13 ++--- src/mc/LivenessChecker.cpp | 6 +-- src/mc/LivenessChecker.hpp | 6 +-- src/mc/SafetyChecker.cpp | 24 +++++---- src/mc/mc_comm_pattern.cpp | 6 +-- src/mc/mc_comm_pattern.h | 6 +-- src/mc/mc_global.cpp | 8 +-- src/mc/mc_private.h | 2 +- src/mc/mc_safety.h | 2 +- src/mc/mc_state.cpp | 62 +++++++++++++--------- src/mc/mc_state.h | 51 ++++++++++-------- src/mc/mc_visited.cpp | 6 +-- 12 files changed, 106 insertions(+), 86 deletions(-) diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 935568da5f..9f7c2a2e18 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -318,7 +318,7 @@ RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) { // Find (pid, value): - mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item); + simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item); int value = 0; smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); @@ -336,7 +336,7 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o std::vector res; for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack); item; item = xbt_fifo_get_prev_item(item)) { - mc_state_t state = (mc_state_t)xbt_fifo_get_item_content(item); + simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item); int value; smx_simcall_t req = MC_state_get_executed_request(state, &value); if (req) { @@ -351,7 +351,7 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o void CommunicationDeterminismChecker::prepare() { - mc_state_t initial_state = nullptr; + simgrid::mc::State* initial_state = nullptr; int i; const int maxpid = MC_smx_get_maxpid(); @@ -409,12 +409,13 @@ int CommunicationDeterminismChecker::main(void) int value; std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; - mc_state_t state = nullptr, next_state = NULL; + simgrid::mc::State* state = nullptr; + simgrid::mc::State* next_state = nullptr; while (xbt_fifo_size(mc_stack) > 0) { /* Get current state */ - state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); + state = (simgrid::mc::State*) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); XBT_DEBUG("**************************************************"); XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)", @@ -508,7 +509,7 @@ int CommunicationDeterminismChecker::main(void) return SIMGRID_MC_EXIT_DEADLOCK; } - while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != nullptr) + while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack)) != nullptr) if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1); diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index 850be7afb9..589a71d5ad 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -43,7 +43,7 @@ static xbt_fifo_t liveness_stack; namespace simgrid { namespace mc { -VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state) +VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, simgrid::mc::State* graph_state) { simgrid::mc::Process* process = &(mc_model_checker->process()); @@ -257,7 +257,7 @@ void LivenessChecker::replay(xbt_fifo_t stack) { xbt_fifo_item_t item; simgrid::mc::Pair* pair = nullptr; - mc_state_t state = nullptr; + simgrid::mc::State* state = nullptr; smx_simcall_t req = nullptr, saved_req = NULL; int value, depth = 1; char *req_str; @@ -284,7 +284,7 @@ void LivenessChecker::replay(xbt_fifo_t stack) pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item); - state = (mc_state_t) pair->graph_state; + state = (simgrid::mc::State*) pair->graph_state; if (pair->exploration_started) { diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp index 263bde47e8..150cd53673 100644 --- a/src/mc/LivenessChecker.hpp +++ b/src/mc/LivenessChecker.hpp @@ -30,7 +30,7 @@ extern XBT_PRIVATE xbt_automaton_t property_automaton; struct XBT_PRIVATE Pair { int num = 0; int search_cycle = 0; - mc_state_t graph_state = nullptr; /* System state included */ + simgrid::mc::State* graph_state = nullptr; /* System state included */ xbt_automaton_state_t automaton_state = nullptr; simgrid::xbt::unique_ptr atomic_propositions; int requests = 0; @@ -49,7 +49,7 @@ struct XBT_PRIVATE VisitedPair { int num = 0; int other_num = 0; /* Dot output for */ int acceptance_pair = 0; - mc_state_t graph_state = nullptr; /* System state included */ + simgrid::mc::State* graph_state = nullptr; /* System state included */ xbt_automaton_state_t automaton_state = nullptr; simgrid::xbt::unique_ptr atomic_propositions; size_t heap_bytes_used = 0; @@ -57,7 +57,7 @@ struct XBT_PRIVATE VisitedPair { int acceptance_removed = 0; int visited_removed = 0; - VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state); + VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, simgrid::mc::State* graph_state); ~VisitedPair(); }; diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 2c9ca22ef0..a32a1a3205 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -44,7 +44,7 @@ static void MC_show_non_termination(void) MC_print_statistics(mc_stats); } -static int snapshot_compare(mc_state_t state1, mc_state_t state2) +static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2) { simgrid::mc::Snapshot* s1 = state1->system_state; simgrid::mc::Snapshot* s2 = state2->system_state; @@ -53,12 +53,12 @@ static int snapshot_compare(mc_state_t state1, mc_state_t state2) return snapshot_compare(num1, s1, num2, s2); } -static int is_exploration_stack_state(mc_state_t current_state){ +static int is_exploration_stack_state(simgrid::mc::State* current_state){ xbt_fifo_item_t item; - mc_state_t stack_state; + simgrid::mc::State* stack_state; for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) { - stack_state = (mc_state_t) xbt_fifo_get_item_content(item); + stack_state = (simgrid::mc::State*) xbt_fifo_get_item_content(item); if(snapshot_compare(stack_state, current_state) == 0){ XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num); return 1; @@ -75,7 +75,7 @@ RecordTrace SafetyChecker::getRecordTrace() // override for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) { // Find (pid, value): - mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item); + simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item); int value = 0; smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); @@ -92,7 +92,7 @@ std::vector SafetyChecker::getTextualTrace() // override std::vector trace; for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack); item; item = xbt_fifo_get_prev_item(item)) { - mc_state_t state = (mc_state_t)xbt_fifo_get_item_content(item); + simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item); int value; smx_simcall_t req = MC_state_get_executed_request(state, &value); if (req) { @@ -112,14 +112,16 @@ int SafetyChecker::run() char *req_str = nullptr; int value; smx_simcall_t req = nullptr; - mc_state_t state = nullptr, prev_state = NULL, next_state = NULL; + simgrid::mc::State* state = nullptr; + simgrid::mc::State* prev_state = nullptr; + simgrid::mc::State* next_state = nullptr; xbt_fifo_item_t item = nullptr; std::unique_ptr visited_state = nullptr; while (xbt_fifo_size(mc_stack) > 0) { /* Get current state */ - state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); + state = (simgrid::mc::State*)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); XBT_DEBUG("**************************************************"); XBT_DEBUG @@ -219,14 +221,14 @@ int SafetyChecker::run() executed before it. If it does then add it to the interleave set of the state that executed that previous request. */ - while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) { + while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack))) { if (reductionMode_ == simgrid::mc::ReductionMode::dpor) { req = MC_state_get_internal_request(state); if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK) xbt_die("Mutex is currently not supported with DPOR, " "use --cfg=model-check/reduction:none"); const smx_process_t issuer = MC_smx_simcall_get_issuer(req); - xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) { + xbt_fifo_foreach(mc_stack, item, prev_state, simgrid::mc::State*) { if (reductionMode_ != simgrid::mc::ReductionMode::none && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { @@ -307,7 +309,7 @@ void SafetyChecker::init() simgrid::mc::visited_states.clear(); - mc_state_t initial_state = MC_state_new(); + simgrid::mc::State* initial_state = MC_state_new(); XBT_DEBUG("**************************************************"); XBT_DEBUG("Initial state"); diff --git a/src/mc/mc_comm_pattern.cpp b/src/mc/mc_comm_pattern.cpp index 3c8966988c..35540c66e3 100644 --- a/src/mc/mc_comm_pattern.cpp +++ b/src/mc/mc_comm_pattern.cpp @@ -70,7 +70,7 @@ static void MC_patterns_copy(xbt_dynar_t dest, xbt_dynar_t source) } } -void MC_restore_communications_pattern(mc_state_t state) +void MC_restore_communications_pattern(simgrid::mc::State* state) { mc_list_comm_pattern_t list_process_comm; unsigned int cursor; @@ -85,7 +85,7 @@ void MC_restore_communications_pattern(mc_state_t state) ); } -void MC_state_copy_incomplete_communications_pattern(mc_state_t state) +void MC_state_copy_incomplete_communications_pattern(simgrid::mc::State* state) { state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp); @@ -96,7 +96,7 @@ void MC_state_copy_incomplete_communications_pattern(mc_state_t state) } } -void MC_state_copy_index_communications_pattern(mc_state_t state) +void MC_state_copy_index_communications_pattern(simgrid::mc::State* state) { state->index_comm = xbt_dynar_new(sizeof(unsigned int), nullptr); mc_list_comm_pattern_t list_process_comm; diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h index 926e9337b9..0360f2da7e 100644 --- a/src/mc/mc_comm_pattern.h +++ b/src/mc/mc_comm_pattern.h @@ -91,13 +91,13 @@ XBT_PRIVATE void MC_comm_pattern_free_voidp(void *p); XBT_PRIVATE void MC_list_comm_pattern_free_voidp(void *p); XBT_PRIVATE void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking); -XBT_PRIVATE void MC_restore_communications_pattern(mc_state_t state); +XBT_PRIVATE void MC_restore_communications_pattern(simgrid::mc::State* state); XBT_PRIVATE mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm); XBT_PRIVATE xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t state); -XBT_PRIVATE void MC_state_copy_incomplete_communications_pattern(mc_state_t state); -XBT_PRIVATE void MC_state_copy_index_communications_pattern(mc_state_t state); +XBT_PRIVATE void MC_state_copy_incomplete_communications_pattern(simgrid::mc::State* state); +XBT_PRIVATE void MC_state_copy_index_communications_pattern(simgrid::mc::State* state); XBT_PRIVATE void MC_comm_pattern_free(mc_comm_pattern_t p); diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 73aefe7f37..7731b41380 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -57,7 +57,7 @@ std::vector processes_time; int user_max_depth_reached = 0; /* MC global data structures */ -mc_state_t mc_current_state = nullptr; +simgrid::mc::State* mc_current_state = nullptr; char mc_replay_mode = false; mc_stats_t mc_stats = nullptr; @@ -122,14 +122,14 @@ void MC_replay(xbt_fifo_t stack) char *req_str; smx_simcall_t req = nullptr, saved_req = NULL; xbt_fifo_item_t item, start_item; - mc_state_t state; + simgrid::mc::State* state; XBT_DEBUG("**** Begin Replay ****"); /* Intermediate backtracking */ if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) { start_item = xbt_fifo_get_first_item(stack); - state = (mc_state_t)xbt_fifo_get_item_content(start_item); + state = (simgrid::mc::State*)xbt_fifo_get_item_content(start_item); if(state->system_state){ simgrid::mc::restore_snapshot(state->system_state); if(_sg_mc_comms_determinism || _sg_mc_send_determinism) @@ -162,7 +162,7 @@ void MC_replay(xbt_fifo_t stack) item != xbt_fifo_get_first_item(stack); item = xbt_fifo_get_prev_item(item)) { - state = (mc_state_t) xbt_fifo_get_item_content(item); + state = (simgrid::mc::State*) xbt_fifo_get_item_content(item); saved_req = MC_state_get_executed_request(state, &value); if (saved_req) { diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 28f7dfb844..556eaecb3b 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -67,7 +67,7 @@ XBT_PRIVATE extern int user_max_depth_reached; XBT_PRIVATE void MC_replay(xbt_fifo_t stack); XBT_PRIVATE void MC_show_deadlock(void); -/** Stack (of `mc_state_t`) representing the current position of the +/** Stack (of `simgrid::mc::State*`) representing the current position of the * the MC in the exploration graph * * It is managed by its head (`xbt_fifo_shift` and `xbt_fifo_unshift`). diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h index 688134a786..0214389ea8 100644 --- a/src/mc/mc_safety.h +++ b/src/mc/mc_safety.h @@ -43,7 +43,7 @@ struct XBT_PRIVATE VisitedState { }; extern XBT_PRIVATE std::vector> visited_states; -XBT_PRIVATE std::unique_ptr is_visited_state(mc_state_t graph_state, bool compare_snpashots); +XBT_PRIVATE std::unique_ptr is_visited_state(simgrid::mc::State* graph_state, bool compare_snpashots); } } diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index fdb9e10009..be66f53e7b 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -22,21 +22,19 @@ using simgrid::mc::remote; XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc, "Logging specific to MC (state)"); -extern "C" { - /** * \brief Creates a state data structure used by the exploration algorithm */ -mc_state_t MC_state_new() +simgrid::mc::State* MC_state_new() { - mc_state_t state = xbt_new0(s_mc_state_t, 1); + simgrid::mc::State* state = new simgrid::mc::State(); + std::memset(&state->internal_comm, 0, sizeof(state->internal_comm)); + std::memset(&state->internal_req, 0, sizeof(state->internal_req)); + std::memset(&state->executed_req, 0, sizeof(state->executed_req)); state->max_pid = MC_smx_get_maxpid(); state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid); - state->system_state = nullptr; state->num = ++mc_stats->expanded_states; - state->in_visited_states = 0; - state->incomplete_comm_pattern = nullptr; /* Stateful model checking */ if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) || _sg_mc_termination){ state->system_state = simgrid::mc::take_snapshot(state->num); @@ -48,35 +46,51 @@ mc_state_t MC_state_new() return state; } +namespace simgrid { +namespace mc { + +State::State() +{ + std::memset(&this->internal_comm, 0, sizeof(this->internal_comm)); + std::memset(&this->internal_req, 0, sizeof(this->internal_req)); + std::memset(&this->executed_req, 0, sizeof(this->executed_req)); +} + +State::~State() +{ + xbt_free(this->index_comm); + xbt_free(this->incomplete_comm_pattern); + xbt_free(this->proc_status); +} + +} +} + /** * \brief Deletes a state data structure * \param trans The state to be deleted */ -void MC_state_delete(mc_state_t state, int free_snapshot){ +void MC_state_delete(simgrid::mc::State* state, int free_snapshot) +{ if (state->system_state && free_snapshot) delete state->system_state; - if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ - xbt_free(state->index_comm); - xbt_free(state->incomplete_comm_pattern); - } - xbt_free(state->proc_status); - xbt_free(state); + delete state; } -void MC_state_interleave_process(mc_state_t state, smx_process_t process) +void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t process) { assert(state); state->proc_status[process->pid].state = MC_INTERLEAVE; state->proc_status[process->pid].interleave_count = 0; } -void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process) +void MC_state_remove_interleave_process(simgrid::mc::State* state, smx_process_t process) { if (state->proc_status[process->pid].state == MC_INTERLEAVE) state->proc_status[process->pid].state = MC_DONE; } -unsigned int MC_state_interleave_size(mc_state_t state) +unsigned int MC_state_interleave_size(simgrid::mc::State* state) { unsigned int i, size = 0; for (i = 0; i < state->max_pid; i++) @@ -86,12 +100,12 @@ unsigned int MC_state_interleave_size(mc_state_t state) return size; } -int MC_state_process_is_done(mc_state_t state, smx_process_t process) +int MC_state_process_is_done(simgrid::mc::State* state, smx_process_t process) { return state->proc_status[process->pid].state == MC_DONE ? TRUE : FALSE; } -void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, +void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req, int value) { state->executed_req = *req; @@ -167,19 +181,19 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, } } -smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value) +smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value) { *value = state->req_num; return &state->executed_req; } -smx_simcall_t MC_state_get_internal_request(mc_state_t state) +smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state) { return &state->internal_req; } static inline smx_simcall_t MC_state_get_request_for_process( - mc_state_t state, int*value, smx_process_t process) + simgrid::mc::State* state, int*value, smx_process_t process) { mc_procstate_t procstate = &state->proc_status[process->pid]; @@ -268,7 +282,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( return nullptr; } -smx_simcall_t MC_state_get_request(mc_state_t state, int *value) +smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value) { for (auto& p : mc_model_checker->process().simix_processes()) { smx_simcall_t res = MC_state_get_request_for_process(state, value, &p.copy); @@ -277,5 +291,3 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value) } return nullptr; } - -} diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 292d15ceb2..f6079963bb 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -14,8 +14,6 @@ #include "src/simix/smx_private.h" #include "src/mc/mc_snapshot.h" -SG_BEGIN_DECL() - extern XBT_PRIVATE mc_global_t initial_global_state; /* Possible exploration status of a process in a state */ @@ -33,39 +31,46 @@ typedef struct mc_procstate{ interleaved */ } s_mc_procstate_t, *mc_procstate_t; +namespace simgrid { +namespace mc { + /* An exploration state. * * The `executed_state` is sometimes transformed into another `internal_req`. * For example WAITANY is transformes into a WAIT and TESTANY into TEST. * See `MC_state_set_executed_request()`. */ -typedef struct XBT_PRIVATE mc_state { - unsigned long max_pid; /* Maximum pid at state's creation time */ - mc_procstate_t proc_status; /* State's exploration status by process */ +struct XBT_PRIVATE State { + unsigned long max_pid = 0; /* Maximum pid at state's creation time */ + mc_procstate_t proc_status = 0; /* State's exploration status by process */ s_smx_synchro_t internal_comm; /* To be referenced by the internal_req */ s_smx_simcall_t internal_req; /* Internal translation of request */ s_smx_simcall_t executed_req; /* The executed request of the state */ - int req_num; /* The request number (in the case of a + int req_num = 0; /* The request number (in the case of a multi-request like waitany ) */ - simgrid::mc::Snapshot* system_state; /* Snapshot of system state */ - int num; - int in_visited_states; + simgrid::mc::Snapshot* system_state = 0; /* Snapshot of system state */ + int num = 0; + int in_visited_states = 0; // comm determinism verification (xbt_dynar_t): - xbt_dynar_t incomplete_comm_pattern; - xbt_dynar_t index_comm; // comm determinism verification -} s_mc_state_t, *mc_state_t; + xbt_dynar_t incomplete_comm_pattern = nullptr; + xbt_dynar_t index_comm = nullptr; // comm determinism verification + + State(); + ~State(); +}; -XBT_PRIVATE mc_state_t MC_state_new(void); -XBT_PRIVATE void MC_state_delete(mc_state_t state, int free_snapshot); -XBT_PRIVATE void MC_state_interleave_process(mc_state_t state, smx_process_t process); -XBT_PRIVATE unsigned int MC_state_interleave_size(mc_state_t state); -XBT_PRIVATE int MC_state_process_is_done(mc_state_t state, smx_process_t process); -XBT_PRIVATE void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int value); -XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value); -XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(mc_state_t state); -XBT_PRIVATE smx_simcall_t MC_state_get_request(mc_state_t state, int *value); -XBT_PRIVATE void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process); +} +} -SG_END_DECL() +XBT_PRIVATE simgrid::mc::State* MC_state_new(void); +XBT_PRIVATE void MC_state_delete(simgrid::mc::State* state, int free_snapshot); +XBT_PRIVATE void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t process); +XBT_PRIVATE unsigned int MC_state_interleave_size(simgrid::mc::State* state); +XBT_PRIVATE int MC_state_process_is_done(simgrid::mc::State* state, smx_process_t process); +XBT_PRIVATE void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req, int value); +XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value); +XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state); +XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value); +XBT_PRIVATE void MC_state_remove_interleave_process(simgrid::mc::State* state, smx_process_t process); #endif diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp index 60a1ba20a7..564a24053f 100644 --- a/src/mc/mc_visited.cpp +++ b/src/mc/mc_visited.cpp @@ -35,8 +35,8 @@ std::vector> visited_states; static int is_exploration_stack_state(simgrid::mc::VisitedState* state){ 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; + if (((simgrid::mc::State*)xbt_fifo_get_item_content(item))->num == state->num){ + ((simgrid::mc::State*)xbt_fifo_get_item_content(item))->in_visited_states = 0; return 1; } item = xbt_fifo_get_next_item(item); @@ -96,7 +96,7 @@ static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::Visi /** * \brief Checks whether a given state has already been visited by the algorithm. */ -std::unique_ptr is_visited_state(mc_state_t graph_state, bool compare_snpashots) +std::unique_ptr is_visited_state(simgrid::mc::State* graph_state, bool compare_snpashots) { -- 2.20.1