From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Fri, 20 May 2011 16:14:01 +0000 (+0200)
Subject: MC LTL : last version dfs algorithm before reduction
X-Git-Tag: exp_20120216~133^2~90
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/6b241a6afed4a8840a1ccf2a4cc8272acd4e4ae7

MC LTL : last version dfs algorithm before reduction
---

diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c
index ba039745d1..a869fd2844 100644
--- a/src/mc/mc_dfs.c
+++ b/src/mc/mc_dfs.c
@@ -179,9 +179,8 @@ void MC_dfs_init(xbt_automaton_t a){
   xbt_state_t state = NULL;
   int res;
   xbt_transition_t transition_succ;
-  xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
-  //  int enabled_transition = 0;
+  xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
   mc_pairs_t pair_succ;
 
   xbt_dynar_foreach(a->states, cursor, state){
@@ -196,97 +195,61 @@ void MC_dfs_init(xbt_automaton_t a){
   	  mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
   	  xbt_dynar_push(successors, &mc_initial_pair);
 
-  	  //XBT_DEBUG("New initial successor");
-
   	  MC_UNSET_RAW_MEM;
 
   	}else{
-  	  if(res == 2){
-
-  	    MC_SET_RAW_MEM;
-	    
-  	    mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-  	    xbt_dynar_push(elses, &mc_initial_pair);
+	  if(res == 2){
+	 
+	    MC_SET_RAW_MEM;
 
-  	    //XBT_DEBUG("New initial successor");
+	    mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
+	    xbt_dynar_push(elses, &mc_initial_pair);
 
-  	    MC_UNSET_RAW_MEM;
-  	  }
-  	}
+	    MC_UNSET_RAW_MEM;
+	  }
+	}
       }
     }
   }
 
