add_executable(bugged2 bugged2.c)
add_executable(bugged3 bugged3.c)
add_executable(random_test random_test.c)
-add_executable(example_liveness_with_cycle2 automaton.c
-automatonparse_promela.c example_liveness_with_cycle2.c)
-add_executable(example_liveness_with_cycle automaton.c
-automatonparse_promela.c example_liveness_with_cycle.c)
+add_executable(bugged1_liveness automaton.c automatonparse_promela.c bugged1_liveness.c)
+add_executable(bugged2_liveness automaton.c automatonparse_promela.c bugged2_liveness.c)
target_link_libraries(bugged2 simgrid m )
target_link_libraries(bugged3 simgrid m )
target_link_libraries(random_test simgrid m )
-target_link_libraries(example_liveness_with_cycle2 simgrid m )
-target_link_libraries(example_liveness_with_cycle simgrid m )
\ No newline at end of file
+target_link_libraries(bugged1_liveness simgrid m )
+target_link_libraries(bugged2_liveness simgrid m )
+++ /dev/null
-never {
-T0_init:
- if
- :: (!d) || (r) -> goto accept_S1
- :: (1) -> goto T1_S4
- :: (1) -> goto T0_S2
- :: (!e) -> goto accept_S3
- fi;
-T1_S4:
- if
- :: (1) -> goto T1_S4
- :: (r) -> goto accept_S1
- fi;
-accept_S1:
- if
- :: (!d) || (r) -> goto accept_S1
- :: (1) -> goto T1_S4
- fi;
-T0_S2:
- if
- :: (1) -> goto T0_S2
- :: (!e) -> goto accept_S3
- fi;
-accept_S3:
- if
- :: (!e) -> goto accept_S3
- fi;
-}
/***************** Centralized Mutual Exclusion Algorithm *********************/
/* This example implements a centralized mutual exclusion algorithm. */
/* CS requests of client 2 not satisfied */
+/* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok) */
/******************************************************************************/
#include "msg/msg.h"
#include "mc/mc.h"
#include "xbt/automaton.h"
#include "xbt/automatonparse_promela.h"
-#include "example_liveness_with_cycle.h"
+#include "bugged1_liveness.h"
#include "y.tab.c"
#define AMOUNT_OF_CLIENTS 2
-#define CS_PER_PROCESS 10
+#define CS_PER_PROCESS 1
XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages");
-int p=0;
-int q=0;
+int r=0;
+int cs=0;
-int predP(){
- return p;
+int predR(){
+ return r;
}
-int predQ(){
- return q;
+int predCS(){
+ return cs;
}
MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
todo--;
}else{
- CS_used = 0;
+ xbt_dynar_pop(requests, &req);
+ MSG_task_send(MSG_task_create("notgrant", 0, 1000, NULL), req);
+ CS_used = 0;
+ todo--;
}
} else { // nobody wants it
XBT_INFO("CS release. resource now idle");
MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
if(strcmp(my_mailbox, "2") == 0){
- p = 1;
- q = 0;
- XBT_DEBUG("Propositions changed : p=1, q=0");
+ r = 1;
+ cs = 0;
+ XBT_DEBUG("Propositions changed : r=1, cs=0");
}
// wait the answer
m_task_t grant = NULL;
MSG_task_receive(&grant, my_mailbox);
+ const char *kind = MSG_task_get_name(grant);
- if(strcmp(my_mailbox, "2") == 0){
- q = 1;
- p = 0;
- XBT_DEBUG("Propositions changed : p=0, q=1");
+ if((strcmp(my_mailbox, "2") == 0) && (strcmp("grant", kind) == 0)){
+ cs = 1;
+ r = 0;
+ XBT_DEBUG("Propositions changed : r=0, cs=1");
}
MSG_process_sleep(my_pid);
if(strcmp(my_mailbox, "2") == 0){
- q=0;
- p=0;
- XBT_DEBUG("Propositions changed : p=0, q=0");
+ cs=0;
+ r=0;
+ XBT_DEBUG("Propositions changed : r=0, cs=0");
}
}
init();
yyparse();
automaton = get_automaton();
- xbt_new_propositional_symbol(automaton,"p", &predP);
- xbt_new_propositional_symbol(automaton,"q", &predQ);
+ xbt_new_propositional_symbol(automaton,"r", &predR);
+ xbt_new_propositional_symbol(automaton,"cs", &predCS);
MSG_global_init(&argc, argv);
MSG_create_environment("../msg_platform.xml");
MSG_function_register("coordinator", coordinator);
MSG_function_register("client", client);
- MSG_launch_application("deploy_mutex2.xml");
+ MSG_launch_application("deploy_bugged1_liveness.xml");
MSG_main_liveness(automaton, argv[0]);
return 0;
-#ifndef _EXAMPLE_LIVENESS_WITH_CYCLE_H
-#define _EXAMPLE_LIVENESS_WITH_CYCLE_H
+#ifndef _BUGGED1_LIVENESS_H
+#define _BUGGED1_LIVENESS_H
int yyparse(void);
int yywrap(void);
int yylex(void);
-int predP(void);
-int predQ(void);
+int predR(void);
+int predCS(void);
int coordinator(int argc, char *argv[]);
int client(int argc, char *argv[]);
--- /dev/null
+#include "msg/msg.h"
+#include "mc/mc.h"
+#include "xbt/automaton.h"
+#include "xbt/automatonparse_promela.h"
+#include "bugged2_liveness.h"
+#include "y.tab.c"
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages");
+
+char* buffer;
+
+int consume = 0;
+int produce = 0;
+int cready = 0;
+int pready = 0;
+
+int predPready(){
+ return pready;
+}
+
+int predCready(){
+ return cready;
+}
+
+int predConsume(){
+ return consume;
+}
+
+int predProduce(){
+ return produce;
+}
+
+int coordinator(int argc, char *argv[])
+{
+ xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
+ int CS_used = 0;
+
+ while(1) {
+ m_task_t task = NULL;
+ MSG_task_receive(&task, "coordinator");
+ const char *kind = MSG_task_get_name(task);
+ if (!strcmp(kind, "request")) {
+ char *req = MSG_task_get_data(task);
+ if (CS_used) {
+ XBT_INFO("CS already used. Queue the request");
+ xbt_dynar_push(requests, &req);
+ } else {
+ m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
+ MSG_task_send(answer, req);
+ CS_used = 1;
+ XBT_INFO("CS idle. Grant immediatly");
+ }
+ } else {
+ if (xbt_dynar_length(requests) > 0) {
+ XBT_INFO("CS release. Grant to queued requests");
+ char *req;
+ xbt_dynar_pop(requests, &req);
+ MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
+ } else {
+ XBT_INFO("CS_realase, ressource now idle");
+ CS_used = 0;
+ }
+ }
+
+ MSG_task_destroy(task);
+
+ }
+
+ return 0;
+
+}
+
+int producer(int argc, char *argv[])
+{
+
+ char * my_mailbox = bprintf("%s", argv[1]);
+
+ //while(1) {
+
+ /* Create message */
+ const char *mess = "message";
+
+ /* CS request */
+ XBT_INFO("Producer ask the request");
+ MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
+
+ /* Wait the answer */
+ m_task_t grant = NULL;
+ MSG_task_receive(&grant, my_mailbox);
+ MSG_task_destroy(grant);
+
+ pready = 1;
+
+ /* Push message (size of buffer = 1) */
+ buffer = strdup(mess);
+
+ /* CS release */
+ MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
+
+ produce = 1;
+ pready = 0;
+
+ //produce = 0;
+ //pready = 0;
+
+ //}
+
+ return 0;
+
+}
+
+int consumer(int argc, char *argv[])
+{
+
+ char * my_mailbox = bprintf("%s", argv[1]);
+ char *mess;
+
+
+ //while(1) {
+
+ /* CS request */
+ XBT_INFO("Consumer ask the request");
+ MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
+
+ /* Wait the answer */
+ m_task_t grant = NULL;
+ MSG_task_receive(&grant, my_mailbox);
+ MSG_task_destroy(grant);
+
+ cready = 1;
+
+ /* Pop message */
+ mess = malloc(8*sizeof(char));
+ mess = strdup(buffer);
+ buffer[0] = '\0';
+
+ /* CS release */
+ MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
+
+ /* Display message */
+ XBT_INFO("Message : %s", mess);
+ if(strcmp(mess, "") != 0)
+ consume = 1;
+
+ cready = 0;
+
+ free(mess);
+
+ //consume = 0;
+ //cready = 0;
+
+ //}
+
+ return 0;
+
+}
+
+
+int main(int argc, char *argv[])
+{
+
+ buffer = malloc(8*sizeof(char));
+ buffer[0]='\0';
+
+ init();
+ yyparse();
+ automaton = get_automaton();
+ xbt_new_propositional_symbol(automaton,"pready", &predPready);
+ xbt_new_propositional_symbol(automaton,"cready", &predCready);
+ xbt_new_propositional_symbol(automaton,"consume", &predConsume);
+ xbt_new_propositional_symbol(automaton,"produce", &predProduce);
+
+ MSG_global_init(&argc, argv);
+ MSG_create_environment("../msg_platform.xml");
+ MSG_function_register("coordinator", coordinator);
+ MSG_function_register("consumer", consumer);
+ MSG_function_register("producer", producer);
+ MSG_launch_application("deploy_bugged2_liveness.xml");
+ MSG_main_liveness(automaton, argv[0]);
+
+ return 0;
+
+}
--- /dev/null
+#ifndef _BUGGED2_LIVENESS_H
+#define _BUGGED2_LIVENESS_H
+
+int yyparse(void);
+int yywrap(void);
+int yylex(void);
+
+int predPready(void);
+int predCready(void);
+int predConsume(void);
+int predProduce(void);
+
+int coordinator(int argc, char *argv[]);
+int producer(int argc, char *argv[]);
+int consumer(int argc, char *argv[]);
+
+#endif
--- /dev/null
+<?xml version='1.0'?>
+
+<!DOCTYPE platform SYSTEM "http://simgrid.gforge.inria.fr/simgrid.dtd">
+
+<platform version="3">
+
+ <process host="Tremblay" function="coordinator" />
+
+ <process host="Fafard" function="consumer" >
+ <argument value="1"/>
+ </process>
+
+ <process host="Boivin" function="producer" >
+ <argument value="2"/>
+ </process>
+
+
+</platform>
+++ /dev/null
-/***************** Centralized Mutual Exclusion Algorithm *********************/
-/* This example implements a centralized mutual exclusion algorithm. */
-/* CS requests of client 2 not satisfied */
-/******************************************************************************/
-
-#include "msg/msg.h"
-#include "mc/mc.h"
-#include "xbt/automaton.h"
-#include "xbt/automatonparse_promela.h"
-#include "example_liveness_with_cycle.h"
-#include "y.tab.c"
-
-#define AMOUNT_OF_CLIENTS 2
-#define CS_PER_PROCESS 3
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle2, "my log messages");
-
-
-int p=0;
-int q=0;
-
-int predP(){
- return p;
-}
-
-int predQ(){
- return q;
-}
-
-
-int coordinator(int argc, char *argv[])
-{
- xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL); // dynamic vector storing requests (which are char*)
- int CS_used = 0; // initially the CS is idle
-
- while(1){
- m_task_t task = NULL;
- MSG_task_receive(&task, "coordinator");
- const char *kind = MSG_task_get_name(task); //is it a request or a release?
- if (!strcmp(kind, "request")) { // that's a request
- char *req = MSG_task_get_data(task);
- if (CS_used) { // need to push the request in the vector
- XBT_INFO("CS already used. Queue the request of client %d", atoi(req) +1);
- xbt_dynar_push(requests, &req);
- } else { // can serve it immediatly
- if(strcmp(req, "1") == 0){
- m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
- MSG_task_send(answer, req);
- CS_used = 1;
- XBT_INFO("CS idle. Grant immediatly");
- }
- }
- } else { // that's a release. Check if someone was waiting for the lock
- if (xbt_dynar_length(requests) > 0) {
- XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
- char *req ;
- xbt_dynar_get_cpy(requests, (xbt_dynar_length(requests) - 1), &req);
- if(strcmp(req, "1") == 0){
- xbt_dynar_pop(requests, &req);
- MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
- }else{
- CS_used = 0;
- }
- } else { // nobody wants it
- XBT_INFO("CS release. resource now idle");
- CS_used = 0;
- }
- }
- MSG_task_destroy(task);
- }
- XBT_INFO("Received all releases, quit now");
- return 0;
-}
-
-int client(int argc, char *argv[])
-{
- int my_pid = MSG_process_get_PID(MSG_process_self());
-
- char *my_mailbox = bprintf("%s", argv[1]);
-
- while(1){
-
- XBT_INFO("Ask the request");
-
- MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
-
- if(strcmp(my_mailbox, "2") == 0){
- p = 1;
- q = 0;
- XBT_INFO("Propositions changed (p=1, q=0)");
- }
-
- // wait the answer
-
- m_task_t grant = NULL;
- MSG_task_receive(&grant, my_mailbox);
-
- if((strcmp(my_mailbox, "2") == 0) && (strcmp(MSG_task_get_name(grant), "grant") == 0)){
- q = 1;
- p = 0;
- XBT_INFO("Propositions changed (q=1, p=0)");
- }
-
- MSG_task_destroy(grant);
- XBT_INFO("%s got the answer. Sleep a bit and release it", argv[1]);
- MSG_process_sleep(1);
-
- MSG_task_send(MSG_task_create("release", 0, 1000, NULL), "coordinator");
-
- MSG_process_sleep(my_pid);
-
- if(strcmp(my_mailbox, "2") == 0){
- q=0;
- p=0;
- XBT_INFO("Propositions changed (q=0, p=0)");
- }
-
- }
-
- XBT_INFO("Got all the CS I wanted (%s), quit now", my_mailbox);
- return 0;
-}
-
-int main(int argc, char *argv[])
-{
- init();
- yyparse();
- automaton = get_automaton();
- xbt_new_propositional_symbol(automaton,"p", &predP);
- xbt_new_propositional_symbol(automaton,"q", &predQ);
-
- MSG_global_init(&argc, argv);
- MSG_create_environment("../msg_platform.xml");
- MSG_function_register("coordinator", coordinator);
- MSG_function_register("client", client);
- MSG_launch_application("deploy_mutex2.xml");
- MSG_main_liveness(automaton, argv[0]);
-
- return 0;
-}
-never { /* !G(p->Fq) */
+never { /* !G(r->Fcs) */
T0_init : /* init */
if
:: (1) -> goto T0_init
- :: (!q && p) -> goto accept_S2
+ :: (!cs && r) -> goto accept_S2
fi;
accept_S2 : /* 1 */
if
- :: (!q) -> goto accept_S2
+ :: (!cs) -> goto accept_S2
fi;
-}
\ No newline at end of file
+}
--- /dev/null
+never { /* !(G((!cs) -> F(cs))) */
+T0_init : /* init */
+ if
+ :: (1) -> goto T0_init
+ :: (!cs) -> goto accept_S2
+ fi;
+accept_S2 : /* 1 */
+ if
+ :: (!cs) -> goto accept_S2
+ fi;
+}
--- /dev/null
+never { /* !(GF((pready U produce) -> (cready U consume))) */
+T0_init : /* init */
+ if
+ :: (1) -> goto T1_S1
+ :: (produce && !consume) -> goto accept_S5
+ :: (pready && !consume) -> goto T0_S5
+ fi;
+T1_S1 : /* 1 */
+ if
+ :: (1) -> goto T1_S1
+ :: (produce && !consume) || (pready && !consume) -> goto accept_S5
+ fi;
+accept_S5 : /* 2 */
+ if
+ :: (pready && !consume) -> goto T0_S5
+ :: (produce && !consume) -> goto accept_S5
+ fi;
+T0_S5 : /* 3 */
+ if
+ :: (pready && !consume) -> goto T0_S5
+ :: (produce && !consume) -> goto accept_S5
+ fi;
+}
\ No newline at end of file
