X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/324ed35d0489e7df64745a022a3d426ff227fba2..2b1e59493dcd4f1709b1228c673364ef7facc6e5:/examples/msg/mc/centralized_liveness_deadlock.c diff --git a/examples/msg/mc/centralized_liveness_deadlock.c b/examples/msg/mc/centralized_liveness_deadlock.c index ba050d64c3..3c02d517a2 100644 --- a/examples/msg/mc/centralized_liveness_deadlock.c +++ b/examples/msg/mc/centralized_liveness_deadlock.c @@ -1,14 +1,12 @@ /***************** Centralized Mutual Exclusion Algorithm *********************/ /* This example implements a centralized mutual exclusion algorithm. */ -/* LTL property checked : !(GFcs) */ +/* LTL property checked : !(GFcs) */ /******************************************************************************/ #include "msg/msg.h" #include "mc/mc.h" #include "xbt/automaton.h" -#include "xbt/automatonparse_promela.h" #include "centralized_liveness.h" -#include "y.tab.c" XBT_LOG_NEW_DEFAULT_CATEGORY(centralized, "my log messages"); @@ -97,17 +95,16 @@ int client(int argc, char *argv[]) int main(int argc, char *argv[]) { - init(); - yyparse(); - automaton = get_automaton(); - xbt_new_propositional_symbol(automaton,"cs", &predCS); + + xbt_automaton_t a = MC_create_automaton("promela_centralized_liveness"); + xbt_new_propositional_symbol(a,"cs", &predCS); - MSG_global_init(&argc, argv); + MSG_init(&argc, argv); MSG_create_environment("../msg_platform.xml"); MSG_function_register("coordinator", coordinator); MSG_function_register("client", client); MSG_launch_application("deploy_centralized_liveness.xml"); - MSG_main_liveness(automaton); + MSG_main_liveness(a); return 0;