#include "msg/msg.h"
#include "mc/mc.h"
#include "xbt/automaton.h"
-#include "xbt/automatonparse_promela.h"
#include "bugged2_liveness.h"
-#include "y.tab.c"
XBT_LOG_NEW_DEFAULT_CATEGORY(bugged2_liveness, "my log messages");
const char *mess = "message";
pready = 1;
+ XBT_INFO("pready = 1");
/* CS request */
XBT_INFO("Producer ask the request");
buffer = strdup(mess);
produce = 1;
+ XBT_INFO("produce = 1");
/* CS release */
MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
produce = 0;
pready = 0;
+ XBT_INFO("pready et produce = 0");
+
}
return 0;
MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
cready = 1;
+ XBT_INFO("cready = 1");
/* Wait the answer */
m_task_t grant = NULL;
mess = strdup(buffer);
buffer[0] = '\0';
- /* Display message */
+ /* Display message */
XBT_INFO("Message : %s", mess);
- if(strcmp(mess, "") != 0)
+ if(strcmp(mess, "") != 0){
consume = 1;
+ XBT_INFO("consume = 1");
+ }
/* CS release */
MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
consume = 0;
cready = 0;
+ XBT_INFO("cready et consume = 0");
+
}
return 0;
buffer = malloc(8*sizeof(char));
buffer[0]='\0';
- init();
- yyparse();
- automaton = get_automaton();
- xbt_new_propositional_symbol(automaton,"pready", &predPready);
- xbt_new_propositional_symbol(automaton,"cready", &predCready);
- xbt_new_propositional_symbol(automaton,"consume", &predConsume);
- xbt_new_propositional_symbol(automaton,"produce", &predProduce);
+ xbt_automaton_t a = MC_create_automaton("promela2_bugged2_liveness");
+ xbt_new_propositional_symbol(a,"pready", &predPready);
+ xbt_new_propositional_symbol(a,"cready", &predCready);
+ xbt_new_propositional_symbol(a,"consume", &predConsume);
+ xbt_new_propositional_symbol(a,"produce", &predProduce);
MSG_global_init(&argc, argv);
MSG_create_environment("../msg_platform.xml");
MSG_function_register("consumer", consumer);
MSG_function_register("producer", producer);
MSG_launch_application("deploy_bugged2_liveness.xml");
- MSG_main_liveness(automaton, argv[0]);
+ MSG_main_liveness(a);
return 0;