X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f74d34bb1e9ca987d4f0616eb1429bb74f1bff33..e6bc6eb53997f4648bf3207348c060e9f50ee282:/src/mc/mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 211f26bbd1..4876944315 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -12,12 +12,37 @@
 #include "../simix/smx_private.h"
 #include "xbt/fifo.h"
 #include "mc_private.h"
-#include "xbt/automaton/automaton_create.h"
+#include "xbt/automaton.h"
 
 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
                                 "Logging specific to MC (global)");
 
+/* Configuration support */
+e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
+
+void _mc_cfg_cb_reduce(const char *name, int pos) {
+  char *val= xbt_cfg_get_string(_surf_cfg_set, name);
+  if (!strcasecmp(val,"none")) {
+    mc_reduce_kind = e_mc_reduce_none;
+  } else if (!strcasecmp(val,"dpor")) {
+    mc_reduce_kind = e_mc_reduce_dpor;
+  } else {
+    xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
+  }
+  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+}
+
+void _mc_cfg_cb_checkpoint(const char *name, int pos) {
+  _surf_mc_checkpoint = xbt_cfg_get_int(_surf_cfg_set, name);
+  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+}
+void _mc_cfg_cb_property(const char *name, int pos) {
+  _surf_mc_property_file= xbt_cfg_get_string(_surf_cfg_set, name);
+  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+}
+
+
 /* MC global data structures */
 
 mc_state_t mc_current_state = NULL;
@@ -36,11 +61,28 @@ mc_stats_pair_t mc_stats_pair = NULL;
 xbt_fifo_t mc_stack_liveness = NULL;
 mc_snapshot_t initial_snapshot_liveness = NULL;
 
-xbt_automaton_t automaton;
+xbt_automaton_t _mc_property_automaton = NULL;
 
-static void MC_init_liveness(xbt_automaton_t a);
 static void MC_assert_pair(int prop);
 
+void MC_do_the_modelcheck_for_real() {
+  if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') {
+    if (mc_reduce_kind==e_mc_reduce_unset)
+      mc_reduce_kind=e_mc_reduce_dpor;
+
+    XBT_INFO("Check a safety property");
+    MC_modelcheck();
+
+  } else  {
+
+    if (mc_reduce_kind==e_mc_reduce_unset)
+      mc_reduce_kind=e_mc_reduce_none;
+
+    XBT_INFO("Check the liveness property %s",_surf_mc_property_file);
+    MC_automaton_load(_surf_mc_property_file);
+    MC_modelcheck_liveness();
+  }
+}
 
 /**
  *  \brief Initialize the model-checker data structures
@@ -78,8 +120,15 @@ void MC_init_safety(void)
 }
 
 
-static void MC_init_liveness(xbt_automaton_t a){
+void MC_modelcheck(void)
+{
+  MC_init_safety();
+  MC_dpor();
+  MC_exit();
+}
 
+void MC_modelcheck_liveness(){
+  /* init stuff */
   XBT_DEBUG("Start init mc");
   
   mc_time = xbt_new0(double, simix_process_maxpid);
@@ -99,30 +148,10 @@ static void MC_init_liveness(xbt_automaton_t a){
 
   MC_UNSET_RAW_MEM;
 
-  automaton = a;
 
   MC_ddfs_init();
 
-  
-}
-
-
-void MC_modelcheck(void)
-{
-  MC_init_safety();
-  MC_dpor();
-  MC_exit();
-}
-
-
-
-void MC_modelcheck_liveness(xbt_automaton_t a){
-  MC_init_liveness(a);
-  MC_exit_liveness();
-}
-
-void MC_exit_liveness(void)
-{
+  /* We're done */
   MC_print_statistics_pairs(mc_stats_pair);
   //xbt_free(mc_time);
   //MC_memory_exit();
@@ -356,7 +385,7 @@ void MC_dump_stack_safety(xbt_fifo_t stack)
 
   MC_show_stack_safety(stack);
 
-  if(!_surf_do_mc_checkpoint){
+  if(!_surf_mc_checkpoint){
 
     mc_state_t state;
 
@@ -531,9 +560,19 @@ void MC_diff(void){
 
 }
 
-xbt_automaton_t MC_create_automaton(const char *file){
+void MC_automaton_load(const char *file){
+  MC_SET_RAW_MEM;
+
+  if (_mc_property_automaton == NULL)
+    _mc_property_automaton = xbt_automaton_new();
+  xbt_automaton_load(_mc_property_automaton,file);
+
+  MC_UNSET_RAW_MEM;
+}
+void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
   MC_SET_RAW_MEM;
-  xbt_automaton_t a = xbt_create_automaton(file);
+  if (_mc_property_automaton == NULL)
+    _mc_property_automaton = xbt_automaton_new();
+  xbt_new_propositional_symbol(_mc_property_automaton,id,fct);
   MC_UNSET_RAW_MEM;
-  return a;
 }