1 /***************** Producer/Consumer Algorithm *************************/
2 /* This example implements a producer/consumer algorithm. */
3 /* If consumer work before producer, message is empty */
4 /* LTL property checked : GF((pready U produce) -> (cready U consume)) */
5 /* (pready = producer got CS, produce=message pushed in the buffer) */
6 /* (cready = consumer got CS, consume=message display by consumer) */
7 /***********************************************************************/
12 #include "xbt/automaton.h"
13 #include "xbt/automatonparse_promela.h"
14 #include "bugged2_liveness.h"
17 XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages");
42 int coordinator(int argc, char *argv[])
44 xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
49 MSG_task_receive(&task, "coordinator");
50 const char *kind = MSG_task_get_name(task);
51 if (!strcmp(kind, "request")) {
52 char *req = MSG_task_get_data(task);
54 XBT_INFO("CS already used. Queue the request");
55 xbt_dynar_push(requests, &req);
57 m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
58 MSG_task_send(answer, req);
60 XBT_INFO("CS idle. Grant immediatly");
63 if (xbt_dynar_length(requests) > 0) {
64 XBT_INFO("CS release. Grant to queued requests");
66 xbt_dynar_pop(requests, &req);
67 MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
69 XBT_INFO("CS_realase, ressource now idle");
74 MSG_task_destroy(task);
82 int producer(int argc, char *argv[])
85 char * my_mailbox = bprintf("%s", argv[1]);
90 const char *mess = "message";
93 XBT_INFO("Producer ask the request");
94 MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
97 m_task_t grant = NULL;
98 MSG_task_receive(&grant, my_mailbox);
99 MSG_task_destroy(grant);
103 /* Push message (size of buffer = 1) */
104 buffer = strdup(mess);
107 MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
121 int consumer(int argc, char *argv[])
124 char * my_mailbox = bprintf("%s", argv[1]);
131 XBT_INFO("Consumer ask the request");
132 MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
134 /* Wait the answer */
135 m_task_t grant = NULL;
136 MSG_task_receive(&grant, my_mailbox);
137 MSG_task_destroy(grant);
142 mess = malloc(8*sizeof(char));
143 mess = strdup(buffer);
147 MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
149 /* Display message */
150 XBT_INFO("Message : %s", mess);
151 if(strcmp(mess, "") != 0)
168 int main(int argc, char *argv[])
171 buffer = malloc(8*sizeof(char));
176 automaton = get_automaton();
177 xbt_new_propositional_symbol(automaton,"pready", &predPready);
178 xbt_new_propositional_symbol(automaton,"cready", &predCready);
179 xbt_new_propositional_symbol(automaton,"consume", &predConsume);
180 xbt_new_propositional_symbol(automaton,"produce", &predProduce);
182 MSG_global_init(&argc, argv);
183 MSG_create_environment("../msg_platform.xml");
184 MSG_function_register("coordinator", coordinator);
185 MSG_function_register("consumer", consumer);
186 MSG_function_register("producer", producer);
187 MSG_launch_application("deploy_bugged2_liveness.xml");
188 MSG_main_liveness(automaton, argv[0]);