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)
+add_executable(centralized_liveness automaton.c automatonparse_promela.c centralized_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 )
+target_link_libraries(centralized_liveness simgrid m )
\ No newline at end of file
+++ /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
+/***************** Producer/Consumer Algorithm *************************/
+/* This example implements a producer/consumer algorithm. */
+/* If consumer work before producer, message is empty */
+/***********************************************************************/
+
+
+#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
+#include "msg/msg.h"
+#include "mc/mc.h"
+#include "xbt/automaton.h"
+#include "xbt/automatonparse_promela.h"
+#include "centralized_liveness.h"
+#include "y.tab.c"
+
+#define AMOUNT_OF_CLIENTS 2
+#define CS_PER_PROCESS 1
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(centralized, "my log messages");
+
+int cs2 = 0;
+
+int predCS2(){
+ return cs2;
+}
+
+
+int coordinator(int argc, char **argv);
+int client(int argc, char **argv);
+
+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");
+ xbt_dynar_push(requests, &req);
+ } else { // can serve it immediatly
+ XBT_INFO("CS idle. Grant immediatly");
+ m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
+ MSG_task_send(answer, req);
+ CS_used = 1;
+ }
+ } else { // that's a release. Check if someone was waiting for the lock
+ if (!xbt_dynar_is_empty(requests)) {
+ XBT_INFO("CS release. Grant to queued requests (queue size: %lu)",
+ xbt_dynar_length(requests));
+ char *req;
+ xbt_dynar_pop(requests, &req);
+ MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
+ } else { // nobody wants it
+ XBT_INFO("CS release. resource now idle");
+ CS_used = 0;
+ }
+ }
+ MSG_task_destroy(task);
+ }
+
+ 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){
+
+ if(!strcmp(my_mailbox, "2"))
+ cs2 = 0;
+
+ XBT_INFO("Client (%s) ask the request", my_mailbox);
+ 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);
+ XBT_INFO("got the answer. Sleep a bit and release it");
+
+ if(!strcmp(my_mailbox, "2"))
+ cs2 = 1;
+
+ MSG_process_sleep(1);
+ MSG_task_send(MSG_task_create("release", 0, 1000, NULL),
+ "coordinator");
+ MSG_process_sleep(my_pid);
+ }
+
+ return 0;
+}
+
+int main(int argc, char *argv[])
+{
+ init();
+ yyparse();
+ automaton = get_automaton();
+ xbt_new_propositional_symbol(automaton,"cs2", &predCS2);
+
+ 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_centralized_liveness.xml");
+ MSG_main_liveness(automaton, argv[0]);
+
+ return 0;
+
+}
--- /dev/null
+#ifndef _CENTRALIZED_LIVENESS_H
+#define _CENTRALIZED_LIVENESS_H
+
+int yyparse(void);
+int yywrap(void);
+int yylex(void);
+
+int predCS2(void);
+
+int coordinator(int argc, char *argv[]);
+int client(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
+<?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="client" >
+ <argument value="1"/>
+ </process>
+
+ <process host="Boivin" function="client" >
+ <argument value="2"/>
+ </process>
+
+ <!-- <process host="TeX" function="client" >
+ <argument value="3"/>
+ </process>
+
+ <process host="Geoff" function="client" >
+ <argument value="4"/>
+ </process>
+
+ <process host="Disney" function="client" />
+
+ <process host="iRMX" function="client" />
+
+ <process host="McGee" function="client" />
+
+ <process host="Gatien" function="client" />
+
+ <process host="Laroche" function="client" />
+
+ <process host="Tanguay" function="client" />
+
+ <process host="Morin" function="client" />
+
+ <process host="Ethernet" function="client" />
+
+ <process host="Bellemarre" function="client" />
+
+ <process host="Kuenning" function="client" />
+
+ <process host="Gaston" function="client" /> -->
+
+</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;
-}
--- /dev/null
+never { /* !G(r->Fcs) */
+T0_init : /* init */
+ if
+ :: (1) -> goto T0_init
+ :: (!cs && r) -> goto accept_S2
+ fi;
+accept_S2 : /* 1 */
+ if
+ :: (!cs) -> goto accept_S2
+ fi;
+}
--- /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 { /* !(G((pready U produce) -> F(cready U consume))) */
+T1_init : /* init */
+ if
+ :: (1) -> goto T1_init
+ :: (pready && !consume) -> goto T0_S2
+ :: (produce && !consume) -> goto accept_S3
+ fi;
+T0_S2 : /* 1 */
+ if
+ :: (pready && !consume) -> goto T0_S2
+ :: (produce && !consume) -> goto accept_S3
+ fi;
+accept_S3 : /* 2 */
+ if
+ :: (!consume) -> goto accept_S3
+ 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
-never { /* !G(p->Fq) */
+never { /* !(GFcs2) */
T0_init : /* init */
if
:: (1) -> goto T0_init
- :: (!q && p) -> goto accept_S2
+ :: (!cs2) -> goto accept_S2
fi;
accept_S2 : /* 1 */
if
- :: (!q) -> goto accept_S2
+ :: (!cs2) -> goto accept_S2
fi;
}
\ No newline at end of file
/********************************* Global *************************************/
XBT_PUBLIC(void) MC_init_safety_stateless(void);
XBT_PUBLIC(void) MC_init_safety_stateful(void);
-XBT_PUBLIC(void) MC_init_liveness_stateful(xbt_automaton_t a, char *prgm);
-XBT_PUBLIC(void) MC_init_liveness_stateless(xbt_automaton_t a, char *prgm);
+XBT_PUBLIC(void) MC_init_liveness(xbt_automaton_t a, char *prgm);
XBT_PUBLIC(void) MC_exit(void);
XBT_PUBLIC(void) MC_exit_liveness(void);
XBT_PUBLIC(void) MC_assert(int);
XBT_PUBLIC(void) MC_assert_stateful(int);
-XBT_PUBLIC(void) MC_assert_pair_stateful(int);
-XBT_PUBLIC(void) MC_assert_pair_stateless(int);
+XBT_PUBLIC(void) MC_assert_pair(int);
XBT_PUBLIC(void) MC_modelcheck(void);
XBT_PUBLIC(void) MC_modelcheck_stateful(void);
XBT_PUBLIC(void) MC_modelcheck_liveness(xbt_automaton_t a, char *prgm);
-XBT_PUBLIC(void) MC_modelcheck_liveness_stateful(xbt_automaton_t a, char *prgm);
-XBT_PUBLIC(void) MC_modelcheck_liveness_stateless(xbt_automaton_t a, char *prgm);
XBT_PUBLIC(int) MC_random(int, int);
XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
if(s1->num_reg != s2->num_reg){
- //XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
+ XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
return 1;
}
int i;
+ int errors = 0;
for(i=0 ; i< s1->num_reg ; i++){
if(s1->regions[i]->type != s2->regions[i]->type){
- //XBT_DEBUG("Different type of region");
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different type of region");
+ errors++;
+ }else{
+ return 1;
+ }
}
switch(s1->regions[i]->type){
case 0:
if(s1->regions[i]->size != s2->regions[i]->size){
- //XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different size of heap (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
+ errors++;
+ }else{
+ return 1;
+ }
}
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
- //XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+ errors++;
+ }else{
+ return 1;
+ }
}
if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){
- //XBT_DEBUG("Different heap (mmalloc_compare)");
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different heap (mmalloc_compare)");
+ errors++;
+ }else{
+ return 1;
+ }
}
break;
case 1 :
if(s1->regions[i]->size != s2->regions[i]->size){
- //XBT_DEBUG("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different size of libsimgrid (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
+ errors++;
+ }else{
+ return 1;
+ }
}
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
- //XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+ errors++;
+ }else{
+ return 1;
+ }
}
if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
- //XBT_DEBUG("Different memcmp for data in libsimgrid");
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different memcmp for data in libsimgrid");
+ errors++;
+ }else{
+ return 1;
+ }
}
break;
- case 2:
+ /*case 2:
if(s1->regions[i]->size != s2->regions[i]->size){
- //XBT_DEBUG("Different size of program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
- return 1;
- }
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different size of program (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
+ errors++;
+ }else{
+ return 1;
+ }
+ }
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
- //XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+ errors++;
+ }else{
+ return 1;
+ }
}
if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
- //XBT_DEBUG("Different memcmp for data in program");
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different memcmp for data in program");
+ errors++;
+ }else{
+ return 1;
+ }
}
- break;
+ break;*/
case 3:
if(s1->regions[i]->size != s2->regions[i]->size){
- //XBT_DEBUG("Different size of stack (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different size of stack (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
+ errors++;
+ }else{
+ return 1;
+ }
}
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
- //XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+ errors++;
+ }else{
+ return 1;
+ }
}
if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
- //XBT_DEBUG("Different memcmp for data in stack");
- return 1;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ XBT_DEBUG("Different memcmp for data in stack");
+ errors++;
+ }else{
+ return 1;
+ }
}
break;
+ default:
+ break;
}
}
- return 0;
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+ return (errors>0);
+ }else{
+ return 0;
+ }
}
xbt_dynar_foreach(reached_pairs, cursor, pair_test){
if(automaton_state_compare(pair_test->automaton_state, st) == 0){
if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+ XBT_DEBUG("Pair reached %d", cursor+1);
if(snapshot_compare(pair_test->system_state, sn) == 0){
MC_free_snapshot(sn);
xbt_dynar_reset(prop_ato);
}
}
- //reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
- reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
+ reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
+ //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
//visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
MC_UNSET_RAW_MEM;
- //set_pair_reached(state);
- set_pair_reached_hash(state);
+ set_pair_reached(state);
+ //set_pair_reached_hash(state);
if(cursor != 0){
MC_restore_snapshot(initial_snapshot_liveness);
mc_stats_pair->visited_pairs++;
- //sleep(1);
+ sleep(1);
int value;
mc_state_t next_graph_state = NULL;
if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
- //if(reached(pair_succ->automaton_state)){
- if(reached_hash(pair_succ->automaton_state)){
+ if(reached(pair_succ->automaton_state)){
+ //if(reached_hash(pair_succ->automaton_state)){
XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
- //set_pair_reached(pair_succ->automaton_state);
- set_pair_reached_hash(pair_succ->automaton_state);
+ set_pair_reached(pair_succ->automaton_state);
+ //set_pair_reached_hash(pair_succ->automaton_state);
- //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
- XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+ XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
MC_SET_RAW_MEM;
xbt_fifo_unshift(mc_stack_liveness, pair_succ);
XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
- //set_pair_reached(pair_succ->automaton_state);
- set_pair_reached_hash(pair_succ->automaton_state);
+ set_pair_reached(pair_succ->automaton_state);
+ //set_pair_reached_hash(pair_succ->automaton_state);
search_cycle = 1;
- //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
- XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+ XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
}
if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
- //if(reached(pair_succ->automaton_state)){
- if(reached_hash(pair_succ->automaton_state)){
+ if(reached(pair_succ->automaton_state)){
+ //if(reached_hash(pair_succ->automaton_state)){
XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
XBT_DEBUG("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
- //set_pair_reached(pair_succ->automaton_state);
- set_pair_reached_hash(pair_succ->automaton_state);
+ set_pair_reached(pair_succ->automaton_state);
+ //set_pair_reached_hash(pair_succ->automaton_state);
- //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
- XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+ XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
MC_SET_RAW_MEM;
xbt_fifo_unshift(mc_stack_liveness, pair_succ);
if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
- //set_pair_reached(pair_succ->automaton_state);
- set_pair_reached_hash(pair_succ->automaton_state);
+ set_pair_reached(pair_succ->automaton_state);
+ //set_pair_reached_hash(pair_succ->automaton_state);
search_cycle = 1;
- //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
- XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+ XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
}
- //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
- if(!visited(pair_succ->automaton_state, search_cycle)){
+ if(!visited_hash(pair_succ->automaton_state, search_cycle)){
+ //if(!visited(pair_succ->automaton_state, search_cycle)){
MC_SET_RAW_MEM;
xbt_fifo_unshift(mc_stack_liveness, pair_succ);
MC_SET_RAW_MEM;
xbt_fifo_shift(mc_stack_liveness);
if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
- //xbt_dynar_pop(reached_pairs, NULL);
- xbt_dynar_pop(reached_pairs_hash, NULL);
+ xbt_dynar_pop(reached_pairs, NULL);
+ //xbt_dynar_pop(reached_pairs_hash, NULL);
}
MC_UNSET_RAW_MEM;
frag_size = pow(2,mdp1->heapinfo[i].busy.type);
for(j=0 ; j< (BLOCKSIZE/frag_size); j++){
if(memcmp((char *)addr_block1 + (j * frag_size), (char *)addr_block2 + (j * frag_size), frag_size) != 0){
- XBT_DEBUG("Different data in fragment %zu of block %zu", j + 1, i);
+ XBT_DEBUG("Different data in fragment %Zu of block %Zu", j + 1, i);
return 1;
}
}
