Logo AND Algorithmique Numérique Distribuée

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