model-checker : minor fix in ddfs algorithm

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

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 3e5b2dd..a360a24 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -83,17 +83,18 @@ static int is_reached_acceptance_pair(mc_pair_t pair){
       nb_processes_test = pair_test->nb_processes;
       if(nb_processes_test < current_nb_processes)
         start = cursor + 1;
-      if(nb_processes_test > current_nb_processes)
+      else if(nb_processes_test > current_nb_processes)
         end = cursor - 1; 
-      if(nb_processes_test == current_nb_processes){
+      else if(nb_processes_test == current_nb_processes){
         if(bytes_used_test < current_bytes_used)
           start = cursor + 1;
-        if(bytes_used_test > current_bytes_used)
+        else if(bytes_used_test > current_bytes_used)
           end = cursor - 1;
-        if(bytes_used_test == current_bytes_used){
+        else if(bytes_used_test == current_bytes_used){
           same_processes_and_bytes_not_found = 0;
           if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
             if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
+              XBT_DEBUG("Compare with state %d", pair_test->num);
               if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
                 if(raw_mem_set)
                   MC_SET_RAW_MEM;
@@ -112,6 +113,7 @@ static int is_reached_acceptance_pair(mc_pair_t pair){
               break;
             if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
               if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){  
+                XBT_DEBUG("Compare with state %d", pair_test->num);
                 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
                   if(raw_mem_set)
                     MC_SET_RAW_MEM;
@@ -131,6 +133,7 @@ static int is_reached_acceptance_pair(mc_pair_t pair){
               break;
             if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
               if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
+                XBT_DEBUG("Compare with state %d", pair_test->num);
                 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
                   if(raw_mem_set)
                     MC_SET_RAW_MEM;
@@ -301,7 +304,6 @@ static int is_visited_pair(mc_pair_t pair){
     size_t bytes_used_test;
     int nb_processes_test;
     int same_processes_and_bytes_not_found = 1;
-    int result;
 
     while(start <= end && same_processes_and_bytes_not_found){
       cursor = (start + end) / 2;
@@ -310,22 +312,29 @@ static int is_visited_pair(mc_pair_t pair){
       nb_processes_test = pair_test->nb_processes;
       if(nb_processes_test < current_nb_processes)
         start = cursor + 1;
-      if(nb_processes_test > current_nb_processes)
+      else if(nb_processes_test > current_nb_processes)
         end = cursor - 1; 
-      if(nb_processes_test == current_nb_processes){
+      else if(nb_processes_test == current_nb_processes){
         if(bytes_used_test < current_bytes_used)
           start = cursor + 1;
-        if(bytes_used_test > current_bytes_used)
+        else if(bytes_used_test > current_bytes_used)
           end = cursor - 1;
-        if(bytes_used_test == current_bytes_used){
+        else if(bytes_used_test == current_bytes_used){
           same_processes_and_bytes_not_found = 0;
           if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
             if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
               if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
+                if(pair_test->other_num == -1)
+                  pair->other_num = pair_test->num;
+                else
+                  pair->other_num = pair_test->other_num;
+                if(dot_output == NULL)
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
+                else
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
                 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
                 xbt_dynar_insert_at(visited_pairs, cursor, &pair);
                 pair_test->visited_removed = 1;
-                result = pair_test->num;
                 if(pair_test->stack_removed && pair_test->visited_removed){
                   if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
                     if(pair_test->acceptance_removed){ 
@@ -339,7 +348,7 @@ static int is_visited_pair(mc_pair_t pair){
                   MC_SET_RAW_MEM;
                 else
                   MC_UNSET_RAW_MEM;
-                return result;
+                return pair->other_num;
               }
             }
           }
@@ -353,10 +362,17 @@ static int is_visited_pair(mc_pair_t pair){
             if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
               if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){  
                 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
+                  if(pair_test->other_num == -1)
+                    pair->other_num = pair_test->num;
+                  else
+                    pair->other_num = pair_test->other_num;
+                  if(dot_output == NULL)
+                    XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
+                  else
+                    XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
                   xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
                   xbt_dynar_insert_at(visited_pairs, previous_cursor, &pair);
                   pair_test->visited_removed = 1;
-                  result = pair_test->num;
                   if(pair_test->stack_removed && pair_test->visited_removed){
                     if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
                       if(pair_test->acceptance_removed){ 
@@ -370,7 +386,7 @@ static int is_visited_pair(mc_pair_t pair){
                     MC_SET_RAW_MEM;
                   else
                     MC_UNSET_RAW_MEM;
-                  return result;
+                  return pair->other_num;
                 }
               }
             }
@@ -385,10 +401,17 @@ static int is_visited_pair(mc_pair_t pair){
             if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
               if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
                 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
+                  if(pair_test->other_num == -1)
+                    pair->other_num = pair_test->num;
+                  else
+                    pair->other_num = pair_test->other_num;
+                  if(dot_output == NULL)
+                    XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
+                  else
+                    XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
                   xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
                   xbt_dynar_insert_at(visited_pairs, next_cursor, &pair);
                   pair_test->visited_removed = 1;
-                  result = pair_test->num;
                   if(pair_test->stack_removed && pair_test->visited_removed){
                     if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
                       if(pair_test->acceptance_removed){ 
@@ -402,7 +425,7 @@ static int is_visited_pair(mc_pair_t pair){
                     MC_SET_RAW_MEM;
                   else
                     MC_UNSET_RAW_MEM;
-                  return result;
+                  return pair->other_num;
                 }
               }
             }
@@ -506,6 +529,7 @@ void MC_ddfs_init(void){
   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 
   initial_state_liveness->snapshot = MC_take_snapshot();
+  initial_state_liveness->prev_pair = 0;
 
   MC_UNSET_RAW_MEM; 
   
@@ -613,7 +637,6 @@ void MC_ddfs(){
   unsigned int cursor = 0;
   int res;
   int reached_num, visited_num;
-  int new_pair = 0;
 
   mc_pair_t next_pair = NULL;
   xbt_dynar_t prop_values = NULL;
@@ -632,6 +655,8 @@ void MC_ddfs(){
             
             MC_SET_RAW_MEM;
             xbt_fifo_shift(mc_stack_liveness);
+            if(dot_output != NULL)
+              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, reached_num, initial_state_liveness->prev_req);
             MC_UNSET_RAW_MEM;
 
             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
@@ -649,19 +674,40 @@ void MC_ddfs(){
 
       if((visited_num = is_visited_pair(current_pair)) != -1){
 
-        XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
+        MC_SET_RAW_MEM;
+        if(dot_output != NULL)
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req);
+        MC_UNSET_RAW_MEM;
+        
       
-      }else{            
+      }else{  
 
         while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
-   
+
+          MC_SET_RAW_MEM;
+          if(dot_output != NULL){
+            if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){
+              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req);
+              xbt_free(initial_state_liveness->prev_req);
+            }
+            initial_state_liveness->prev_pair = current_pair->num;
+          }
+          MC_UNSET_RAW_MEM;
+
           /* Debug information */
-          
           if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
             req_str = MC_request_to_string(req, value);
             XBT_DEBUG("Execute: %s", req_str);
             xbt_free(req_str);
           }
+
+          MC_SET_RAW_MEM;
+          if(dot_output != NULL){
+            initial_state_liveness->prev_req = MC_request_get_dot_output(req, value);
+            if(current_pair->search_cycle)
+              fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
+          }
+          MC_UNSET_RAW_MEM; 
           
           MC_state_set_executed_request(current_pair->graph_state, req, value);  
           mc_stats->executed_transitions++;
@@ -684,9 +730,6 @@ void MC_ddfs(){
 
             if(res == 1){ // enabled transition in automaton
 
-              if(new_pair)
-               MC_replay_liveness(mc_stack_liveness, 1); 
-
               MC_SET_RAW_MEM;
 
               next_pair = MC_pair_new();
@@ -713,8 +756,6 @@ void MC_ddfs(){
 
               MC_UNSET_RAW_MEM;
 
-              new_pair = 1;
-
               MC_ddfs();
 
             }
@@ -728,9 +769,6 @@ void MC_ddfs(){
             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
   
             if(res == 2){ // true transition in automaton
-
-              if(new_pair)
-                MC_replay_liveness(mc_stack_liveness, 1); 
             
               MC_SET_RAW_MEM;
             
@@ -758,8 +796,6 @@ void MC_ddfs(){
             
               MC_UNSET_RAW_MEM;
 
-              new_pair = 1;
-
               MC_ddfs();
 
             }
@@ -824,9 +860,6 @@ void MC_ddfs(){
 
           if(res == 1){ // enabled transition in automaton
 
-            if(new_pair)
-              MC_replay_liveness(mc_stack_liveness, 1);
-
             MC_SET_RAW_MEM;
 
             next_pair = MC_pair_new();
@@ -843,9 +876,10 @@ void MC_ddfs(){
             if(mc_stats->expanded_pairs%1000 == 0)
               XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 
-            MC_UNSET_RAW_MEM;
+            if(dot_output != NULL)
+              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
 
-            new_pair = 1;
+            MC_UNSET_RAW_MEM;
 
             MC_ddfs();
 
@@ -861,9 +895,6 @@ void MC_ddfs(){
   
           if(res == 2){ // true transition in automaton
 
-            if(new_pair)
-              MC_replay_liveness(mc_stack_liveness, 1);
-
             MC_SET_RAW_MEM;
             
             next_pair = MC_pair_new();
@@ -880,9 +911,10 @@ void MC_ddfs(){
             if(mc_stats->expanded_pairs%1000 == 0)
               XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
             
-            MC_UNSET_RAW_MEM;
+            if(dot_output != NULL)
+              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
 
-            new_pair = 1;
+            MC_UNSET_RAW_MEM;
 
             MC_ddfs();
 
@@ -914,7 +946,7 @@ void MC_ddfs(){
   xbt_dynar_free(&prop_values);
   current_pair = xbt_fifo_shift(mc_stack_liveness);
   current_pair->stack_removed = 1;
-  if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
+  if(current_pair->search_cycle){
     remove_acceptance_pair(current_pair);
   }else{
     if(_sg_mc_visited == 0)
@@ -922,6 +954,7 @@ void MC_ddfs(){
     else if(current_pair->visited_removed)
       MC_pair_delete(current_pair);
   }
+
   MC_UNSET_RAW_MEM;
 
 }