model-checker : update chord example for exhaustive exploration with MC

diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c
index 09c455f..e2aa9d0 100644 (file)
--- a/examples/msg/chord/chord.c
+++ b/examples/msg/chord/chord.c
@@ -293,6 +293,12 @@ int node(int argc, char *argv[])
   double next_check_predecessor_date = init_time + periodic_check_predecessor_delay;
   double next_lookup_date = init_time + periodic_lookup_delay;
 
   double next_check_predecessor_date = init_time + periodic_check_predecessor_delay;
   double next_lookup_date = init_time + periodic_lookup_delay;
 

+  #ifdef HAVE_MC
+  int listen = 0;
+  int no_op = 0;
+  int sub_protocol = 0;
+  #endif
+

   xbt_assert(argc == 3 || argc == 5, "Wrong number of arguments for this node");
 
   // initialize my node
   xbt_assert(argc == 3 || argc == 5, "Wrong number of arguments for this node");
 
   // initialize my node


@@ -339,67 +345,68 @@ int node(int argc, char *argv[])
         // FIXME: do not make MSG_task_irecv() calls from several functions
       }
 
         // FIXME: do not make MSG_task_irecv() calls from several functions
       }
 

+      //XBT_INFO("Node %d is ring member : %d", node.id, is_ring_member(known_id, node.id) != -1);
+

       if (!MSG_comm_test(node.comm_receive)) {
 
         // no task was received: make some periodic calls
 
       if (!MSG_comm_test(node.comm_receive)) {
 
         // no task was received: make some periodic calls
 

-        #ifdef HAVE_MC
-          if(MC_is_active()){
-            if(MC_random()){
+#ifdef HAVE_MC
+        if(MC_is_active()){
+          if(!MC_visited_reduction() && no_op){
+              MC_cut();
+          }
+          if(listen == 0 && (sub_protocol = MC_random(0, 4)) > 0){
+            if(sub_protocol == 1)

               stabilize(&node);
               stabilize(&node);

-            }else if(MC_random()){
+            else if(sub_protocol == 2)

               fix_fingers(&node);
               fix_fingers(&node);

-            }else if(MC_random()){
+            else if(sub_protocol == 3)

               check_predecessor(&node);
               check_predecessor(&node);

-            }else if(MC_random()){
+            else

               random_lookup(&node);
               random_lookup(&node);

-            }else{
-              MSG_process_sleep(5);
-            }
+            listen = 1;

           }else{
           }else{

-            if (MSG_get_clock() >= next_stabilize_date) {
-              stabilize(&node);
-              next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay;
-            }
-            else if (MSG_get_clock() >= next_fix_fingers_date) {
-              fix_fingers(&node);
-              next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay;
-            }
-            else if (MSG_get_clock() >= next_check_predecessor_date) {
-              check_predecessor(&node);
-              next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay;
-            }
-            else if (MSG_get_clock() >= next_lookup_date) {
-              random_lookup(&node);
-              next_lookup_date = MSG_get_clock() + periodic_lookup_delay;
-            }
-            else {
-              // nothing to do: sleep for a while
-              MSG_process_sleep(5);
-            }
+            MSG_process_sleep(5);
+            if(!MC_visited_reduction())
+              no_op = 1;

           }
           }

-        #else
+        }else{

           if (MSG_get_clock() >= next_stabilize_date) {
             stabilize(&node);
             next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay;
           if (MSG_get_clock() >= next_stabilize_date) {
             stabilize(&node);
             next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay;

-          }
-          else if (MSG_get_clock() >= next_fix_fingers_date) {
+          }else if (MSG_get_clock() >= next_fix_fingers_date) {

             fix_fingers(&node);
             next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay;
             fix_fingers(&node);
             next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay;

-          }
-          else if (MSG_get_clock() >= next_check_predecessor_date) {
+          }else if (MSG_get_clock() >= next_check_predecessor_date) {

             check_predecessor(&node);
             next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay;
             check_predecessor(&node);
             next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay;

-          }
-          else if (MSG_get_clock() >= next_lookup_date) {
+          }else if (MSG_get_clock() >= next_lookup_date) {

             random_lookup(&node);
             next_lookup_date = MSG_get_clock() + periodic_lookup_delay;
             random_lookup(&node);
             next_lookup_date = MSG_get_clock() + periodic_lookup_delay;

-          }
-          else {
+          }else {

             // nothing to do: sleep for a while
             MSG_process_sleep(5);
           }
             // nothing to do: sleep for a while
             MSG_process_sleep(5);
           }

-        #endif
+        }
+#else
+        if (MSG_get_clock() >= next_stabilize_date) {
+          stabilize(&node);
+          next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay;
+        }else if (MSG_get_clock() >= next_fix_fingers_date) {
+          fix_fingers(&node);
+          next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay;
+        }else if (MSG_get_clock() >= next_check_predecessor_date) {
+          check_predecessor(&node);
+          next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay;
+        }else if (MSG_get_clock() >= next_lookup_date) {
+          random_lookup(&node);
+          next_lookup_date = MSG_get_clock() + periodic_lookup_delay;
+        }else {
+          // nothing to do: sleep for a while
+          MSG_process_sleep(5);
+        }
+#endif

 
       } else {
         // a transfer has occurred
 
       } else {
         // a transfer has occurred


@@ -781,9 +788,9 @@ static int remote_get_predecessor(node_t node, int ask_to)
         msg_task_t task_received = MSG_comm_get_task(node->comm_receive);
         task_data_t ans_data = MSG_task_get_data(task_received);
 
         msg_task_t task_received = MSG_comm_get_task(node->comm_receive);
         task_data_t ans_data = MSG_task_get_data(task_received);
 

-        if (MC_is_active()) {
+        /*if (MC_is_active()) {

           MC_assert(task_received == task_sent);
           MC_assert(task_received == task_sent);

-        }
+          }*/

 
         if (task_received != task_sent) {
           MSG_comm_destroy(node->comm_receive);
 
         if (task_received != task_sent) {
           MSG_comm_destroy(node->comm_receive);

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index 5cffc94..376ab92 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -15,8 +15,10 @@
 #ifdef HAVE_MC
 
 extern int _sg_do_model_check; /* please don't use directly: we inline MC_is_active, but that's what you should use */
 #ifdef HAVE_MC
 
 extern int _sg_do_model_check; /* please don't use directly: we inline MC_is_active, but that's what you should use */

+extern int _sg_mc_visited;

 
 #define MC_is_active() _sg_do_model_check
 
 #define MC_is_active() _sg_do_model_check

+#define MC_visited_reduction() _sg_mc_visited

 
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(int) MC_random(int min, int max);
 
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(int) MC_random(int min, int max);


@@ -29,6 +31,7 @@ XBT_PUBLIC(void) MC_cut(void);
 
 #define MC_assert(a) xbt_assert(a)
 #define MC_is_active() 0
 
 #define MC_assert(a) xbt_assert(a)
 #define MC_is_active() 0

+#define MC_visited_reduction() 0

 
 #endif
 
 
 #endif