From: Marion Guthmuller Date: Mon, 30 Jan 2012 13:12:15 +0000 (+0100) Subject: model-checker : fix compilation error X-Git-Tag: exp_20120216~118 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/b7c05078f9a89dba063df2fc7edea55ae1d6a3ed?hp=c5ad8ca1a68bbaa9152471c8d0eeb99d762f0d86 model-checker : fix compilation error --- diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 68f11cd175..7760797e1a 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -4,7 +4,7 @@ #include #include "../surf/surf_private.h" -#include "../simix/private.h" +#include "../simix/smx_private.h" #include "xbt/fifo.h" #include "private.h" @@ -185,7 +185,7 @@ void MC_wait_for_requests(void) SIMIX_process_runall(); xbt_dynar_foreach(simix_global->process_that_ran, iter, process) { req = &process->simcall; - if (req->call != REQ_NO_REQ && !MC_request_is_visible(req)) + if (req->call != SIMCALL_NONE && !MC_request_is_visible(req)) SIMIX_simcall_pre(req, 0); } } @@ -198,7 +198,7 @@ int MC_deadlock_check() if(xbt_swag_size(simix_global->process_list)){ deadlock = TRUE; xbt_swag_foreach(process, simix_global->process_list){ - if(process->simcall.call != REQ_NO_REQ + if(process->simcall.call != SIMCALL_NONE && MC_request_is_enabled(&process->simcall)){ deadlock = FALSE; break; diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 00a2eb970b..75615b70f9 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -190,7 +190,7 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu xbt_fifo_item_t item1, item2; smx_action_t action1, action2; xbt_fifo_item_t item_req1, item_req2; - smx_req_t req1, req2; + smx_simcall_t req1, req2; int i=0; int j=0; @@ -225,25 +225,25 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu return 1; } - if(xbt_fifo_size(action1->request_list) != xbt_fifo_size(action2->request_list)){ - XBT_DEBUG("Different size of request list (%d - %d", xbt_fifo_size(action1->request_list), xbt_fifo_size(action2->request_list)); + if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){ + XBT_DEBUG("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls)); return 1; }else{ - item_req1 = xbt_fifo_get_first_item(action1->request_list); - item_req2 = xbt_fifo_get_first_item(action2->request_list); + item_req1 = xbt_fifo_get_first_item(action1->simcalls); + item_req2 = xbt_fifo_get_first_item(action2->simcalls); - while(jrequest_list)){ + while(jsimcalls)){ - req1 = (smx_req_t) xbt_fifo_get_item_content(item_req1); - req2 = (smx_req_t) xbt_fifo_get_item_content(item_req2); + req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1); + req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2); if(req1->call != req2->call){ - XBT_DEBUG("Different request call in request_list of action (%d - %d)", req1->call, req2->call); + XBT_DEBUG("Different simcall call in simcalls of action (%d - %d)", req1->call, req2->call); return 1; } if(req1->issuer->pid != req2->issuer->pid){ - XBT_DEBUG("Different request issuer in request_list of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid); + XBT_DEBUG("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid); return 1; } diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index 83fd8058a7..f6a70ad635 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -15,86 +15,86 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) if (r1->issuer == r2->issuer) return FALSE; - if(r1->call == REQ_COMM_ISEND && r2->call == REQ_COMM_IRECV) + if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV) return FALSE; - if(r1->call == REQ_COMM_IRECV && r2->call == REQ_COMM_ISEND) + if(r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND) return FALSE; - if( (r1->call == REQ_COMM_ISEND || r1->call == REQ_COMM_IRECV) - && r2->call == REQ_COMM_WAIT){ + if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV) + && r2->call == SIMCALL_COMM_WAIT){ if(r2->comm_wait.comm->comm.rdv == NULL) return FALSE; - smx_rdv_t rdv = r1->call == REQ_COMM_ISEND ? r1->comm_isend.rdv : r1->comm_irecv.rdv; + smx_rdv_t rdv = r1->call == SIMCALL_COMM_ISEND ? r1->comm_isend.rdv : r1->comm_irecv.rdv; if(r2->comm_wait.comm->comm.rdv != rdv) return FALSE; - if(r2->comm_wait.comm->comm.type == SIMIX_COMM_SEND && r1->call == REQ_COMM_ISEND) + if(r2->comm_wait.comm->comm.type == SIMIX_COMM_SEND && r1->call == SIMCALL_COMM_ISEND) return FALSE; - if(r2->comm_wait.comm->comm.type == SIMIX_COMM_RECEIVE && r1->call == REQ_COMM_IRECV) + if(r2->comm_wait.comm->comm.type == SIMIX_COMM_RECEIVE && r1->call == SIMCALL_COMM_IRECV) return FALSE; } - if( (r2->call == REQ_COMM_ISEND || r2->call == REQ_COMM_IRECV) - && r1->call == REQ_COMM_WAIT){ + if( (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV) + && r1->call == SIMCALL_COMM_WAIT){ if(r1->comm_wait.comm->comm.rdv != NULL) return FALSE; - smx_rdv_t rdv = r2->call == REQ_COMM_ISEND ? r2->comm_isend.rdv : r2->comm_irecv.rdv; + smx_rdv_t rdv = r2->call == SIMCALL_COMM_ISEND ? r2->comm_isend.rdv : r2->comm_irecv.rdv; if(r1->comm_wait.comm->comm.rdv != rdv) return FALSE; - if(r1->comm_wait.comm->comm.type == SIMIX_COMM_SEND && r2->call == REQ_COMM_ISEND) + if(r1->comm_wait.comm->comm.type == SIMIX_COMM_SEND && r2->call == SIMCALL_COMM_ISEND) return FALSE; - if(r1->comm_wait.comm->comm.type == SIMIX_COMM_RECEIVE && r2->call == REQ_COMM_IRECV) + if(r1->comm_wait.comm->comm.type == SIMIX_COMM_RECEIVE && r2->call == SIMCALL_COMM_IRECV) return FALSE; } /* FIXME: the following rule assumes that the result of the * isend/irecv call is not stored in a buffer used in the * test call. */ - if( (r1->call == REQ_COMM_ISEND || r1->call == REQ_COMM_IRECV) - && r2->call == REQ_COMM_TEST) + if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV) + && r2->call == SIMCALL_COMM_TEST) return FALSE; /* FIXME: the following rule assumes that the result of the * isend/irecv call is not stored in a buffer used in the * test call.*/ - if( (r2->call == REQ_COMM_ISEND || r2->call == REQ_COMM_IRECV) - && r1->call == REQ_COMM_TEST) + if( (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV) + && r1->call == SIMCALL_COMM_TEST) return FALSE; - if(r1->call == REQ_COMM_ISEND && r2->call == REQ_COMM_ISEND + if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_ISEND && r1->comm_isend.rdv != r2->comm_isend.rdv) return FALSE; - if(r1->call == REQ_COMM_IRECV && r2->call == REQ_COMM_IRECV + if(r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_IRECV && r1->comm_irecv.rdv != r2->comm_irecv.rdv) return FALSE; - if(r1->call == REQ_COMM_WAIT && (r2->call == REQ_COMM_WAIT || r2->call == REQ_COMM_TEST) + if(r1->call == SIMCALL_COMM_WAIT && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST) && (r1->comm_wait.comm->comm.src_proc == NULL || r1->comm_wait.comm->comm.dst_proc == NULL)) return FALSE; - if(r2->call == REQ_COMM_WAIT && (r1->call == REQ_COMM_WAIT || r1->call == REQ_COMM_TEST) + if(r2->call == SIMCALL_COMM_WAIT && (r1->call == SIMCALL_COMM_WAIT || r1->call == SIMCALL_COMM_TEST) && (r2->comm_wait.comm->comm.src_proc == NULL || r2->comm_wait.comm->comm.dst_proc == NULL)) return FALSE; - if(r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_WAIT + if(r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT && r1->comm_wait.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff && r1->comm_wait.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff) return FALSE; - if (r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_WAIT + if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT && r1->comm_wait.comm->comm.src_buff != NULL && r1->comm_wait.comm->comm.dst_buff != NULL && r2->comm_wait.comm->comm.src_buff != NULL @@ -104,29 +104,29 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) && r2->comm_wait.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff) return FALSE; - if(r1->call == REQ_COMM_TEST && + if(r1->call == SIMCALL_COMM_TEST && (r1->comm_test.comm == NULL || r1->comm_test.comm->comm.src_buff == NULL || r1->comm_test.comm->comm.dst_buff == NULL)) return FALSE; - if(r2->call == REQ_COMM_TEST && + if(r2->call == SIMCALL_COMM_TEST && (r2->comm_test.comm == NULL || r2->comm_test.comm->comm.src_buff == NULL || r2->comm_test.comm->comm.dst_buff == NULL)) return FALSE; - if(r1->call == REQ_COMM_TEST && r2->call == REQ_COMM_WAIT + if(r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT && r1->comm_test.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff && r1->comm_test.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff) return FALSE; - if(r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_TEST + if(r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST && r1->comm_wait.comm->comm.src_buff == r2->comm_test.comm->comm.src_buff && r1->comm_wait.comm->comm.dst_buff == r2->comm_test.comm->comm.dst_buff) return FALSE; - if (r1->call == REQ_COMM_WAIT && r2->call == REQ_COMM_TEST + if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST && r1->comm_wait.comm->comm.src_buff != NULL && r1->comm_wait.comm->comm.dst_buff != NULL && r2->comm_test.comm->comm.src_buff != NULL @@ -136,7 +136,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) && r2->comm_test.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff) return FALSE; - if (r1->call == REQ_COMM_TEST && r2->call == REQ_COMM_WAIT + if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT && r1->comm_test.comm->comm.src_buff != NULL && r1->comm_test.comm->comm.dst_buff != NULL && r2->comm_wait.comm->comm.src_buff != NULL @@ -174,20 +174,20 @@ char *MC_request_to_string(smx_simcall_t req, int value) size_t size = 0; switch(req->call){ - case REQ_COMM_ISEND: + case SIMCALL_COMM_ISEND: type = xbt_strdup("iSend"); p = pointer_to_string(req->comm_isend.src_buff); bs = buff_size_to_string(req->comm_isend.src_buff_size); args = bprintf("src=%s, buff=%s, size=%s", req->issuer->name, p, bs); break; - case REQ_COMM_IRECV: + case SIMCALL_COMM_IRECV: size = req->comm_irecv.dst_buff_size ? *req->comm_irecv.dst_buff_size : 0; type = xbt_strdup("iRecv"); p = pointer_to_string(req->comm_irecv.dst_buff); bs = buff_size_to_string(size); args = bprintf("dst=%s, buff=%s, size=%s", req->issuer->name, p, bs); break; - case REQ_COMM_WAIT: + case SIMCALL_COMM_WAIT: act = req->comm_wait.comm; if(value == -1){ type = xbt_strdup("WaitTimeout"); @@ -203,7 +203,7 @@ char *MC_request_to_string(smx_simcall_t req, int value) act->comm.dst_proc ? act->comm.dst_proc->name : ""); } break; - case REQ_COMM_TEST: + case SIMCALL_COMM_TEST: act = req->comm_test.comm; if(act->comm.src_proc == NULL || act->comm.dst_proc == NULL){ type = xbt_strdup("Test FALSE"); @@ -218,14 +218,14 @@ char *MC_request_to_string(smx_simcall_t req, int value) } break; - case REQ_COMM_WAITANY: + case SIMCALL_COMM_WAITANY: type = xbt_strdup("WaitAny"); p = pointer_to_string(xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t)); args = bprintf("comm=%s (%d of %lu)", p, value+1, xbt_dynar_length(req->comm_waitany.comms)); break; - case REQ_COMM_TESTANY: + case SIMCALL_COMM_TESTANY: if(value == -1){ type = xbt_strdup("TestAny FALSE"); args = xbt_strdup("-"); @@ -262,12 +262,12 @@ unsigned int MC_request_testany_fail(smx_simcall_t req) int MC_request_is_visible(smx_simcall_t req) { - return req->call == REQ_COMM_ISEND - || req->call == REQ_COMM_IRECV - || req->call == REQ_COMM_WAIT - || req->call == REQ_COMM_WAITANY - || req->call == REQ_COMM_TEST - || req->call == REQ_COMM_TESTANY; + return req->call == SIMCALL_COMM_ISEND + || req->call == SIMCALL_COMM_IRECV + || req->call == SIMCALL_COMM_WAIT + || req->call == SIMCALL_COMM_WAITANY + || req->call == SIMCALL_COMM_TEST + || req->call == SIMCALL_COMM_TESTANY; } int MC_request_is_enabled(smx_simcall_t req) @@ -277,7 +277,7 @@ int MC_request_is_enabled(smx_simcall_t req) switch (req->call) { - case REQ_COMM_WAIT: + case SIMCALL_COMM_WAIT: /* FIXME: check also that src and dst processes are not suspended */ /* If it has a timeout it will be always be enabled, because even if the @@ -291,7 +291,7 @@ int MC_request_is_enabled(smx_simcall_t req) } break; - case REQ_COMM_WAITANY: + case SIMCALL_COMM_WAITANY: /* Check if it has at least one communication ready */ xbt_dynar_foreach(req->comm_waitany.comms, index, act) { if (act->comm.src_proc && act->comm.dst_proc){ @@ -313,18 +313,18 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) switch (req->call) { - case REQ_COMM_WAIT: + case SIMCALL_COMM_WAIT: /* FIXME: check also that src and dst processes are not suspended */ act = req->comm_wait.comm; return (act->comm.src_proc && act->comm.dst_proc); break; - case REQ_COMM_WAITANY: + case SIMCALL_COMM_WAITANY: act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t); return (act->comm.src_proc && act->comm.dst_proc); break; - case REQ_COMM_TESTANY: + case SIMCALL_COMM_TESTANY: act = xbt_dynar_get_as(req->comm_testany.comms, idx, smx_action_t); return (act->comm.src_proc && act->comm.dst_proc); break; @@ -336,7 +336,7 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) int MC_process_is_enabled(smx_process_t process) { - if (process->simcall.call != REQ_NO_REQ && MC_request_is_enabled(&process->simcall)) + if (process->simcall.call != SIMCALL_NONE && MC_request_is_enabled(&process->simcall)) return TRUE; return FALSE; diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index d8604de9b6..ad66b618e3 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -1,6 +1,6 @@ -#include "../simix/private.h" +#include "../simix/smx_private.h" #include "xbt/fifo.h" #include "private.h" @@ -72,16 +72,16 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu * corresponding communication action so it can be treated later by the dependence * function. */ switch(req->call){ - case REQ_COMM_WAITANY: - state->internal_req.call = REQ_COMM_WAIT; + case SIMCALL_COMM_WAITANY: + state->internal_req.call = SIMCALL_COMM_WAIT; state->internal_req.issuer = req->issuer; state->internal_comm = *xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t); state->internal_req.comm_wait.comm = &state->internal_comm; state->internal_req.comm_wait.timeout = 0; break; - case REQ_COMM_TESTANY: - state->internal_req.call = REQ_COMM_TEST; + case SIMCALL_COMM_TESTANY: + state->internal_req.call = SIMCALL_COMM_TEST; state->internal_req.issuer = req->issuer; if(value > 0) @@ -91,14 +91,14 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu state->internal_req.comm_test.result = value; break; - case REQ_COMM_WAIT: + case SIMCALL_COMM_WAIT: state->internal_req = *req; state->internal_comm = *(req->comm_wait.comm); state->executed_req.comm_wait.comm = &state->internal_comm; state->internal_req.comm_wait.comm = &state->internal_comm; break; - case REQ_COMM_TEST: + case SIMCALL_COMM_TEST: state->internal_req = *req; state->internal_comm = *req->comm_test.comm; state->executed_req.comm_test.comm = &state->internal_comm; @@ -134,7 +134,7 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value) if(procstate->state == MC_INTERLEAVE){ if(MC_process_is_enabled(process)){ switch(process->simcall.call){ - case REQ_COMM_WAITANY: + case SIMCALL_COMM_WAITANY: *value = -1; while(procstate->interleave_count < xbt_dynar_length(process->simcall.comm_waitany.comms)){ if(MC_request_is_enabled_by_idx(&process->simcall, procstate->interleave_count++)){ @@ -151,7 +151,7 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value) break; - case REQ_COMM_TESTANY: + case SIMCALL_COMM_TESTANY: start_count = procstate->interleave_count; *value = -1; while(procstate->interleave_count < xbt_dynar_length(process->simcall.comm_testany.comms)){ @@ -169,7 +169,7 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value) break; - case REQ_COMM_WAIT: + case SIMCALL_COMM_WAIT: if(process->simcall.comm_wait.comm->comm.src_proc && process->simcall.comm_wait.comm->comm.dst_proc){ *value = 0; diff --git a/src/mc/private.h b/src/mc/private.h index 3c7006030e..d277c41014 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -15,7 +15,7 @@ #include "xbt/config.h" #include "xbt/function_types.h" #include "xbt/mmalloc.h" -#include "../simix/private.h" +#include "../simix/smx_private.h" #include "xbt/automaton.h" #include "xbt/hash.h" #include "msg/msg.h"