Merge branch 'master' into deterministicScheds

resources/3rdparty/gmm-5.2/include/gmm/gmm_blas.h

@@ -44,7 +44,7 @@
 
 #ifdef STORM_HAVE_INTELTBB
 #include <new> // This fixes a potential dependency ordering problem between GMM and TBB
-#include "tbb/tbb.h"
+#include "storm/adapters/IntelTbbAdapter.h"
 #include <iterator>
 #endif
 

src/storm-cli-utilities/cli.cpp

@@ -17,9 +17,8 @@
 
 
 // Includes for the linked libraries and versions header.
-#ifdef STORM_HAVE_INTELTBB
-#	include "tbb/tbb_stddef.h"
-#endif
+#include "storm/adapters/IntelTbbAdapter.h"
+
 #ifdef STORM_HAVE_GLPK
 #	include "glpk.h"
 #endif

src/storm/adapters/IntelTbbAdapter.h

@@ -0,0 +1,32 @@
+#pragma once
+
+// To detect whether the usage of TBB is possible, this include is neccessary
+#include "storm-config.h"
+
+
+/* On macOS, TBB includes the header
+ * /Library/Developer/CommandLineTools/SDKs/MacOSX10.14.sdk/usr/include/mach/boolean.h
+ * which #defines macros TRUE and FALSE. Since these also occur as identifiers, we #undef them after including TBB.
+ * We still issue a warning in case these macros have been defined before.
+*/
+
+#ifdef TRUE
+#warning "Undefining previously defined macro 'TRUE'."
+#endif
+
+#ifdef FALSE
+#warning "Undefining previously defined macro 'FALSE'."
+#endif
+
+#ifdef STORM_HAVE_INTELTBB
+#include "tbb/tbb.h"
+#include "tbb/tbb_stddef.h"
+#endif
+
+#ifdef TRUE
+#undef TRUE
+#endif
+
+#ifdef FALSE
+#undef FALSE
+#endif

src/storm/adapters/RationalFunctionAdapter.h

@@ -9,27 +9,6 @@
 #include <carl/core/Relation.h>
 #include <carl/util/stringparser.h>
 
-// Some header files on macOS (included via INTEL TBB) might #define TRUE and FALSE, which in carl/formula/Formula.h are used as FormulaTypes.
-// Hence, we temporarily #undef these:
-#ifdef TRUE
-#define STORM_TEMP_TRUE TRUE
-#undef TRUE
-#endif
-#ifdef FALSE
-#define STORM_TEMP_FALSE FALSE
-#undef FALSE
-#endif
-#include <carl/formula/Formula.h>
-// Restore TRUE / FALSE macros.
-#ifdef STORM_TEMP_TRUE
-#define TRUE STORM_TEMP_TRUE
-#undef STORM_TEMP_TRUE
-#endif
-#ifdef STORM_TEMP_FALSE
-#define FALSE STORM_TEMP_FALSE
-#undef STORM_TEMP_FALSE
-#endif
-
 namespace carl {
     // Define hash values for all polynomials and rational function.
     template<typename C, typename O, typename P>
@@ -78,7 +57,5 @@ namespace storm {
     
     typedef carl::RationalFunction<Polynomial, true> RationalFunction;
     typedef carl::Interval<double> Interval;
-
-    typedef carl::Formula<RawPolynomial> RationalFunctionConstraint;
 }
 

src/storm/analysis/GraphConditions.h

@@ -4,6 +4,7 @@
 #include <unordered_set>
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/models/sparse/Dtmc.h"
+#include <carl/formula/Formula.h>
 
 namespace storm {
     namespace analysis {
@@ -16,7 +17,7 @@ namespace storm {
 
         template<typename ValueType>
         struct ConstraintType<ValueType, typename std::enable_if<std::is_same<storm::RationalFunction, ValueType>::value>::type> {
-            typedef storm::RationalFunctionConstraint val;
+            typedef carl::Formula<typename storm::RationalFunction::PolyType::PolyType> val;
         };
 
         /**

src/storm/settings/modules/CoreSettings.cpp

@@ -9,6 +9,7 @@
 #include "storm/solver/SolverSelectionOptions.h"
 
 #include "storm/storage/dd/DdType.h"
+#include "storm/adapters/IntelTbbAdapter.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/IllegalArgumentValueException.h"

src/storm/solver/GmmxxMultiplier.cpp

@@ -2,6 +2,7 @@
 
 #include "storm/adapters/RationalNumberAdapter.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
+#include "storm/adapters/IntelTbbAdapter.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"

src/storm/solver/NativeMultiplier.cpp

@@ -10,6 +10,7 @@
 
 #include "storm/adapters/RationalNumberAdapter.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
+#include "storm/adapters/IntelTbbAdapter.h"
 
 #include "storm/utility/macros.h"
 

src/storm/storage/SparseMatrix.cpp

@@ -1,12 +1,5 @@
 #include <boost/functional/hash.hpp>
 
-// To detect whether the usage of TBB is possible, this include is neccessary
-#include "storm-config.h"
-
-#ifdef STORM_HAVE_INTELTBB
-#include "tbb/tbb.h"
-#endif
-
 #include "storm/storage/sparse/StateType.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/adapters/RationalFunctionAdapter.h"

src/storm/storage/SparseMatrix.h

@@ -16,6 +16,7 @@
 #include "storm/utility/macros.h"
 #include "storm/utility/constants.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
+#include "storm/adapters/IntelTbbAdapter.h"
 
 // Forward declaration for adapter classes.
 namespace storm {

src/storm/utility/VectorHelper.cpp

@@ -5,8 +5,7 @@
 
 #include "storm/adapters/RationalNumberAdapter.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
-
-#include "storm-config.h"
+#include "storm/adapters/IntelTbbAdapter.h"
 
 #include "storm/utility/vector.h"
 

src/storm/utility/constants.cpp

@@ -52,7 +52,7 @@ namespace storm {
         
         template<>
         bool isNan(double const& value) {
-            return isnan(value);
+            return std::isnan(value);
         }
         
         bool isAlmostZero(double const& a) {

src/storm/utility/vector.h

@@ -1,16 +1,12 @@
 #ifndef STORM_UTILITY_VECTOR_H_
 #define STORM_UTILITY_VECTOR_H_
 
-#include "storm-config.h"
-#ifdef STORM_HAVE_INTELTBB
-#include "tbb/tbb.h"
-#endif
-
 #include <iostream>
 #include <algorithm>
 #include <functional>
 #include <numeric>
 #include <storm/adapters/RationalFunctionAdapter.h>
+#include <storm/adapters/IntelTbbAdapter.h>
 
 #include <boost/optional.hpp>