From: Martin Quinson <martin.quinson@loria.fr>
Date: Wed, 8 Feb 2012 16:15:25 +0000 (+0100)
Subject: Merge branch 'master' of scm.gforge.inria.fr:/gitroot/simgrid/simgrid
X-Git-Tag: exp_20120216~42
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/12323b05439d211235c524631170e7534abe4268?hp=599c51d596d1b8cec905af3e219023cf3bd51417

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 f6ce033da1..de95ba8c02 100644
--- 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 16425d7c63..80fbae2723 100644
--- 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 cb4ec29fe8..4bf0381230 100644
--- 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 95c08544e3..28ef0f7a5f 100644
--- 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 6b4597d6c9..8c6df80f40 100644
--- 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 8e33b31fa1..0a21025cce 100644
--- 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 c7e474dc83..9dda26d5f8 100644
--- 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
index 087692b4ac..0000000000
--- 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
index 0000000000..f07d42e409
--- /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 03794ce301..e07f48a826 100644
--- 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 bffb7e6b50..10b7691393 100644
--- 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()