Merge branch 'master' of scm.gforge.inria.fr:/gitroot/simgrid/simgrid

diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c
index f6ce033..de95ba8 100644 (file)
--- a/examples/msg/chord/chord.c
+++ b/examples/msg/chord/chord.c
@@ -9,8 +9,7 @@
 #include "msg/msg.h"
 #include "xbt/log.h"
 #include "xbt/asserts.h"
-#include "mc/modelchecker.h"
-#include "mc/mc.h"
+#include "simgrid/modelchecker.h"
 #include "xbt/xbt_os_time.h"
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(msg_chord,

diff --git a/examples/msg/mc/bugged1.c b/examples/msg/mc/bugged1.c
index 16425d7..80fbae2 100644 (file)
--- a/examples/msg/mc/bugged1.c
+++ b/examples/msg/mc/bugged1.c
@@ -4,7 +4,7 @@
 /******************************************************************************/
 
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 #define N 3
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");

diff --git a/examples/msg/mc/bugged1_stateful.c b/examples/msg/mc/bugged1_stateful.c
index cb4ec29..4bf0381 100644 (file)
--- a/examples/msg/mc/bugged1_stateful.c
+++ b/examples/msg/mc/bugged1_stateful.c
@@ -4,7 +4,7 @@
 /******************************************************************************/
 
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 #define N 3
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");
@@ -62,4 +62,4 @@ int main(int argc, char *argv[])
    
   return 0;
 
-}
\ No newline at end of file
+}

diff --git a/examples/msg/mc/bugged2.c b/examples/msg/mc/bugged2.c
index 95c0854..28ef0f7 100644 (file)
--- a/examples/msg/mc/bugged2.c
+++ b/examples/msg/mc/bugged2.c
@@ -4,7 +4,7 @@
 /******************************************************************************/
 
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 #define N 3
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");

diff --git a/examples/msg/mc/bugged2_stateful.c b/examples/msg/mc/bugged2_stateful.c
index 6b4597d..8c6df80 100644 (file)
--- a/examples/msg/mc/bugged2_stateful.c
+++ b/examples/msg/mc/bugged2_stateful.c
@@ -4,7 +4,7 @@
 /******************************************************************************/
 
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 #define N 3
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");

diff --git a/examples/msg/mc/bugged3.c b/examples/msg/mc/bugged3.c
index 8e33b31..0a21025 100644 (file)
--- a/examples/msg/mc/bugged3.c
+++ b/examples/msg/mc/bugged3.c
@@ -8,7 +8,7 @@
 /******************************************************************************/
 
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "this example");
 

diff --git a/examples/msg/mc/random_test.c b/examples/msg/mc/random_test.c
index c7e474d..9dda26d 100644 (file)
--- a/examples/msg/mc/random_test.c
+++ b/examples/msg/mc/random_test.c
@@ -1,5 +1,5 @@
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(random_test, "Random Test");
 

diff --git a/include/mc/modelchecker.h b/include/mc/modelchecker.h
deleted file mode 100644 (file)
index 087692b..0000000
--- a/include/mc/modelchecker.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#include "xbt.h"
-
-XBT_PUBLIC(void) MC_assert(int);
-XBT_PUBLIC(void) MC_assert_stateful(int);
-XBT_PUBLIC(int) MC_random(int min, int max);
-XBT_PUBLIC(void) MC_diff();

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
new file mode 100644 (file)
index 0000000..f07d42e
--- /dev/null
+++ b/include/simgrid/modelchecker.h
@@ -0,0 +1,34 @@
+/* simgrid/modelchecker.h - Formal Verification made possible in SimGrid    */
+
+/* Copyright (c) 2008-2012. The SimGrid Team. All rights reserved.          */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <simgrid_config.h> /* HAVE_MC ? */
+#include <xbt.h>
+
+#ifndef SIMGRID_MODELCHECKER_H
+#define SIMGRID_MODELCHECKER_H
+
+#ifdef HAVE_MC
+
+extern int _surf_do_model_check;
+#define MC_IS_ENABLED _surf_do_model_check
+
+XBT_PUBLIC(void) MC_assert(int);
+XBT_PUBLIC(void) MC_assert_stateful(int);
+XBT_PUBLIC(int) MC_random(int min, int max);
+XBT_PUBLIC(void) MC_diff();
+
+#else
+
+#define MC_IS_ENABLED 0
+#define MC_assert(a) xbt_assert(a)
+#define MC_assert_stateful(a) xbt_assert(a)
+
+#endif
+
+
+
+#endif /* SIMGRID_MODELCHECKER_H */

diff --git a/include/simgrid_config.h.in b/include/simgrid_config.h.in
index 03794ce..e07f48a 100644 (file)
--- a/include/simgrid_config.h.in
+++ b/include/simgrid_config.h.in
@@ -132,6 +132,8 @@ XBT_PUBLIC(char *) bprintf(const char *fmt, ...) _XBT_GNUC_PRINTF(1, 2);
 /* If __thread is available */
 #cmakedefine HAVE_THREAD_LOCAL_STORAGE @HAVE_THREAD_LOCAL_STORAGE@
 
+/* If Model-Checking support was requested */
+#cmakedefine HAVE_MC @HAVE_MC@
 
 SG_END_DECL()
 #endif /* SIMGRID_PUBLIC_CONFIG_H */

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index bffb7e6..10b7691 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -12,15 +12,9 @@
 #include "xbt/function_types.h"
 #include "mc/datatypes.h"
 #include "simix/datatypes.h"
-#include "gras_config.h" /* Definition of HAVE_MC */
+#include "simgrid/modelchecker.h" /* our public interface (and definition of HAVE_MC) */
 #include "xbt/automaton.h"
 
-#ifdef HAVE_MC
-extern int _surf_do_model_check;
-#define MC_IS_ENABLED _surf_do_model_check
-#else
-#define MC_IS_ENABLED 0
-#endif
 
 SG_BEGIN_DECL()