-  if(xbt_dynar_length(successors) > 0){
-
-    cursor = 0;
-    xbt_dynar_foreach(successors, cursor, pair_succ){
-      MC_SET_RAW_MEM;
-
-      xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+ 
+  cursor = 0;
+  xbt_dynar_foreach(successors, cursor, pair_succ){
+    MC_SET_RAW_MEM;
 
-      XBT_DEBUG("**************************************************");
-      XBT_DEBUG("Initial state=%p ", pair_succ);
+    xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 
-      MC_UNSET_RAW_MEM;
+    XBT_DEBUG("**************************************************");
+    XBT_DEBUG("Initial pair=%p (graph=%p, automaton=%p(%s)) ", pair_succ, pair_succ->graph_state, pair_succ->automaton_state,pair_succ->automaton_state->id );
 
-      set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
+    MC_UNSET_RAW_MEM;
 
-      if(cursor == 0){
-  	MC_dfs(a, 0, 0);
-  	if(pair_succ->automaton_state->type == 1){
-  	  set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);
-  	  MC_dfs(a, 1, 0);
-  	}
-      }else{
-  	MC_dfs(a, 0, 1);
-  	if(pair_succ->automaton_state->type == 1){
-  	  MC_dfs(a, 1, 1);
-  	}
-      }
+    set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
 
-      /* if(cursor == 0) */
-      /* 	MC_dfs(a, 0, 0); */
-      /* else */
-      /* 	MC_dfs(a, 0, 1); */
-      
+    if(cursor == 0){
+      MC_dfs(a, 0, 0);
+    }else{
+      MC_dfs(a, 0, 1);
     }
-
   }
 
-  if(xbt_dynar_length(elses) > 0){
-    cursor = 0;
-    xbt_dynar_foreach(elses, cursor, pair_succ){
-      MC_SET_RAW_MEM;
-
-      xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+  cursor = 0;
+  xbt_dynar_foreach(elses, cursor, pair_succ){
+    MC_SET_RAW_MEM;
 
-      XBT_DEBUG("**************************************************");
-      XBT_DEBUG("Initial state=%p ", pair_succ);
+    xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 
-      MC_UNSET_RAW_MEM;
+    XBT_DEBUG("**************************************************");
+    XBT_DEBUG("Initial pair=%p (graph=%p, automaton=%p(%s)) ", pair_succ, pair_succ->graph_state, pair_succ->automaton_state,pair_succ->automaton_state->id );
 
-      set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
+    MC_UNSET_RAW_MEM;
 
-      if(cursor == 0){
-	MC_dfs(a, 0, 0);
-	if(pair_succ->automaton_state->type == 1){
-	  set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);
-	  MC_dfs(a, 1, 0);
-	}
-      }else{
-	MC_dfs(a, 0, 1);
-	if(pair_succ->automaton_state->type == 1){
-	  MC_dfs(a, 1, 1);
-	}
-      }
+    set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
 
-      /* if(cursor == 0) */
-      /*   MC_dfs(a, 0, 0); */
-      /* else */
-      /*   MC_dfs(a, 0, 1); */
-  	
-    
+    if((xbt_dynar_length(successors) == 0) && (cursor == 0)){
+      MC_dfs(a, 0, 0);
+    }else{
+      MC_dfs(a, 0, 1);
     }
   }
   
@@ -342,6 +305,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
   //int enabled_transition = 0;
 
   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
+  xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 
   mc_pairs_t next_pair;
   mc_snapshot_t next_snapshot;
@@ -391,6 +355,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
     MC_UNSET_RAW_MEM;
 
     xbt_dynar_reset(successors);
+    xbt_dynar_reset(elses);
     
     cursor = 0;
     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
@@ -402,9 +367,14 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
 
       //XBT_DEBUG("Next pair : %p", next_pair);
 	
-      if((res == 1) || (res == 2)){ // enabled transition in automaton
+      if(res == 1){ // enabled transition in automaton
 	xbt_dynar_push(successors, &next_pair);
 	mc_stats_pair->expanded_pairs++;
+      }else{
+	if(res == 2){ // enabled transition in automaton
+	  xbt_dynar_push(elses, &next_pair);
+	  mc_stats_pair->expanded_pairs++;
+	}
       }
 
       MC_UNSET_RAW_MEM;
@@ -421,62 +391,105 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
 	
     }
 
-    // XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors));
-    //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses));
 
-    if(xbt_dynar_length(successors) >0){
+    cursor = 0;
+    xbt_dynar_foreach(successors, cursor, pair_succ){
 
-      cursor = 0;
-      xbt_dynar_foreach(successors, cursor, pair_succ){
+      //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
+
+      if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
+	XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+	XBT_INFO("|             ACCEPTANCE CYCLE            |");
+	XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+	XBT_INFO("Counter-example that violates formula :");
+	MC_show_snapshot_stack(mc_snapshot_stack);
+	MC_dump_snapshot_stack(mc_snapshot_stack);
+	MC_print_statistics_pairs(mc_stats_pair);
+	exit(0);
+      }
+	
+      if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
 
-	//XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
+	//XBT_DEBUG("Unvisited pair !");
+
+	mc_stats_pair->executed_transitions++;
+ 
+	MC_SET_RAW_MEM;
+	xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+	MC_UNSET_RAW_MEM;
+
+	set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
+	MC_dfs(a, search_cycle, 0);
+
+	if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
+
+	  MC_restore_snapshot(current_pair->system_state);
+	  MC_UNSET_RAW_MEM;
+ 
+	  xbt_swag_foreach(process, simix_global->process_list){
+	    if(MC_process_is_enabled(process)){
+	      //XBT_DEBUG("Pid : %lu", process->pid);
+	      MC_state_interleave_process(current_pair->graph_state, process);
+	    }
+	  }
+	    
+	  set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
+	  XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
+	  MC_dfs(a, 1, 1);
 
-	if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
-	  XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-	  XBT_INFO("|             ACCEPTANCE CYCLE            |");
-	  XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-	  XBT_INFO("Counter-example that violates formula :");
-	  MC_show_snapshot_stack(mc_snapshot_stack);
-	  MC_dump_snapshot_stack(mc_snapshot_stack);
-	  MC_print_statistics_pairs(mc_stats_pair);
-	  exit(0);
 	}
+      }
+    }
+
+    cursor = 0;
+    xbt_dynar_foreach(elses, cursor, pair_succ){
+
+      //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
+
+      if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
+	XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+	XBT_INFO("|             ACCEPTANCE CYCLE            |");
+	XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+	XBT_INFO("Counter-example that violates formula :");
+	MC_show_snapshot_stack(mc_snapshot_stack);
+	MC_dump_snapshot_stack(mc_snapshot_stack);
+	MC_print_statistics_pairs(mc_stats_pair);
+	exit(0);
+      }
 	
-	if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
+      if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
 
-	  //XBT_DEBUG("Unvisited pair !");
+	//XBT_DEBUG("Unvisited pair !");
 
-	  mc_stats_pair->executed_transitions++;
+	mc_stats_pair->executed_transitions++;
  
-	  MC_SET_RAW_MEM;
-	  xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
-	  MC_UNSET_RAW_MEM;
+	MC_SET_RAW_MEM;
+	xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+	MC_UNSET_RAW_MEM;
 
-	  set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
-	  MC_dfs(a, search_cycle, 0);
+	set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
+	MC_dfs(a, search_cycle, 0);
 
-	  if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
+	if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 
-	    MC_restore_snapshot(current_pair->system_state);
-	    MC_UNSET_RAW_MEM;
+	  MC_restore_snapshot(current_pair->system_state);
+	  MC_UNSET_RAW_MEM;
  
-	    xbt_swag_foreach(process, simix_global->process_list){
-	      if(MC_process_is_enabled(process)){
-	    	//XBT_DEBUG("Pid : %lu", process->pid);
-	    	MC_state_interleave_process(current_pair->graph_state, process);
-	      }
+	  xbt_swag_foreach(process, simix_global->process_list){
+	    if(MC_process_is_enabled(process)){
+	      //XBT_DEBUG("Pid : %lu", process->pid);
+	      MC_state_interleave_process(current_pair->graph_state, process);
 	    }
+	  }
 	    
-	    set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
-	    XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-	    MC_dfs(a, 1, 1);
+	  set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
+	  XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
+	  MC_dfs(a, 1, 1);
 
-	  }
 	}
       }
-    
     }
-
+    
     
     if(MC_state_interleave_size(current_pair->graph_state) > 0){
       MC_restore_snapshot(current_snapshot);