model-check : show stack when property not valid

diff --git a/examples/msg/mc/example_automaton.c b/examples/msg/mc/example_automaton.c
index a4c9572..fbf546a 100644 (file)
--- a/examples/msg/mc/example_automaton.c
+++ b/examples/msg/mc/example_automaton.c
@@ -6,7 +6,7 @@
 
 #include "y.tab.c"
 
-#define N 5
+#define N 3
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "Example with automaton");
 
@@ -14,7 +14,7 @@ extern xbt_automaton_t automaton;
 
 
 int d=1;
-int r=1;
+int r=0;
 int e=1;
 
 int predD(){
@@ -40,10 +40,10 @@ int server(int argc, char *argv[])
     }
     MSG_task_receive(&task, "mymailbox");
     count++;
-    r=(r+1)%4;
+    //r=(r+1)%4;
      
   }
-  MC_assert(atoi(MSG_task_get_name(task)) == 3);
+  MC_assert_pair(atoi(MSG_task_get_name(task)) == 3);
 
   XBT_INFO("OK");
   return 0;
@@ -59,7 +59,7 @@ int client(int argc, char *argv[])
   MSG_task_send(task, "mymailbox");
   
   XBT_INFO("Sent!");
-   r=(r+1)%4;
+   //r=(r+1)%4;
   return 0;
 }
 

diff --git a/include/mc/modelchecker.h b/include/mc/modelchecker.h
index 2ca38fa..dd65adb 100644 (file)
--- a/include/mc/modelchecker.h
+++ b/include/mc/modelchecker.h
@@ -1,4 +1,5 @@
 #include "xbt.h"
 
 XBT_PUBLIC(void) MC_assert(int);
+XBT_PUBLIC(void) MC_assert_pair(int);
 XBT_PUBLIC(int) MC_random(int min, int max);

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index c715276..06cc3eb 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -32,6 +32,7 @@ XBT_PUBLIC(void) MC_init(void);
 XBT_PUBLIC(void) MC_init_with_automaton(xbt_automaton_t a);
 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_assert(int);
+XBT_PUBLIC(void) MC_assert_pair(int);
 XBT_PUBLIC(void) MC_modelcheck(void);
 XBT_PUBLIC(void) MC_modelcheck_with_automaton(xbt_automaton_t a);
 XBT_PUBLIC(int) MC_random(int, int);

diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c
index 01d4313..246b21b 100644 (file)
--- a/src/mc/mc_dfs.c
+++ b/src/mc/mc_dfs.c
@@ -454,7 +454,6 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
   //XBT_DEBUG("State shifted in snapshot_stack, mc_snapshot_stack size=%d", xbt_fifo_size(mc_snapshot_stack));
   MC_UNSET_RAW_MEM;
 
-
 }
 
 void MC_show_snapshot_stack(xbt_fifo_t stack){

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index fc018b8..85770ea 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -268,6 +268,19 @@ void MC_assert(int prop)
   }
 }
 
+void MC_assert_pair(int prop){
+  if (MC_IS_ENABLED && !prop) {
+    XBT_INFO("**************************");
+    XBT_INFO("*** PROPERTY NOT VALID ***");
+    XBT_INFO("**************************");
+    XBT_INFO("Counter-example execution trace:");
+    MC_show_snapshot_stack(mc_snapshot_stack);
+    MC_dump_snapshot_stack(mc_snapshot_stack);
+    //MC_print_statistics(mc_stats);
+    xbt_abort();
+  }
+}
+
 void MC_process_clock_add(smx_process_t process, double amount)
 {
   mc_time[process->pid] += amount;

diff --git a/src/mc/private.h b/src/mc/private.h
index 688298e..ee8df4e 100644 (file)
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -203,4 +203,5 @@ void MC_show_snapshot_stack(xbt_fifo_t stack);
 void MC_dump_snapshot_stack(xbt_fifo_t stack);
 void MC_pair_delete(mc_pairs_t pair);
 
+
 #endif