model-checker : cosmetics in log message

[simgrid.git] / src / mc / mc_dpor.c

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index ba6c542..ac5e674 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -66,7 +66,7 @@ static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2
 static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){
 
   if(!xbt_dynar_is_empty(incomplete_communications_pattern))
-    xbt_die("Oh oh ...");
+    xbt_die("Damn ! Some communications are incomplete that means one or several simcalls are not handle ... ");
 
   unsigned int cursor = 0, send_index = 0, recv_index = 0;
   mc_comm_pattern_t comm1, comm2;
@@ -691,7 +691,6 @@ void MC_dpor(void)
       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
         if(initial_state_safety->initial_communications_pattern_done){
           if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
-            //print_communications_pattern(communications_pattern);
             deterministic_pattern(initial_communications_pattern, communications_pattern);
             if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
               XBT_INFO("****************************************************");
@@ -704,9 +703,9 @@ void MC_dpor(void)
               MC_print_statistics(mc_stats);
               return;
             }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
-              XBT_INFO("****************************************************");
+              XBT_INFO("*********************************************************");
               XBT_INFO("***** Non-send-deterministic communications pattern *****");
-              XBT_INFO("****************************************************");
+              XBT_INFO("*********************************************************");
               XBT_INFO("Initial communications pattern:");
               print_communications_pattern(initial_communications_pattern);
               XBT_INFO("Communications pattern counter-example:");