From 8449f8cd86a230453d0621072573d85c7ac611f4 Mon Sep 17 00:00:00 2001
From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Mon, 14 Nov 2011 17:14:30 +0100
Subject: [PATCH 1/1] model-checker : add name of program in arguments of
 function MSG_main_liveness_stateless, MC_modelcheck_liveness_stateless,
 MC_init_liveness_stateless, MC_ddfs_stateless_init and MC_ddfs_stateless

---
 include/msg/msg.h   |  2 +-
 src/include/mc/mc.h |  4 ++--
 src/mc/mc_global.c  | 10 +++++-----
 src/mc/private.h    |  7 ++++---
 src/msg/global.c    |  4 ++--
 5 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/include/msg/msg.h b/include/msg/msg.h
index 2a92b9f050..630e64b1ab 100644
--- a/include/msg/msg.h
+++ b/include/msg/msg.h
@@ -24,7 +24,7 @@ XBT_PUBLIC(int) MSG_get_channel_number(void);
 XBT_PUBLIC(MSG_error_t) MSG_main(void);
 XBT_PUBLIC(MSG_error_t) MSG_main_stateful(void);
 XBT_PUBLIC(MSG_error_t) MSG_main_liveness_stateful(xbt_automaton_t a);
-XBT_PUBLIC(MSG_error_t) MSG_main_liveness_stateless(xbt_automaton_t a);
+XBT_PUBLIC(MSG_error_t) MSG_main_liveness_stateless(xbt_automaton_t a, char *prgm);
 XBT_PUBLIC(MSG_error_t) MSG_clean(void);
 XBT_PUBLIC(void) MSG_function_register(const char *name,
                                        xbt_main_func_t code);
diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 29a70270d8..ce4697626f 100644
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -31,7 +31,7 @@ SG_BEGIN_DECL()
 XBT_PUBLIC(void) MC_init_safety_stateless(void);
 XBT_PUBLIC(void) MC_init_safety_stateful(void);
 XBT_PUBLIC(void) MC_init_liveness_stateful(xbt_automaton_t a);
-XBT_PUBLIC(void) MC_init_liveness_stateless(xbt_automaton_t a);
+XBT_PUBLIC(void) MC_init_liveness_stateless(xbt_automaton_t a, char *prgm);
 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_exit_liveness(void);
 XBT_PUBLIC(void) MC_assert(int);
@@ -41,7 +41,7 @@ XBT_PUBLIC(void) MC_assert_pair_stateless(int);
 XBT_PUBLIC(void) MC_modelcheck(void);
 XBT_PUBLIC(void) MC_modelcheck_stateful(void);
 XBT_PUBLIC(void) MC_modelcheck_liveness_stateful(xbt_automaton_t a);
-XBT_PUBLIC(void) MC_modelcheck_liveness_stateless(xbt_automaton_t a);
+XBT_PUBLIC(void) MC_modelcheck_liveness_stateless(xbt_automaton_t a, char *prgm);
 XBT_PUBLIC(int) MC_random(int, int);
 XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
 XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index a1d46ebbfb..ec871c133e 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -116,12 +116,12 @@ void MC_init_liveness_stateful(xbt_automaton_t a){
 
   MC_UNSET_RAW_MEM;
 
-  MC_ddfs_stateful_init(a);
+  //MC_ddfs_stateful_init(a);
   //MC_dpor2_init(a);
   //MC_dpor3_init(a);
 }
 
-void MC_init_liveness_stateless(xbt_automaton_t a){
+void MC_init_liveness_stateless(xbt_automaton_t a, char *prgm){
 
   XBT_DEBUG("Start init mc");
   
@@ -142,7 +142,7 @@ void MC_init_liveness_stateless(xbt_automaton_t a){
 
   MC_UNSET_RAW_MEM;
 
-  MC_ddfs_stateless_init(a);
+  MC_ddfs_stateless_init(a, prgm);
 
   
 }
@@ -167,8 +167,8 @@ void MC_modelcheck_liveness_stateful(xbt_automaton_t a){
   MC_exit_liveness();
 }
 
-void MC_modelcheck_liveness_stateless(xbt_automaton_t a){
-  MC_init_liveness_stateless(a);
+void MC_modelcheck_liveness_stateless(xbt_automaton_t a, char *prgm){
+  MC_init_liveness_stateless(a, prgm);
   MC_exit_liveness();
 }
 
diff --git a/src/mc/private.h b/src/mc/private.h
index 89e78929c6..86a9ba04f7 100644
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -36,6 +36,7 @@ typedef struct s_mc_snapshot{
 } s_mc_snapshot_t, *mc_snapshot_t;
 
 void MC_take_snapshot(mc_snapshot_t);
+void MC_take_snapshot_liveness(mc_snapshot_t s, char *prgm);
 void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);
 
@@ -44,7 +45,7 @@ extern double *mc_time;
 
 /* Bound of the MC depth-first search algorithm */
 #define MAX_DEPTH 1000
-#define MAX_DEPTH_LIVENESS 150
+#define MAX_DEPTH_LIVENESS 1000
 
 int MC_deadlock_check(void);
 void MC_replay(xbt_fifo_t stack);
@@ -248,8 +249,8 @@ typedef struct s_mc_pair_stateless{
 extern xbt_fifo_t mc_stack_liveness_stateless;
 
 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r);
-void MC_ddfs_stateless_init(xbt_automaton_t a);
-void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay);
+void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm);
+void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *prgm);
 void MC_show_stack_liveness_stateless(xbt_fifo_t stack);
 void MC_dump_stack_liveness_stateless(xbt_fifo_t stack);
 void MC_pair_stateless_delete(mc_pair_stateless_t pair);
diff --git a/src/msg/global.c b/src/msg/global.c
index 2122c9eff6..1cb8503102 100644
--- a/src/msg/global.c
+++ b/src/msg/global.c
@@ -183,14 +183,14 @@ MSG_error_t MSG_main_liveness_stateful(xbt_automaton_t a)
   return MSG_OK;
 }
 
-MSG_error_t MSG_main_liveness_stateless(xbt_automaton_t a)
+MSG_error_t MSG_main_liveness_stateless(xbt_automaton_t a, char *prgm)
 {
   /* Clean IO before the run */
   fflush(stdout);
   fflush(stderr);
 
   if (MC_IS_ENABLED) {
-    MC_modelcheck_liveness_stateless(a);
+    MC_modelcheck_liveness_stateless(a, prgm);
   }
   else {
     SIMIX_run();
-- 
2.20.1