/***************** Producer/Consumer Algorithm *************************/
/* This example implements a producer/consumer algorithm. */
/* If consumer work before producer, message is empty */
-/* LTL property checked : GF((pready U produce) -> (cready U consume)) */
-/* (pready = producer got CS, produce=message pushed in the buffer) */
-/* (cready = consumer got CS, consume=message display by consumer) */
/***********************************************************************/
#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(example_liveness_with_cycle, "my log messages");
+XBT_LOG_NEW_DEFAULT_CATEGORY(bugged2_liveness, "my log messages");
char* buffer;
char * my_mailbox = bprintf("%s", argv[1]);
- //while(1) {
+ while(1) {
/* Create message */
const char *mess = "message";
+
+ pready = 1;
+ XBT_INFO("pready = 1");
/* CS request */
XBT_INFO("Producer ask the request");
MSG_task_receive(&grant, my_mailbox);
MSG_task_destroy(grant);
- pready = 1;
-
/* Push message (size of buffer = 1) */
buffer = strdup(mess);
+ produce = 1;
+ XBT_INFO("produce = 1");
+
/* CS release */
MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
- produce = 1;
+ produce = 0;
pready = 0;
- //produce = 0;
- //pready = 0;
+ XBT_INFO("pready et produce = 0");
- //}
+ }
return 0;
char *mess;
- //while(1) {
+ while(1) {
/* CS request */
XBT_INFO("Consumer ask the request");
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;
MSG_task_receive(&grant, my_mailbox);
MSG_task_destroy(grant);
- cready = 1;
-
/* Pop message */
mess = malloc(8*sizeof(char));
mess = strdup(buffer);
buffer[0] = '\0';
- /* CS release */
- MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
-
/* Display message */
XBT_INFO("Message : %s", mess);
- if(strcmp(mess, "") != 0)
+ if(strcmp(mess, "") != 0){
consume = 1;
+ XBT_INFO("consume = 1");
+ }
- cready = 0;
+ /* CS release */
+ MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
free(mess);
- //consume = 0;
- //cready = 0;
+ 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;