Logo AND Algorithmique Numérique Distribuée

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