Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : examples updated with new lex and yacc parsing
[simgrid.git] / examples / msg / mc / bugged2_liveness.c
1 /***************** Producer/Consumer Algorithm *************************/
2 /* This example implements a producer/consumer algorithm.              */
3 /* If consumer work before producer, message is empty                  */
4 /***********************************************************************/
5
6
7 #include "msg/msg.h"
8 #include "mc/mc.h"
9 #include "xbt/automaton.h"
10 #include "bugged2_liveness.h"
11
12 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged2_liveness, "my log messages");
13
14 char* buffer;
15
16 int consume = 0;
17 int produce = 0;
18 int cready = 0;
19 int pready = 0;
20
21 int predPready(){
22   return pready;
23 }
24
25 int predCready(){
26   return cready;
27 }
28
29 int predConsume(){
30   return consume;
31 }
32
33 int predProduce(){
34   return produce;
35 }
36
37 int coordinator(int argc, char *argv[])
38 {
39   xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
40   int CS_used = 0;
41
42   while(1) {
43     m_task_t task = 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);
48       if (CS_used) {
49         XBT_INFO("CS already used. Queue the request");
50         xbt_dynar_push(requests, &req);
51       } else {
52         m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
53         MSG_task_send(answer, req);
54         CS_used = 1;
55         XBT_INFO("CS idle. Grant immediatly");
56       }
57     } else {
58       if (xbt_dynar_length(requests) > 0) {
59         XBT_INFO("CS release. Grant to queued requests");
60         char *req;
61         xbt_dynar_pop(requests, &req);
62         MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
63       } else {
64         XBT_INFO("CS_realase, ressource now idle");
65         CS_used = 0;
66       }
67     }
68
69     MSG_task_destroy(task);
70
71   }
72
73   return 0;
74
75 }
76
77 int producer(int argc, char *argv[])
78 {
79
80   char * my_mailbox = bprintf("%s", argv[1]);
81   
82   while(1) {
83     
84     /* Create message */
85     const char *mess = "message";
86
87     pready = 1;
88     XBT_INFO("pready = 1");
89     
90     /* CS request */
91     XBT_INFO("Producer ask the request");
92     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
93
94     /* Wait the answer */
95     m_task_t grant = NULL;
96     MSG_task_receive(&grant, my_mailbox);
97     MSG_task_destroy(grant);
98
99     /* Push message (size of buffer = 1) */
100     buffer = strdup(mess);
101
102     produce = 1;
103     XBT_INFO("produce = 1");
104
105     /* CS release */
106     MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
107
108     produce = 0;
109     pready = 0;
110
111     XBT_INFO("pready et produce = 0");
112
113   }
114
115   return 0;
116
117 }
118
119 int consumer(int argc, char *argv[])
120 {
121
122   char * my_mailbox = bprintf("%s", argv[1]);
123   char *mess;
124
125
126   while(1) {
127     
128     /* CS request */
129     XBT_INFO("Consumer ask the request");
130     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
131
132     cready = 1;
133     XBT_INFO("cready = 1");
134
135     /* Wait the answer */
136     m_task_t grant = NULL;
137     MSG_task_receive(&grant, my_mailbox);
138     MSG_task_destroy(grant);
139
140     /* Pop message  */
141     mess = malloc(8*sizeof(char));
142     mess = strdup(buffer);
143     buffer[0] = '\0'; 
144
145     /* Display message */
146     XBT_INFO("Message : %s", mess);
147     if(strcmp(mess, "") != 0){
148       consume = 1;
149       XBT_INFO("consume = 1");
150     }
151
152     /* CS release */
153     MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
154
155     free(mess);
156
157     consume = 0;
158     cready = 0;
159
160     XBT_INFO("cready et consume = 0");
161
162   }
163
164   return 0;
165
166 }
167
168
169 int main(int argc, char *argv[])
170 {
171
172   buffer = malloc(8*sizeof(char));
173   buffer[0]='\0';
174
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); 
180   
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);
188
189   return 0;
190
191 }