model-checker : add name of program in arguments of function MSG_main_liveness_statel...

diff --git a/include/msg/msg.h b/include/msg/msg.h
index 2a92b9f..630e64b 100644 (file)
--- 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 29a7027..ce46976 100644 (file)
--- 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 a1d46eb..ec871c1 100644 (file)
--- 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 89e7892..86a9ba0 100644 (file)
--- 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 2122c9e..1cb8503 100644 (file)
--- 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();