X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b08e93079ce626559903d763ea5c79d3de220a24..fea2606dff029fec63088d8e3d9f42925a67efea:/src/mc/mc_state.cpp diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index 208187ed24..3720ff795d 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2014. The SimGrid Team. +/* Copyright (c) 2008-2015. The SimGrid Team. * All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it @@ -6,14 +6,14 @@ #include -#include "../simix/smx_private.h" +#include "src/simix/smx_private.h" #include "xbt/fifo.h" -#include "mc_state.h" -#include "mc_request.h" -#include "mc_private.h" -#include "mc_comm_pattern.h" -#include "mc_smx.h" -#include "mc_xbt.hpp" +#include "src/mc/mc_state.h" +#include "src/mc/mc_request.h" +#include "src/mc/mc_private.h" +#include "src/mc/mc_comm_pattern.h" +#include "src/mc/mc_smx.h" +#include "src/mc/mc_xbt.hpp" using simgrid::mc::remote; @@ -37,7 +37,7 @@ mc_state_t MC_state_new() state->incomplete_comm_pattern = NULL; /* Stateful model checking */ if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) || _sg_mc_termination){ - state->system_state = MC_take_snapshot(state->num); + state->system_state = simgrid::mc::take_snapshot(state->num); if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ MC_state_copy_incomplete_communications_pattern(state); MC_state_copy_index_communications_pattern(state); @@ -105,24 +105,30 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, * corresponding communication action so it can be treated later by the dependence * function. */ switch (req->call) { - case SIMCALL_COMM_WAITANY: + case SIMCALL_COMM_WAITANY: { state->internal_req.call = SIMCALL_COMM_WAIT; state->internal_req.issuer = req->issuer; + smx_synchro_t remote_comm; read_element(mc_model_checker->process(), - &state->internal_comm, remote(simcall_comm_waitany__get__comms(req)), - value, sizeof(state->internal_comm)); + &remote_comm, remote(simcall_comm_waitany__get__comms(req)), + value, sizeof(remote_comm)); + mc_model_checker->process().read(&state->internal_comm, remote(remote_comm)); simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm); simcall_comm_wait__set__timeout(&state->internal_req, 0); break; + } case SIMCALL_COMM_TESTANY: state->internal_req.call = SIMCALL_COMM_TEST; state->internal_req.issuer = req->issuer; - if (value > 0) - read_element(mc_model_checker->process(), - &state->internal_comm, remote(simcall_comm_testany__get__comms(req)), - value, sizeof(state->internal_comm)); + if (value > 0) { + smx_synchro_t remote_comm; + read_element(mc_model_checker->process(), + &remote_comm, remote(simcall_comm_testany__get__comms(req)), + value, sizeof(remote_comm)); + mc_model_checker->process().read(&state->internal_comm, remote(remote_comm)); + } simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm); simcall_comm_test__set__result(&state->internal_req, value);