X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/24e5543a2803412d6edeb3ace5ecf0fc87de7cd4..5a9c70d5dfe11c9c7660b795b00f49b4170da968:/src/mc/mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index f28b56fd1d..0e8d494993 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -53,34 +53,6 @@ void set_pair_reached(mc_pair_t pair){
 
 }
 
-void MC_show_snapshot_stack(xbt_fifo_t stack){
-  int value;
-  mc_pair_t pair;
-  xbt_fifo_item_t item;
-  smx_req_t req;
-  char *req_str = NULL;
-  
-  for (item = xbt_fifo_get_last_item(stack);
-       (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
-        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
-    req = MC_state_get_executed_request(pair->graph_state, &value);
-    if(req){
-      req_str = MC_request_to_string(req, value);
-      XBT_INFO("%s", req_str);
-      xbt_free(req_str);
-    }
-  }
-}
-
-void MC_dump_snapshot_stack(xbt_fifo_t stack){
-  mc_pair_t pair;
-
-  MC_SET_RAW_MEM;
-  while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
-    MC_pair_delete(pair);
-  MC_UNSET_RAW_MEM;
-}
-
 void MC_pair_delete(mc_pair_t pair){
   xbt_free(pair->graph_state->proc_status);
   xbt_free(pair->graph_state);
@@ -175,10 +147,10 @@ int visited(mc_pair_t pair, int sc){
 }
 
 
-void MC_vddfs_with_restore_snapshot_init(xbt_automaton_t a){
+void MC_vddfs_stateful_init(xbt_automaton_t a){
 
   XBT_DEBUG("**************************************************");
-  XBT_DEBUG("Double-DFS with visited state and restore snapshot init");
+  XBT_DEBUG("Double-DFS stateful with visited state init");
   XBT_DEBUG("**************************************************");
  
   mc_pair_t mc_initial_pair;
@@ -255,36 +227,36 @@ void MC_vddfs_with_restore_snapshot_init(xbt_automaton_t a){
   xbt_dynar_foreach(successors, cursor, pair_succ){
     MC_SET_RAW_MEM;
 
-    xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+    xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
     set_pair_visited(pair_succ, 0);
 
     MC_UNSET_RAW_MEM;
 
     if(cursor == 0){
-      MC_vddfs_with_restore_snapshot(a, 0, 0);
+      MC_vddfs_stateful(a, 0, 0);
     }else{
-      MC_vddfs_with_restore_snapshot(a, 0, 1);
+      MC_vddfs_stateful(a, 0, 1);
     }
   }  
 }
 
 
-void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
+void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 
   smx_process_t process = NULL;
 
 
-  if(xbt_fifo_size(mc_snapshot_stack) == 0)
+  if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
     return;
 
   if(restore == 1){
-    MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
+    MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
     MC_UNSET_RAW_MEM;
   }
 
 
   /* Get current state */
-  mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+  mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 
   if(restore==1){
     xbt_swag_foreach(process, simix_global->process_list){
@@ -396,8 +368,8 @@ void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int res
 	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_show_stack_liveness_stateful(mc_stack_liveness_stateful);
+	MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 	MC_print_statistics_pairs(mc_stats_pair);
 	exit(0);
       }
@@ -407,11 +379,11 @@ void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int res
 	mc_stats_pair->executed_transitions++;
  
 	MC_SET_RAW_MEM;
-	xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+	xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 	set_pair_visited(pair_succ, search_cycle);
 	MC_UNSET_RAW_MEM;
 
-	MC_vddfs_with_restore_snapshot(a, search_cycle, 0);
+	MC_vddfs_stateful(a, search_cycle, 0);
 
 	if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 
@@ -426,7 +398,7 @@ void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int res
 	    
 	  set_pair_reached(current_pair);
 	  XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-	  MC_vddfs_with_restore_snapshot(a, 1, 1);
+	  MC_vddfs_stateful(a, 1, 1);
 
 	}
       }else{
@@ -445,7 +417,7 @@ void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int res
 
   
   MC_SET_RAW_MEM;
-  xbt_fifo_shift(mc_snapshot_stack);
+  xbt_fifo_shift(mc_stack_liveness_stateful);
   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
   MC_UNSET_RAW_MEM;
 
@@ -453,12 +425,13 @@ void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int res
 
 
 
-/********************* Double-DFS without visited state *******************/
+/********************* Double-DFS stateful without visited state *******************/
+
 
-void MC_ddfs_with_restore_snapshot_init(xbt_automaton_t a){
+void MC_ddfs_stateful_init(xbt_automaton_t a){
 
   XBT_DEBUG("**************************************************");
-  XBT_DEBUG("Double-DFS without visited state and with restore snapshot init");
+  XBT_DEBUG("Double-DFS stateful without visited state init");
   XBT_DEBUG("**************************************************");
  
   mc_pair_t mc_initial_pair;
@@ -534,35 +507,35 @@ void MC_ddfs_with_restore_snapshot_init(xbt_automaton_t a){
   xbt_dynar_foreach(successors, cursor, pair_succ){
     MC_SET_RAW_MEM;
 
-    xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+    xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 
     MC_UNSET_RAW_MEM;
 
     if(cursor == 0){
-      MC_ddfs_with_restore_snapshot(a, 0, 0);
+      MC_ddfs_stateful(a, 0, 0);
     }else{
-      MC_ddfs_with_restore_snapshot(a, 0, 1);
+      MC_ddfs_stateful(a, 0, 1);
     }
   }  
 }
 
 
-void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
+void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 
   smx_process_t process = NULL;
 
 
-  if(xbt_fifo_size(mc_snapshot_stack) == 0)
+  if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
     return;
 
   if(restore == 1){
-    MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
+    MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
     MC_UNSET_RAW_MEM;
   }
 
 
   /* Get current state */
-  mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+  mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 
   if(restore==1){
     xbt_swag_foreach(process, simix_global->process_list){
@@ -674,8 +647,8 @@ void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int rest
 	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_show_stack_liveness_stateful(mc_stack_liveness_stateful);
+	MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 	MC_print_statistics_pairs(mc_stats_pair);
 	exit(0);
       }
@@ -683,10 +656,10 @@ void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int rest
       mc_stats_pair->executed_transitions++;
  
       MC_SET_RAW_MEM;
-      xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+      xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
       MC_UNSET_RAW_MEM;
 
-      MC_ddfs_with_restore_snapshot(a, search_cycle, 0);
+      MC_ddfs_stateful(a, search_cycle, 0);
 
       if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 
@@ -701,7 +674,7 @@ void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int rest
 	    
 	set_pair_reached(current_pair);
 	XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-	MC_ddfs_with_restore_snapshot(a, 1, 1);
+	MC_ddfs_stateful(a, 1, 1);
 
       }
     }
@@ -715,8 +688,154 @@ void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int rest
 
   
   MC_SET_RAW_MEM;
-  xbt_fifo_shift(mc_snapshot_stack);
+  xbt_fifo_shift(mc_stack_liveness_stateful);
   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
   MC_UNSET_RAW_MEM;
 
 }
+
+
+
+/********************* Double-DFS stateless *******************/
+
+void MC_pair_stateless_delete(mc_pair_stateless_t pair){
+  xbt_free(pair->graph_state->proc_status);
+  xbt_free(pair->graph_state);
+  //xbt_free(pair->automaton_state); -> FIXME : à implémenter
+  xbt_free(pair);
+}
+
+mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
+  mc_pair_stateless_t p = NULL;
+  p = xbt_new0(s_mc_pair_stateless_t, 1);
+  p->automaton_state = st;
+  p->graph_state = sg;
+  mc_stats_pair->expanded_pairs++;
+  return p;
+}
+
+
+int reached_stateless(mc_pair_stateless_t pair){
+
+  char* hash_reached = malloc(sizeof(char)*160);
+  unsigned int c= 0;
+
+  MC_SET_RAW_MEM;
+  char *hash = malloc(sizeof(char)*160);
+  xbt_sha((char *)&pair, hash);
+  xbt_dynar_foreach(reached_pairs, c, hash_reached){
+    if(strcmp(hash, hash_reached) == 0){
+      MC_UNSET_RAW_MEM;
+      return 1;
+    }
+  }
+  
+  MC_UNSET_RAW_MEM;
+  return 0;
+}
+
+void set_pair_stateless_reached(mc_pair_stateless_t pair){
+
+  if(reached_stateless(pair) == 0){
+    MC_SET_RAW_MEM;
+    char *hash = malloc(sizeof(char)*160) ;
+    xbt_sha((char *)&pair, hash);
+    xbt_dynar_push(reached_pairs, &hash); 
+    MC_UNSET_RAW_MEM;
+  }
+
+}
+
+
+void MC_ddfs_stateless_init(xbt_automaton_t a){
+
+  XBT_DEBUG("**************************************************");
+  XBT_DEBUG("Double-DFS without visited state and with restore snapshot init");
+  XBT_DEBUG("**************************************************");
+ 
+  mc_pair_stateless_t mc_initial_pair;
+  mc_state_t initial_graph_state;
+  smx_process_t process; 
+ 
+  MC_wait_for_requests();
+
+  MC_SET_RAW_MEM;
+
+  initial_graph_state = MC_state_pair_new();
+  xbt_swag_foreach(process, simix_global->process_list){
+    if(MC_process_is_enabled(process)){
+      MC_state_interleave_process(initial_graph_state, process);
+    }
+  }
+
+  reached_pairs = xbt_dynar_new(sizeof(char *), NULL); 
+
+  MC_UNSET_RAW_MEM; 
+
+  /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système 
+    -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
+
+  unsigned int cursor = 0;
+  unsigned int cursor2 = 0;
+  xbt_state_t state = NULL;
+  int res;
+  xbt_transition_t transition_succ;
+  xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
+  mc_pair_stateless_t pair_succ;
+
+  xbt_dynar_foreach(a->states, cursor, state){
+    if(state->type == -1){
+      xbt_dynar_foreach(state->out, cursor2, transition_succ){
+  	res = MC_automaton_evaluate_label(a, transition_succ->label);
+	
+  	if((res == 1) || (res == 2)){
+	 
+  	  MC_SET_RAW_MEM;
+
+  	  mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
+  	  xbt_dynar_push(successors, &mc_initial_pair);
+
+  	  MC_UNSET_RAW_MEM;
+
+	}
+      }
+    }
+  }
+
+  cursor = 0;
+
+  if(xbt_dynar_length(successors) == 0){
+    xbt_dynar_foreach(a->states, cursor, state){
+      if(state->type == -1){
+	MC_SET_RAW_MEM;
+
+	mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
+	xbt_dynar_push(successors, &mc_initial_pair);
+	
+	MC_UNSET_RAW_MEM;
+      }
+    }
+  }
+
+  cursor = 0;
+  xbt_dynar_foreach(successors, cursor, pair_succ){
+    MC_SET_RAW_MEM;
+
+    xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+
+    MC_UNSET_RAW_MEM;
+
+    if(cursor == 0){
+      MC_ddfs_stateless(a, 0, 0);
+    }else{
+      MC_ddfs_stateless(a, 0, 1);
+    }
+  }  
+}
+
+
+void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int restore){
+
+ 
+}
+