X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f28d984fb76ea5e45562168a2e67b60a8b1d0fb2..830b5c4bc694ade087c43f39015faa9065795630:/examples/msg/mc/test_snapshot.c diff --git a/examples/msg/mc/test_snapshot.c b/examples/msg/mc/test_snapshot.c index 13ca8d00fd..32b6165d2b 100644 --- a/examples/msg/mc/test_snapshot.c +++ b/examples/msg/mc/test_snapshot.c @@ -1,7 +1,6 @@ #include "msg/msg.h" #include "mc/mc.h" #include "xbt/automaton.h" -#include "xbt/automatonparse_promela.h" #include "test_snapshot.h" //#include "y.tab.c" #include @@ -54,7 +53,7 @@ int coordinator(int argc, char *argv[]) while(i>0){ - m_task_t task = NULL; + msg_task_t task = NULL; MSG_task_receive(&task, "coordinator"); const char *kind = MSG_task_get_name(task); @@ -62,7 +61,7 @@ int coordinator(int argc, char *argv[]) if (!strcmp(kind, "request")) { char *req = MSG_task_get_data(task); - m_task_t answer = MSG_task_create("received", 0, 1000, NULL); + msg_task_t answer = MSG_task_create("received", 0, 1000, NULL); MSG_task_send(answer, req); }else{ XBT_INFO("End of coordinator"); @@ -89,7 +88,7 @@ int client(int argc, char *argv[]) check(); // wait the answer - m_task_t task = NULL; + msg_task_t task = NULL; MSG_task_receive(&task, my_mailbox); MSG_task_destroy(task); @@ -121,8 +120,9 @@ int client(int argc, char *argv[]) return 0; } -int main(int argc, char *argv[]) -{ +int main(int argc, char *argv[]) { + + MSG_init(&argc, argv); d1 = xbt_dynar_new(sizeof(char *), NULL); XBT_DEBUG("Dynar d1 : %p -> %p", &d1, d1); @@ -130,18 +130,15 @@ int main(int argc, char *argv[]) xbt_dynar_push(d1, &c1); xbt_dynar_push(d1, &c1); - init(); - yyparse(); - automaton = get_automaton(); - xbt_new_propositional_symbol(automaton,"r", &predR); - xbt_new_propositional_symbol(automaton,"cs", &predCS); + MSG_config("model-check/property","promela_test_snapshot"); + MC_automaton_new_propositional_symbol("r", &predR); + MC_automaton_new_propositional_symbol("cs", &predCS); - MSG_global_init(&argc, argv); MSG_create_environment("../msg_platform.xml"); MSG_function_register("coordinator", coordinator); MSG_function_register("client", client); MSG_launch_application("deploy_test_snapshot.xml"); - MSG_main_liveness(automaton); + MSG_main(); return 0; }