1 /***************** Producer/Consumer Algorithm *************************/
2 /* This example implements a producer/consumer algorithm. */
3 /* If consumer work before producer, message is empty */
4 /***********************************************************************/
9 #include "xbt/automaton.h"
10 #include "bugged2_liveness.h"
12 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged2_liveness, "my log messages");
37 int coordinator(int argc, char *argv[])
39 xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
44 MSG_task_receive(&task, "coordinator");
45 const char *kind = MSG_task_get_name(task);
46 if (!strcmp(kind, "request")) {
47 char *req = MSG_task_get_data(task);
49 XBT_INFO("CS already used. Queue the request");
50 xbt_dynar_push(requests, &req);
52 m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
53 MSG_task_send(answer, req);
55 XBT_INFO("CS idle. Grant immediatly");
58 if (xbt_dynar_length(requests) > 0) {
59 XBT_INFO("CS release. Grant to queued requests");
61 xbt_dynar_pop(requests, &req);
62 MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
64 XBT_INFO("CS_realase, ressource now idle");
69 MSG_task_destroy(task);
77 int producer(int argc, char *argv[])
80 char * my_mailbox = bprintf("%s", argv[1]);
85 const char *mess = "message";
88 XBT_INFO("pready = 1");
91 XBT_INFO("Producer ask the request");
92 MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
95 m_task_t grant = NULL;
96 MSG_task_receive(&grant, my_mailbox);
97 MSG_task_destroy(grant);
99 /* Push message (size of buffer = 1) */
100 buffer = strdup(mess);
103 XBT_INFO("produce = 1");
106 MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
111 XBT_INFO("pready et produce = 0");
119 int consumer(int argc, char *argv[])
122 char * my_mailbox = bprintf("%s", argv[1]);
129 XBT_INFO("Consumer ask the request");
130 MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
133 XBT_INFO("cready = 1");
135 /* Wait the answer */
136 m_task_t grant = NULL;
137 MSG_task_receive(&grant, my_mailbox);
138 MSG_task_destroy(grant);
141 mess = malloc(8*sizeof(char));
142 mess = strdup(buffer);
145 /* Display message */
146 XBT_INFO("Message : %s", mess);
147 if(strcmp(mess, "") != 0){
149 XBT_INFO("consume = 1");
153 MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
160 XBT_INFO("cready et consume = 0");
169 int main(int argc, char *argv[])
172 buffer = malloc(8*sizeof(char));
175 xbt_automaton_t a = MC_create_automaton("promela2_bugged2_liveness");
176 xbt_new_propositional_symbol(a,"pready", &predPready);
177 xbt_new_propositional_symbol(a,"cready", &predCready);
178 xbt_new_propositional_symbol(a,"consume", &predConsume);
179 xbt_new_propositional_symbol(a,"produce", &predProduce);
181 MSG_global_init(&argc, argv);
182 MSG_create_environment("../msg_platform.xml");
183 MSG_function_register("coordinator", coordinator);
184 MSG_function_register("consumer", consumer);
185 MSG_function_register("producer", producer);
186 MSG_launch_application("deploy_bugged2_liveness.xml");
187 MSG_main_liveness(a);