model-checker : fix dpor

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

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index c3a3383..c52988b 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -28,7 +28,7 @@ static void visited_state_free_voidp(void *s){
 static int is_visited_state(){
 
   if(_sg_mc_visited == 0)
-    return 0;
+    return -1;
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
@@ -49,14 +49,14 @@ static int is_visited_state(){
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
- 
-    return 0;
+
+    return -1;
 
   }else{
 
     MC_SET_RAW_MEM;
     
-    size_t current_chunks_used = new_state->system_state->heap_chunks_used;
+    size_t current_bytes_used = new_state->system_state->heap_bytes_used;
 
     unsigned int cursor = 0;
     int previous_cursor = 0, next_cursor = 0;
@@ -64,60 +64,63 @@ static int is_visited_state(){
     int end = xbt_dynar_length(visited_states) - 1;
 
     mc_safety_visited_state_t state_test = NULL;
-    size_t chunks_used_test;
-    int same_chunks_not_found = 1;
+    size_t bytes_used_test;
+    int same_bytes_not_found = 1;
 
-    while(start <= end && same_chunks_not_found){
+    while(start <= end && same_bytes_not_found){
       cursor = (start + end) / 2;
       state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
-      chunks_used_test = state_test->system_state->heap_chunks_used;
-      if(chunks_used_test < current_chunks_used)
+      bytes_used_test = state_test->system_state->heap_bytes_used;
+      if(bytes_used_test < current_bytes_used)
         start = cursor + 1;
-      if(chunks_used_test > current_chunks_used)
+      if(bytes_used_test > current_bytes_used)
         end = cursor - 1; 
-      if(chunks_used_test == current_chunks_used){
-        same_chunks_not_found = 0;
+      if(bytes_used_test == current_bytes_used){
+        same_bytes_not_found = 0;
         if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
           xbt_dynar_remove_at(visited_states, cursor, NULL);
           xbt_dynar_insert_at(visited_states, cursor, &new_state);
+          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
           if(raw_mem_set)
             MC_SET_RAW_MEM;
           else
             MC_UNSET_RAW_MEM;
-          return 1;
+          return state_test->num;
         }else{
-          /* Search another state with same number of chunks used */
+          /* Search another state with same number of bytes used */
           previous_cursor = cursor - 1;
           while(previous_cursor >= 0){
             state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t);
-            chunks_used_test = state_test->system_state->heap_chunks_used;
-            if(chunks_used_test != current_chunks_used)
+            bytes_used_test = state_test->system_state->heap_bytes_used;
+            if(bytes_used_test != current_bytes_used)
               break;
             if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
               xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
               xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
+              XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
               if(raw_mem_set)
                 MC_SET_RAW_MEM;
               else
                 MC_UNSET_RAW_MEM;
-              return 1;
+              return state_test->num;
             }
             previous_cursor--;
           }
           next_cursor = cursor + 1;
           while(next_cursor < xbt_dynar_length(visited_states)){
             state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t);
-            chunks_used_test = state_test->system_state->heap_chunks_used;
-            if(chunks_used_test != current_chunks_used)
+            bytes_used_test = state_test->system_state->heap_bytes_used;
+            if(bytes_used_test != current_bytes_used)
               break;
             if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
               xbt_dynar_remove_at(visited_states, next_cursor, NULL);
               xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
+              XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
               if(raw_mem_set)
                 MC_SET_RAW_MEM;
               else
                 MC_UNSET_RAW_MEM;
-              return 1;
+              return state_test->num;
             }
             next_cursor++;
           }
@@ -126,9 +129,9 @@ static int is_visited_state(){
     }
 
     state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
-    chunks_used_test = state_test->system_state->heap_chunks_used;
+    bytes_used_test = state_test->system_state->heap_bytes_used;
 
-    if(chunks_used_test < current_chunks_used)
+    if(bytes_used_test < current_bytes_used)
       xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
     else
       xbt_dynar_insert_at(visited_states, cursor, &new_state);
@@ -151,7 +154,7 @@ static int is_visited_state(){
     if(raw_mem_set)
       MC_SET_RAW_MEM;
     
-    return 0;
+    return -1;
     
   }
 }
@@ -219,6 +222,7 @@ void MC_dpor(void)
   xbt_fifo_item_t item = NULL;
   int pos, i, interleave_size;
   int interleave_proc[simix_process_maxpid];
+  int visited_state;
 
   while (xbt_fifo_size(mc_stack_safety) > 0) {
 
@@ -245,6 +249,8 @@ void MC_dpor(void)
         XBT_DEBUG("Execute: %s", req_str);
         xbt_free(req_str);
       }
+        
+      req_str = MC_request_get_dot_output(req, value);
 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
@@ -292,7 +298,7 @@ void MC_dpor(void)
 
       next_state = MC_state_new();
 
-      if(!is_visited_state()){
+      if((visited_state = is_visited_state()) == -1){
      
         /* Get an enabled process and insert it in the interleave set of the next state */
         xbt_swag_foreach(process, simix_global->process_list){
@@ -306,15 +312,23 @@ void MC_dpor(void)
           next_state->system_state = MC_take_snapshot();
         }
 
+        if(dot_output != NULL)
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
+
       }else{
 
-        XBT_DEBUG("State already visited !");
-        
+        if(dot_output != NULL)
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
+
       }
 
+      
+
       xbt_fifo_unshift(mc_stack_safety, next_state);
       MC_UNSET_RAW_MEM;
 
+      xbt_free(req_str);
+
       /* Let's loop again */
 
       /* The interleave set is empty or the maximum depth is reached, let's back-track */