diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index dbd5c1994..edde6925d 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -28,7 +28,7 @@
#include "src/models/AtomicPropositionsLabeling.h"
#include "src/storage/SparseMatrix.h"
#include "src/settings/SettingsManager.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm {
@@ -106,7 +106,7 @@ namespace storm {
std::map<std::string, storm::expressions::Expression> constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions);
- LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants.");
+ STORM_LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants.");
// Now that we have defined all the constants in the program, we need to substitute their appearances in
// all expressions in the program so we can then evaluate them without having to store the values of the
@@ -173,10 +173,10 @@ namespace storm {
{
newValue = assignment.getExpression().evaluateAsInt(baseState);
auto const& boundsPair = variableInformation.variableToBoundsMap.find(assignment.getVariableName());
- LOG_THROW(boundsPair->second.first <= newValue && newValue <= boundsPair->second.second, storm::exceptions::InvalidArgumentException, "Invalid value " << newValue << " for variable '" << assignment.getVariableName() << "'.");
+ STORM_LOG_THROW(boundsPair->second.first <= newValue && newValue <= boundsPair->second.second, storm::exceptions::InvalidArgumentException, "Invalid value " << newValue << " for variable '" << assignment.getVariableName() << "'.");
newState->setIntegerValue(assignment.getVariableName(), newValue); break;
}
- default: LOG_ASSERT(false, "Invalid type of assignment."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid type of assignment."); break;
}
}
return newState;
@@ -312,7 +312,7 @@ namespace storm {
}
// Check that the resulting distribution is in fact a distribution.
- LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "'.");
+ STORM_LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "'.");
}
}
diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h
index 7f850f9d3..4c162378f 100644
--- a/src/adapters/Z3ExpressionAdapter.h
+++ b/src/adapters/Z3ExpressionAdapter.h
@@ -18,7 +18,7 @@
#include "storm-config.h"
#include "src/storage/expressions/Expressions.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/ExpressionEvaluationException.h"
#include "src/exceptions/InvalidTypeException.h"
#include "src/exceptions/NotImplementedException.h"
@@ -68,7 +68,7 @@ namespace storm {
variables = expression.getVariablesAndTypes();
}
catch (storm::exceptions::InvalidTypeException* e) {
- LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with ambigious type while trying to autocreate solver variables: " << e);
+ STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with ambigious type while trying to autocreate solver variables: " << e);
}
for (auto variableAndType : variables) {
@@ -85,7 +85,7 @@ namespace storm {
this->variableToExpressionMap.insert(std::make_pair(variableAndType.first, context.real_const(variableAndType.first.c_str())));
break;
default:
- LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with unknown type while trying to autocreate solver variables: " << variableAndType.first);
+ STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with unknown type while trying to autocreate solver variables: " << variableAndType.first);
break;
}
}
@@ -118,7 +118,7 @@ namespace storm {
return storm::expressions::Expression::createTrue();
break;
default:
- LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant boolean, but value is undefined.");
+ STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant boolean, but value is undefined.");
break;
}
} else if (expr.is_int() && expr.is_const()) {
@@ -126,7 +126,7 @@ namespace storm {
if (Z3_get_numeral_int64(expr.ctx(), expr, &value)) {
return storm::expressions::Expression::createIntegerLiteral(value);
} else {
- LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant integer and value does not fit into 64-bit integer.");
+ STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant integer and value does not fit into 64-bit integer.");
}
} else if (expr.is_real() && expr.is_const()) {
int_fast64_t num;
@@ -134,7 +134,7 @@ namespace storm {
if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) {
return storm::expressions::Expression::createDoubleLiteral(static_cast<double>(num) / static_cast<double>(den));
} else {
- LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant real and value does not fit into a fraction with 64-bit integer numerator and denominator.");
+ STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant real and value does not fit into a fraction with 64-bit integer numerator and denominator.");
}
} else */
if (expr.is_app()) {
@@ -149,7 +149,7 @@ namespace storm {
return this->translateExpression(expr.arg(0)).ite(this->translateExpression(expr.arg(1)), this->translateExpression(expr.arg(2)));
case Z3_OP_AND: {
unsigned args = expr.num_args();
- LOG_THROW(args != 0, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. 0-ary AND is assumed to be an error.");
+ STORM_LOG_THROW(args != 0, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. 0-ary AND is assumed to be an error.");
if (args == 1) {
return this->translateExpression(expr.arg(0));
} else {
@@ -162,7 +162,7 @@ namespace storm {
}
case Z3_OP_OR: {
unsigned args = expr.num_args();
- LOG_THROW(args != 0, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. 0-ary OR is assumed to be an error.");
+ STORM_LOG_THROW(args != 0, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. 0-ary OR is assumed to be an error.");
if (args == 1) {
return this->translateExpression(expr.arg(0));
} else {
@@ -208,7 +208,7 @@ namespace storm {
if (Z3_get_numeral_int64(expr.ctx(), expr, &value)) {
return storm::expressions::Expression::createIntegerLiteral(value);
} else {
- LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant integer and value does not fit into 64-bit integer.");
+ STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant integer and value does not fit into 64-bit integer.");
}
} else if (expr.is_real() && expr.is_const()) {
long long num;
@@ -216,12 +216,12 @@ namespace storm {
if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) {
return storm::expressions::Expression::createDoubleLiteral(static_cast<double>(num) / static_cast<double>(den));
} else {
- LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant real and value does not fit into a fraction with 64-bit integer numerator and denominator.");
+ STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant real and value does not fit into a fraction with 64-bit integer numerator and denominator.");
}
}
case Z3_OP_UNINTERPRETED:
//storm only supports uninterpreted constant functions
- LOG_THROW(expr.is_const(), storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered non constant uninterpreted function.");
+ STORM_LOG_THROW(expr.is_const(), storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered non constant uninterpreted function.");
if (expr.is_bool()) {
return storm::expressions::Expression::createBooleanVariable(expr.decl().name().str());
} else if (expr.is_int()) {
@@ -229,15 +229,15 @@ namespace storm {
} else if (expr.is_real()) {
return storm::expressions::Expression::createDoubleVariable(expr.decl().name().str());
} else {
- LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered constant uninterpreted function of unknown sort.");
+ STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered constant uninterpreted function of unknown sort.");
}
default:
- LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unhandled Z3_decl_kind " << expr.decl().kind() <<".");
+ STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unhandled Z3_decl_kind " << expr.decl().kind() <<".");
break;
}
} else {
- LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unknown expression type.");
+ STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unknown expression type.");
}
}
diff --git a/src/exceptions/ArgumentUnificationException.h b/src/exceptions/ArgumentUnificationException.h
index 7f772819c..86d37dba2 100644
--- a/src/exceptions/ArgumentUnificationException.h
+++ b/src/exceptions/ArgumentUnificationException.h
@@ -1,23 +1,15 @@
-/*
- * ArgumentUnificationException.h
- *
- * Created on: 19.07.2013
- * Author: Philipp Berger
- */
-
#ifndef STORM_EXCEPTIONS_ARGUMENTUNIFICATIONEXCEPTION_H_
#define STORM_EXCEPTIONS_ARGUMENTUNIFICATIONEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-STORM_EXCEPTION_DEFINE_NEW(ArgumentUnificationException)
-
-}
-
-}
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(ArgumentUnificationException)
+
+ } // namespace exceptions
+} // namespace storm
#endif /* STORM_EXCEPTIONS_ARGUMENTUNIFICATIONEXCEPTION_H_ */
diff --git a/src/exceptions/BaseException.cpp b/src/exceptions/BaseException.cpp
new file mode 100644
index 000000000..0acae02ac
--- /dev/null
+++ b/src/exceptions/BaseException.cpp
@@ -0,0 +1,25 @@
+#include "src/exceptions/BaseException.h"
+
+namespace storm {
+ namespace exceptions {
+ BaseException::BaseException() : exception() {
+ // Intentionally left empty.
+ }
+
+ BaseException::BaseException(BaseException const& other) : exception(other), stream(other.stream.str()) {
+ // Intentionally left empty.
+ }
+
+ BaseException::BaseException(char const* cstr) {
+ stream << cstr;
+ }
+
+ const char* BaseException::what() const throw() {
+ std::string errorString = this->stream.str();
+ char* result = new char[errorString.size() + 1];
+ result[errorString.size()] = '\0';
+ std::copy(errorString.begin(), errorString.end(), result);
+ return result;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/exceptions/BaseException.h b/src/exceptions/BaseException.h
index 6c670f88b..8bf12ea23 100644
--- a/src/exceptions/BaseException.h
+++ b/src/exceptions/BaseException.h
@@ -5,55 +5,43 @@
#include <sstream>
namespace storm {
-namespace exceptions {
-
-template<typename E>
-class BaseException : public std::exception {
- public:
- BaseException() : exception() {}
- BaseException(const BaseException& cp)
- : exception(cp), stream(cp.stream.str()) {
- }
-
- BaseException(const char* cstr) {
- stream << cstr;
- }
-
- ~BaseException() throw() { }
-
- template<class T>
- E& operator<<(const T& var) {
- this->stream << var;
- return * dynamic_cast<E*>(this);
- }
-
- virtual const char* what() const throw() {
- std::string errorString = this->stream.str();
- char* result = new char[errorString.size() + 1];
- result[errorString.size()] = '\0';
- std::copy(errorString.begin(), errorString.end(), result);
- return result;
- }
-
- private:
- std::stringstream stream;
-};
-
-} // namespace exceptions
+ namespace exceptions {
+
+ /*!
+ * This class represents the base class of all exception classes.
+ */
+ class BaseException : public std::exception {
+ public:
+ /*!
+ * Creates a base exception without a message.
+ */
+ BaseException();
+
+ /*!
+ * Creates a base expression from the given exception.
+ *
+ * @param other The expression from which to copy-construct.
+ */
+ BaseException(BaseException const& other);
+
+ /*!
+ * Adds the given string to the message of this exception.
+ */
+ BaseException(char const* cstr);
+
+ /*!
+ * Retrieves the message associated with this exception.
+ *
+ * @return The message associated with this exception.
+ */
+ virtual const char* what() const throw();
+
+ protected:
+ // This stream stores the message of this exception.
+ std::stringstream stream;
+ };
+
+ } // namespace exceptions
} // namespace storm
-/* Macro to generate descendant exception classes.
- * As all classes are nearly the same, this makes changing common features much easier.
- */
-#define STORM_EXCEPTION_DEFINE_NEW(exception_name) class exception_name : public BaseException<exception_name> { \
-public: \
- exception_name() : BaseException() { \
- } \
- exception_name(const char* cstr) : BaseException(cstr) { \
- } \
- exception_name(const exception_name& cp) : BaseException(cp) { \
- } \
-};
-
-
#endif // STORM_EXCEPTIONS_BASEEXCEPTION_H_
diff --git a/src/exceptions/ExceptionMacros.h b/src/exceptions/ExceptionMacros.h
index bbf2f4f36..943990ae7 100644
--- a/src/exceptions/ExceptionMacros.h
+++ b/src/exceptions/ExceptionMacros.h
@@ -1,36 +1,23 @@
#ifndef STORM_EXCEPTIONS_EXCEPTIONMACROS_H_
#define STORM_EXCEPTIONS_EXCEPTIONMACROS_H_
-#include <cassert>
+/*!
+ * Macro to generate descendant exception classes. As all classes are nearly the same, this makes changing common
+ * features much easier.
+ */
+#define STORM_NEW_EXCEPTION(exception_name) class exception_name : public BaseException { \
+public: \
+exception_name() : BaseException() { \
+} \
+exception_name(char const* cstr) : BaseException(cstr) { \
+} \
+exception_name(exception_name const& cp) : BaseException(cp) { \
+} \
+template<typename T> \
+exception_name& operator<<(T const& var) { \
+ this->stream << var; \
+ return *this; \
+} \
+};
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-
-extern log4cplus::Logger logger;
-
-#ifndef NDEBUG
-#define LOG_ASSERT(cond, message) \
-{ \
- if (!(cond)) { \
- LOG4CPLUS_ERROR(logger, message); \
- assert(cond); \
- } \
-} while (false)
-#define LOG_DEBUG(message) \
-{ \
- LOG4CPLUS_DEBUG(logger, message); \
-} while (false)
-#else
-#define LOG_ASSERT(cond, message) /* empty */
-#define LOG_DEBUG(message) /* empty */
-#endif
-
-#define LOG_THROW(cond, exception, message) \
-{ \
-if (!(cond)) { \
-LOG4CPLUS_ERROR(logger, message); \
-throw exception() << message; \
-} \
-} while (false)
-
-#endif /* STORM_EXCEPTIONS_EXCEPTIONMACROS_H_ */
\ No newline at end of file
+#endif /* STORM_EXCEPTIONS_EXCEPTIONMACROS_H_ */
diff --git a/src/exceptions/ExpressionEvaluationException.h b/src/exceptions/ExpressionEvaluationException.h
index 390991c1d..8ca4e81db 100644
--- a/src/exceptions/ExpressionEvaluationException.h
+++ b/src/exceptions/ExpressionEvaluationException.h
@@ -1,23 +1,15 @@
-/*
- * ExpressionEvaluationException.h
- *
- * Created on: 12.01.2013
- * Author: Christian Dehnert
- */
-
#ifndef STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_
#define STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-STORM_EXCEPTION_DEFINE_NEW(ExpressionEvaluationException)
-
-}
-
-}
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(ExpressionEvaluationException)
+
+ } // namespace exceptions
+} // namespace storm
#endif /* STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_ */
diff --git a/src/exceptions/FileIoException.h b/src/exceptions/FileIoException.h
index 2d7e63d47..f6363f154 100644
--- a/src/exceptions/FileIoException.h
+++ b/src/exceptions/FileIoException.h
@@ -1,23 +1,15 @@
-/*
- * FileIoException.h
- *
- * Created on: 16.08.2012
- * Author: Thomas Heinemann
- */
-
#ifndef STORM_EXCEPTIONS_FILEIOEXCEPTION_H_
#define STORM_EXCEPTIONS_FILEIOEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-STORM_EXCEPTION_DEFINE_NEW(FileIoException)
-
-}
-
-}
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(FileIoException)
+
+ } // namespace exceptions
+} // namespace storm
#endif /* STORM_EXCEPTIONS_FILEIOEXCEPTION_H_ */
diff --git a/src/exceptions/IllegalArgumentException.h b/src/exceptions/IllegalArgumentException.h
index baa1581de..1faf838bb 100644
--- a/src/exceptions/IllegalArgumentException.h
+++ b/src/exceptions/IllegalArgumentException.h
@@ -2,17 +2,14 @@
#define STORM_EXCEPTIONS_ILLEGALARGUMENTEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-/*!
- * @brief This exception is thrown when a parameter is invalid or illegal in this context
- */
-STORM_EXCEPTION_DEFINE_NEW(IllegalArgumentException)
-
-} // namespace exceptions
-
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(IllegalArgumentException)
+
+ } // namespace exceptions
} // namespace storm
-#endif // STORM_EXCEPTIONS_ILLEGALARGUMENTEXCEPTION_H_
+
+#endif /* STORM_EXCEPTIONS_ILLEGALARGUMENTEXCEPTION_H_ */
diff --git a/src/exceptions/IllegalArgumentTypeException.h b/src/exceptions/IllegalArgumentTypeException.h
index 8a5f242da..bd12b9728 100644
--- a/src/exceptions/IllegalArgumentTypeException.h
+++ b/src/exceptions/IllegalArgumentTypeException.h
@@ -1,23 +1,15 @@
-/*
- * IllegalArgumentTypeException.h
- *
- * Created on: 10.08.2013
- * Author: Philipp Berger
- */
-
#ifndef STORM_EXCEPTIONS_ILLEGALARGUMENTTYPEEXCEPTION_H_
#define STORM_EXCEPTIONS_ILLEGALARGUMENTTYPEEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-STORM_EXCEPTION_DEFINE_NEW(IllegalArgumentTypeException)
-
-}
-
-}
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(IllegalArgumentTypeException)
+
+ } // namespace exceptions
+} // namespace storm
#endif /* STORM_EXCEPTIONS_ILLEGALARGUMENTTYPEEXCEPTION_H_ */
diff --git a/src/exceptions/IllegalArgumentValueException.h b/src/exceptions/IllegalArgumentValueException.h
index 28b14af79..465e8ff00 100644
--- a/src/exceptions/IllegalArgumentValueException.h
+++ b/src/exceptions/IllegalArgumentValueException.h
@@ -1,23 +1,15 @@
-/*
- * IllegalArgumentValueException.h
- *
- * Created on: 10.08.2013
- * Author: Philipp Berger
- */
-
#ifndef STORM_EXCEPTIONS_ILLEGALARGUMENTVALUEEXCEPTION_H_
#define STORM_EXCEPTIONS_ILLEGALARGUMENTVALUEEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-STORM_EXCEPTION_DEFINE_NEW(IllegalArgumentValueException)
-
-}
-
-}
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(IllegalArgumentValueException)
+
+ } // namespace exceptions
+} // namespace storm
#endif /* STORM_EXCEPTIONS_ILLEGALARGUMENTVALUEEXCEPTION_H_ */
diff --git a/src/exceptions/IllegalFunctionCallException.h b/src/exceptions/IllegalFunctionCallException.h
index 0515e1c00..c0dead65f 100644
--- a/src/exceptions/IllegalFunctionCallException.h
+++ b/src/exceptions/IllegalFunctionCallException.h
@@ -1,25 +1,15 @@
-/*
- * IllegalFunctionCallException.h
- *
- * Created on: 09.08.2013
- * Author: Philipp Berger
- */
-
#ifndef STORM_EXCEPTIONS_ILLEGALFUNCTIONCALLEXCEPTION_H_
#define STORM_EXCEPTIONS_ILLEGALFUNCTIONCALLEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-/*!
- * @brief This exception is thrown when a function call is not allowed in this context
- */
-STORM_EXCEPTION_DEFINE_NEW(IllegalFunctionCallException)
-
-} // namespace exceptions
-
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(IllegalFunctionCallException)
+
+ } // namespace exceptions
} // namespace storm
-#endif // STORM_EXCEPTIONS_ILLEGALFUNCTIONCALLEXCEPTION_H_
+
+#endif /* STORM_EXCEPTIONS_ILLEGALFUNCTIONCALLEXCEPTION_H_ */
diff --git a/src/exceptions/InternalTypeErrorException.h b/src/exceptions/InternalTypeErrorException.h
index ed1f609ba..d3a1223e1 100644
--- a/src/exceptions/InternalTypeErrorException.h
+++ b/src/exceptions/InternalTypeErrorException.h
@@ -1,26 +1,15 @@
-/*
- * InternalTypeErrorException.h
- *
- * Created on: 09.08.2013
- * Author: Philipp Berger
- */
-
#ifndef STORM_EXCEPTIONS_INTERNALTYPEERROREXCEPTION_H_
#define STORM_EXCEPTIONS_INTERNALTYPEERROREXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-/*!
- * @brief This exception is thrown when an internal function observes an unknown state or type, e.g. a missing case statement.
- */
-STORM_EXCEPTION_DEFINE_NEW(InternalTypeErrorException)
-
-}
-
-}
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(InternalTypeErrorException)
+
+ } // namespace exceptions
+} // namespace storm
#endif /* STORM_EXCEPTIONS_INTERNALTYPEERROREXCEPTION_H_ */
diff --git a/src/exceptions/InvalidAccessException.h b/src/exceptions/InvalidAccessException.h
index af413b1ed..f1e2f8059 100644
--- a/src/exceptions/InvalidAccessException.h
+++ b/src/exceptions/InvalidAccessException.h
@@ -2,18 +2,14 @@
#define STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-/*!
- * @brief This exception is thrown when a function is used/accessed that is forbidden to use (e.g. Copy Constructors)
- */
-STORM_EXCEPTION_DEFINE_NEW(InvalidAccessException)
-
-} // namespace exceptions
-
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(InvalidAccessException)
+
+ } // namespace exceptions
} // namespace storm
-#endif // STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_
+#endif /* STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_ */
diff --git a/src/exceptions/InvalidArgumentException.h b/src/exceptions/InvalidArgumentException.h
index fac516554..a0e7c49dd 100644
--- a/src/exceptions/InvalidArgumentException.h
+++ b/src/exceptions/InvalidArgumentException.h
@@ -2,17 +2,14 @@
#define STORM_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-/*!
- * @brief This exception is thrown when a parameter is invalid in this context
- */
-STORM_EXCEPTION_DEFINE_NEW(InvalidArgumentException)
-
-} // namespace exceptions
-
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(InvalidArgumentException)
+
+ } // namespace exceptions
} // namespace storm
-#endif // STORM_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_
+
+#endif /* STORM_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_ */
diff --git a/src/exceptions/InvalidOperationException.h b/src/exceptions/InvalidOperationException.h
index 728f7ff1c..7bb91fcea 100644
--- a/src/exceptions/InvalidOperationException.h
+++ b/src/exceptions/InvalidOperationException.h
@@ -2,16 +2,14 @@
#define STORM_EXCEPTIONS_INVALIDOPERATIONEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
namespace exceptions {
- /*!
- * @brief This exception is thrown when an operation is invalid in this context
- */
- STORM_EXCEPTION_DEFINE_NEW(InvalidOperationException)
+ STORM_NEW_EXCEPTION(InvalidOperationException)
} // namespace exceptions
} // namespace storm
-#endif // STORM_EXCEPTIONS_INVALIDOPERATIONEXCEPTION_H_
+
+#endif /* STORM_EXCEPTIONS_INVALIDOPERATIONEXCEPTION_H_ */
diff --git a/src/exceptions/InvalidPropertyException.h b/src/exceptions/InvalidPropertyException.h
index 6cddb9d91..77952b708 100644
--- a/src/exceptions/InvalidPropertyException.h
+++ b/src/exceptions/InvalidPropertyException.h
@@ -1,26 +1,15 @@
-/*
- * InvalidPropertyException.h
- *
- * Created on: 27.12.2012
- * Author: Christian Dehnert
- */
-
#ifndef STORM_EXCEPTIONS_INVALIDPROPERTYEXCEPTION_H_
#define STORM_EXCEPTIONS_INVALIDPROPERTYEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-/*!
- * @brief This exception is thrown when a parameter is invalid in this context
- */
-STORM_EXCEPTION_DEFINE_NEW(InvalidPropertyException)
-
-} // namespace exceptions
-
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(InvalidPropertyException)
+
+ } // namespace exceptions
} // namespace storm
#endif /* STORM_EXCEPTIONS_INVALIDPROPERTYEXCEPTION_H_ */
diff --git a/src/exceptions/InvalidSettingsException.h b/src/exceptions/InvalidSettingsException.h
index 12b0ba5b2..39e0d2c45 100644
--- a/src/exceptions/InvalidSettingsException.h
+++ b/src/exceptions/InvalidSettingsException.h
@@ -2,13 +2,14 @@
#define STORM_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-namespace exceptions {
-
-STORM_EXCEPTION_DEFINE_NEW(InvalidSettingsException)
-
-} // namespace exceptions
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(InvalidSettingsException)
+
+ } // namespace exceptions
} // namespace storm
-#endif // STORM_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_
+#endif /* STORM_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_ */
diff --git a/src/exceptions/InvalidStateException.h b/src/exceptions/InvalidStateException.h
index 0489e08ca..ad0cbc50a 100644
--- a/src/exceptions/InvalidStateException.h
+++ b/src/exceptions/InvalidStateException.h
@@ -2,19 +2,14 @@
#define STORM_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-/*!
- * @brief This exception is thrown when a memory request can not be
- * fulfilled.
- */
-STORM_EXCEPTION_DEFINE_NEW(InvalidStateException)
-
-} // namespace exceptions
-
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(InvalidStateException)
+
+ } // namespace exceptions
} // namespace storm
-#endif // STORM_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_
+#endif /* STORM_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_ */
diff --git a/src/exceptions/InvalidTypeException.h b/src/exceptions/InvalidTypeException.h
index de2874218..be7e745ba 100644
--- a/src/exceptions/InvalidTypeException.h
+++ b/src/exceptions/InvalidTypeException.h
@@ -2,17 +2,14 @@
#define STORM_EXCEPTIONS_INVALIDTYPEEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
namespace exceptions {
- /*!
- * @brief This exception is thrown when a type is invalid in this context
- */
- STORM_EXCEPTION_DEFINE_NEW(InvalidTypeException)
+ STORM_NEW_EXCEPTION(InvalidTypeException)
} // namespace exceptions
-
} // namespace storm
-#endif // STORM_EXCEPTIONS_INVALIDTYPEEXCEPTION_H_
+
+#endif /* STORM_EXCEPTIONS_INVALIDTYPEEXCEPTION_H_ */
diff --git a/src/exceptions/NoConvergenceException.h b/src/exceptions/NoConvergenceException.h
index a3fdd3ba3..8ba22855e 100644
--- a/src/exceptions/NoConvergenceException.h
+++ b/src/exceptions/NoConvergenceException.h
@@ -2,16 +2,14 @@
#define STORM_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-namespace exceptions {
-
-/*!
- * @brief This exception is thrown when an iterative solver failed to converge with the given maxIterations
- */
-STORM_EXCEPTION_DEFINE_NEW(NoConvergenceException)
-
-} // namespace exceptions
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(NoConvergenceException)
+
+ } // namespace exceptions
} // namespace storm
-#endif // STORM_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_
+#endif /* STORM_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_ */
diff --git a/src/exceptions/NotImplementedException.h b/src/exceptions/NotImplementedException.h
index cf98d4d99..857ad7c77 100644
--- a/src/exceptions/NotImplementedException.h
+++ b/src/exceptions/NotImplementedException.h
@@ -1,23 +1,15 @@
-/*
- * NotImplementedException.h
- *
- * Created on: 12.01.2013
- * Author: Christian Dehnert
- */
-
#ifndef STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_
#define STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-STORM_EXCEPTION_DEFINE_NEW(NotImplementedException)
-
-}
-
-}
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(NotImplementedException)
+
+ } // namespace exceptions
+} // namespace storm
#endif /* STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_ */
diff --git a/src/exceptions/OptionParserException.h b/src/exceptions/OptionParserException.h
index d0befae51..1f54a5801 100644
--- a/src/exceptions/OptionParserException.h
+++ b/src/exceptions/OptionParserException.h
@@ -1,23 +1,15 @@
-/*
- * OptionParserException.h
- *
- * Created on: 23.08.2013
- * Author: Philipp Berger
- */
-
#ifndef STORM_EXCEPTIONS_OPTIONPARSEREXCEPTION_H_
#define STORM_EXCEPTIONS_OPTIONPARSEREXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-STORM_EXCEPTION_DEFINE_NEW(OptionParserException)
-
-}
-
-}
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(OptionParserException)
+
+ } // namespace exceptions
+} // namespace storm
#endif /* STORM_EXCEPTIONS_OPTIONPARSEREXCEPTION_H_ */
diff --git a/src/exceptions/OptionUnificationException.h b/src/exceptions/OptionUnificationException.h
index 6eac306e7..0aeef9e5c 100644
--- a/src/exceptions/OptionUnificationException.h
+++ b/src/exceptions/OptionUnificationException.h
@@ -1,23 +1,15 @@
-/*
- * OptionUnificationException.h
- *
- * Created on: 21.08.2013
- * Author: Philipp Berger
- */
-
#ifndef STORM_EXCEPTIONS_OPTIONUNIFICATIONEXCEPTION_H_
#define STORM_EXCEPTIONS_OPTIONUNIFICATIONEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-STORM_EXCEPTION_DEFINE_NEW(OptionUnificationException)
-
-}
-
-}
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(OptionUnificationException)
+
+ } // namespace exceptions
+} // namespace storm
#endif /* STORM_EXCEPTIONS_OPTIONUNIFICATIONEXCEPTION_H_ */
diff --git a/src/exceptions/OutOfRangeException.h b/src/exceptions/OutOfRangeException.h
index af0856213..dc51e934b 100644
--- a/src/exceptions/OutOfRangeException.h
+++ b/src/exceptions/OutOfRangeException.h
@@ -2,17 +2,14 @@
#define STORM_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-/*
- * @briefThis exception is thrown when a parameter is not in the range of valid values
- */
-STORM_EXCEPTION_DEFINE_NEW(OutOfRangeException)
-
-} // namespace exceptions
-
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(OutOfRangeException)
+
+ } // namespace exceptions
} // namespace storm
-#endif // STORM_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_
+
+#endif /* STORM_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_ */
diff --git a/src/exceptions/WrongFormatException.h b/src/exceptions/WrongFormatException.h
index 6196eac82..933838047 100644
--- a/src/exceptions/WrongFormatException.h
+++ b/src/exceptions/WrongFormatException.h
@@ -1,27 +1,15 @@
-/*
- * WrongFormatException.h
- *
- * Created on: 16.08.2012
- * Author: Thomas Heinemann
- */
-
#ifndef STORM_EXCEPTIONS_WRONGFORMATEXCEPTION_H_
#define STORM_EXCEPTIONS_WRONGFORMATEXCEPTION_H_
#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
namespace storm {
-
-namespace exceptions {
-
-/*!
- * @brief This exception is thrown when an input file
- * contains invalid or missing keys.
- */
-STORM_EXCEPTION_DEFINE_NEW(WrongFormatException)
-
-} //namespace exceptions
-
-} //namespace storm
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(WrongFormatException)
+
+ } // namespace exceptions
+} // namespace storm
#endif /* STORM_EXCEPTIONS_WRONGFORMATEXCEPTION_H_ */
diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp
index b7f54b06f..6edcd08fb 100644
--- a/src/modelchecker/reachability/SparseSccModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp
@@ -6,7 +6,7 @@
#include "src/utility/graph.h"
#include "src/utility/vector.h"
#include "src/exceptions/InvalidStateException.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
namespace storm {
namespace modelchecker {
@@ -34,7 +34,7 @@ namespace storm {
template<typename ValueType>
ValueType SparseSccModelChecker<ValueType>::computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
// First, do some sanity checks to establish some required properties.
- LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
+ STORM_LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
typename FlexibleSparseMatrix<ValueType>::index_type initialStateIndex = *dtmc.getInitialStates().begin();
// Then, compute the subset of states that has a probability of 0 or 1, respectively.
@@ -204,7 +204,7 @@ namespace storm {
typename FlexibleSparseMatrix<ValueType>::row_type::iterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
// Make sure we have found the probability and set it to zero.
- LOG_THROW(multiplyElement != predecessorForwardTransitions.end(), storm::exceptions::InvalidStateException, "No probability for successor found.");
+ STORM_LOG_THROW(multiplyElement != predecessorForwardTransitions.end(), storm::exceptions::InvalidStateException, "No probability for successor found.");
ValueType multiplyFactor = multiplyElement->getValue();
multiplyElement->setValue(0);
diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp
index 4c2a91fde..697740a7f 100644
--- a/src/parser/AutoParser.cpp
+++ b/src/parser/AutoParser.cpp
@@ -12,7 +12,7 @@
#include "src/parser/DeterministicModelParser.h"
#include "src/parser/NondeterministicModelParser.h"
#include "src/parser/MarkovAutomatonParser.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/utility/cstring.h"
@@ -76,7 +76,7 @@ namespace storm {
// Open the file.
MappedFile file(filename.c_str());
- LOG_THROW(file.getDataSize() >= STORM_PARSER_AUTOPARSER_HINT_LENGTH, storm::exceptions::WrongFormatException, "File too short to be readable.");
+ STORM_LOG_THROW(file.getDataSize() >= STORM_PARSER_AUTOPARSER_HINT_LENGTH, storm::exceptions::WrongFormatException, "File too short to be readable.");
char const* fileData = file.getData();
char filehintBuffer[STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1];
diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp
index ed6d1d642..052f4470c 100644
--- a/src/parser/ExpressionParser.cpp
+++ b/src/parser/ExpressionParser.cpp
@@ -95,7 +95,7 @@ namespace storm {
try {
return e1.ite(e2, e3);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -107,10 +107,10 @@ namespace storm {
switch (operatorType) {
case storm::expressions::OperatorType::Or: return e1 || e2; break;
case storm::expressions::OperatorType::Implies: return e1.implies(e2); break;
- default: LOG_ASSERT(false, "Invalid operation."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -121,10 +121,10 @@ namespace storm {
try {
switch (operatorType) {
case storm::expressions::OperatorType::And: return e1 && e2; break;
- default: LOG_ASSERT(false, "Invalid operation."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -138,10 +138,10 @@ namespace storm {
case storm::expressions::OperatorType::Greater: return e1 > e2; break;
case storm::expressions::OperatorType::LessOrEqual: return e1 <= e2; break;
case storm::expressions::OperatorType::Less: return e1 < e2; break;
- default: LOG_ASSERT(false, "Invalid operation."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -153,10 +153,10 @@ namespace storm {
switch (operatorType) {
case storm::expressions::OperatorType::Equal: return e1.hasBooleanReturnType() && e2.hasBooleanReturnType() ? e1.iff(e2) : e1 == e2; break;
case storm::expressions::OperatorType::NotEqual: return e1 != e2; break;
- default: LOG_ASSERT(false, "Invalid operation."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -168,10 +168,10 @@ namespace storm {
switch (operatorType) {
case storm::expressions::OperatorType::Plus: return e1 + e2; break;
case storm::expressions::OperatorType::Minus: return e1 - e2; break;
- default: LOG_ASSERT(false, "Invalid operation."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -183,10 +183,10 @@ namespace storm {
switch (operatorType) {
case storm::expressions::OperatorType::Times: return e1 * e2; break;
case storm::expressions::OperatorType::Divide: return e1 / e2; break;
- default: LOG_ASSERT(false, "Invalid operation."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -197,10 +197,10 @@ namespace storm {
try {
switch (operatorType) {
case storm::expressions::OperatorType::Power: return e1 ^ e2; break;
- default: LOG_ASSERT(false, "Invalid operation."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -213,13 +213,13 @@ namespace storm {
switch (operatorType.get()) {
case storm::expressions::OperatorType::Not: return !e1; break;
case storm::expressions::OperatorType::Minus: return -e1; break;
- default: LOG_ASSERT(false, "Invalid operation."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
} else {
return e1;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -252,10 +252,10 @@ namespace storm {
switch (operatorType) {
case storm::expressions::OperatorType::Min: return storm::expressions::Expression::minimum(e1, e2); break;
case storm::expressions::OperatorType::Max: return storm::expressions::Expression::maximum(e1, e2); break;
- default: LOG_ASSERT(false, "Invalid operation."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -267,10 +267,10 @@ namespace storm {
switch (operatorType) {
case storm::expressions::OperatorType::Floor: return e1.floor(); break;
case storm::expressions::OperatorType::Ceil: return e1.ceil(); break;
- default: LOG_ASSERT(false, "Invalid operation."); break;
+ default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
@@ -278,9 +278,9 @@ namespace storm {
storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier) const {
if (this->createExpressions) {
- LOG_THROW(this->identifiers_ != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping.");
+ STORM_LOG_THROW(this->identifiers_ != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping.");
storm::expressions::Expression const* expression = this->identifiers_->find(identifier);
- LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
+ STORM_LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
return *expression;
} else {
return storm::expressions::Expression::createFalse();
diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h
index 423227aa2..f5a616e0b 100644
--- a/src/parser/ExpressionParser.h
+++ b/src/parser/ExpressionParser.h
@@ -1,9 +1,11 @@
#ifndef STORM_PARSER_EXPRESSIONPARSER_H_
#define STORM_PARSER_EXPRESSIONPARSER_H_
+#include <sstream>
+
#include "src/parser/SpiritParserDefinitions.h"
#include "src/storage/expressions/Expression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm {
@@ -223,7 +225,9 @@ namespace storm {
template<typename T1, typename T2, typename T3, typename T4>
qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << what << ".");
+ std::stringstream whatAsString;
+ whatAsString << what;
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << whatAsString.str() << ".");
return qi::fail;
}
};
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index ba87a2baa..b327b0984 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -8,7 +8,7 @@ namespace storm {
storm::prism::Program PrismParser::parse(std::string const& filename) {
// Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in);
- LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
+ STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
storm::prism::Program result;
@@ -40,8 +40,8 @@ namespace storm {
try {
// Start first run.
bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
- LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in first pass.");
- LOG_DEBUG("First pass of parsing PRISM input finished.");
+ STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in first pass.");
+ STORM_LOG_DEBUG("First pass of parsing PRISM input finished.");
// Start second run.
first = PositionIteratorType(input.begin());
@@ -49,13 +49,13 @@ namespace storm {
last = PositionIteratorType(input.end());
grammar.moveToSecondRun();
succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
- LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in second pass.");
+ STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in second pass.");
} catch (qi::expectation_failure<PositionIteratorType> const& e) {
// If the parser expected content different than the one provided, display information about the location of the error.
std::size_t lineNumber = boost::spirit::get_line(e.first);
// Now propagate exception.
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << ".");
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << ".");
}
return result;
@@ -213,7 +213,7 @@ namespace storm {
}
bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) {
- LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs.");
+ STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs.");
if (globalProgramInformation.hasInitialConstruct) {
return false;
}
@@ -224,7 +224,7 @@ namespace storm {
storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+ STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename());
@@ -232,7 +232,7 @@ namespace storm {
storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+ STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename());
@@ -240,7 +240,7 @@ namespace storm {
storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+ STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename());
@@ -248,7 +248,7 @@ namespace storm {
storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+ STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename());
@@ -256,7 +256,7 @@ namespace storm {
storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+ STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename());
@@ -264,7 +264,7 @@ namespace storm {
storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+ STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename());
@@ -272,7 +272,7 @@ namespace storm {
storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << formulaName << "'.");
+ STORM_LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << formulaName << "'.");
this->identifiers_.add(formulaName, expression);
} else {
this->identifiers_.at(formulaName) = expression;
@@ -312,7 +312,7 @@ namespace storm {
storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
+ STORM_LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName));
}
return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename());
@@ -320,7 +320,7 @@ namespace storm {
storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
+ STORM_LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName));
}
return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename());
@@ -334,19 +334,19 @@ namespace storm {
storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const {
// Check whether the module to rename actually exists.
auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
- LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": No module named '" << oldModuleName << "' to rename.");
+ STORM_LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": No module named '" << oldModuleName << "' to rename.");
storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
if (!this->secondRun) {
// Register all (renamed) variables for later use.
for (auto const& variable : moduleToRename.getBooleanVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
- LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
+ STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createBooleanVariable(renamingPair->second));
}
for (auto const& variable : moduleToRename.getIntegerVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
- LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
+ STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createIntegerVariable(renamingPair->second));
}
@@ -370,7 +370,7 @@ namespace storm {
std::vector<storm::prism::BooleanVariable> booleanVariables;
for (auto const& variable : moduleToRename.getBooleanVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
- LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
+ STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
}
@@ -379,7 +379,7 @@ namespace storm {
std::vector<storm::prism::IntegerVariable> integerVariables;
for (auto const& variable : moduleToRename.getIntegerVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
- LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
+ STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
}
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index ac36883e9..2f6b13251 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -11,7 +11,7 @@
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/Expressions.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm {
diff --git a/src/settings/Argument.h b/src/settings/Argument.h
index d0471c01b..6626ba35d 100644
--- a/src/settings/Argument.h
+++ b/src/settings/Argument.h
@@ -14,7 +14,7 @@
#include "src/settings/ArgumentBase.h"
#include "src/settings/ArgumentType.h"
#include "src/settings/ArgumentTypeInferationHelper.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/ArgumentUnificationException.h"
#include "src/exceptions/IllegalArgumentException.h"
#include "src/exceptions/IllegalArgumentValueException.h"
@@ -94,9 +94,9 @@ namespace storm {
*/
template <typename S>
bool isCompatibleWith(Argument<S> const& other) const {
- LOG_THROW(this->getType() == other.getType(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because they have different types.");
- LOG_THROW(this->getIsOptional() == other.getIsOptional(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments '" << this->getName() << "' and '" << other.getName() << "', because one of them is optional and the other one is not.");
- LOG_THROW(this->getHasDefaultValue() == other.getHasDefaultValue(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because one of them has a default value and the other one does not.");
+ STORM_LOG_THROW(this->getType() == other.getType(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because they have different types.");
+ STORM_LOG_THROW(this->getIsOptional() == other.getIsOptional(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments '" << this->getName() << "' and '" << other.getName() << "', because one of them is optional and the other one is not.");
+ STORM_LOG_THROW(this->getHasDefaultValue() == other.getHasDefaultValue(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because one of them has a default value and the other one does not.");
return true;
}
@@ -106,7 +106,7 @@ namespace storm {
* @return The value of the argument.
*/
T const& getArgumentValue() const {
- LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument, because it was neither set nor specifies a default value.");
+ STORM_LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument, because it was neither set nor specifies a default value.");
if (this->getHasBeenSet()) {
return this->argumentValue;
} else {
@@ -119,9 +119,9 @@ namespace storm {
}
void setFromDefaultValue() override {
- LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument has none.");
+ STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument has none.");
bool result = this->setFromTypeValue(this->defaultValue);
- LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument, because it was rejected.");
+ STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument, because it was rejected.");
}
virtual std::string getValueAsString() const override {
@@ -144,7 +144,7 @@ namespace storm {
switch (this->argumentType) {
case ArgumentType::Integer:
return inferToInteger(ArgumentType::Integer, this->getArgumentValue());
- default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as integer."); break;
+ default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as integer."); break;
}
}
@@ -153,7 +153,7 @@ namespace storm {
switch (this->argumentType) {
case ArgumentType::UnsignedInteger:
return inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue());
- default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as unsigned integer."); break;
+ default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as unsigned integer."); break;
}
}
@@ -162,7 +162,7 @@ namespace storm {
switch (this->argumentType) {
case ArgumentType::Double:
return inferToDouble(ArgumentType::Double, this->getArgumentValue());
- default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as double."); break;
+ default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as double."); break;
}
}
@@ -171,7 +171,7 @@ namespace storm {
switch (this->argumentType) {
case ArgumentType::Boolean:
return inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
- default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as boolean."); break;
+ default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as boolean."); break;
}
}
@@ -200,7 +200,7 @@ namespace storm {
* @param newDefault The new default value of the argument.
*/
void setDefaultValue(T const& newDefault) {
- LOG_THROW(this->validate(newDefault), storm::exceptions::IllegalArgumentValueException, "The default value for the argument did not pass all validation functions.");
+ STORM_LOG_THROW(this->validate(newDefault), storm::exceptions::IllegalArgumentValueException, "The default value for the argument did not pass all validation functions.");
this->defaultValue = newDefault;
this->hasDefaultValue = true;
}
diff --git a/src/settings/ArgumentBuilder.h b/src/settings/ArgumentBuilder.h
index 712697460..a6902ab85 100644
--- a/src/settings/ArgumentBuilder.h
+++ b/src/settings/ArgumentBuilder.h
@@ -16,7 +16,7 @@
#include "src/settings/Argument.h"
#include "src/settings/ArgumentValidators.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/IllegalFunctionCallException.h"
#include "src/exceptions/IllegalArgumentTypeException.h"
@@ -96,14 +96,14 @@ namespace storm {
*/
ArgumentBuilder& setIsOptional(bool isOptional) {
this->isOptional = isOptional;
- LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to make argument '" << this->name << "' optional without default value.");
+ STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to make argument '" << this->name << "' optional without default value.");
return *this;
}
#define PPCAT_NX(A, B) A ## B
#define PPCAT(A, B) PPCAT_NX(A, B)
#define MACROaddValidationFunction(funcName, funcType) ArgumentBuilder& PPCAT(addValidationFunction, funcName) (storm::settings::Argument< funcType >::userValidationFunction_t userValidationFunction) { \
-LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal validation function for argument, because it takes arguments of different type."); \
+STORM_LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal validation function for argument, because it takes arguments of different type."); \
( PPCAT(this->userValidationFunctions_, funcName) ).push_back(userValidationFunction); \
return *this; \
}
@@ -117,7 +117,7 @@ return *this; \
#define MACROsetDefaultValue(funcName, funcType) ArgumentBuilder& PPCAT(setDefaultValue, funcName) (funcType const& defaultValue) { \
-LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal default value for argument" << this->name << ", because it is of different type."); \
+STORM_LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal default value for argument" << this->name << ", because it is of different type."); \
PPCAT(this->defaultValue_, funcName) = defaultValue; \
this->hasDefaultValue = true; \
return *this; \
@@ -136,7 +136,7 @@ return *this; \
* @return The resulting argument.
*/
std::shared_ptr<ArgumentBase> build() {
- LOG_THROW(!this->hasBeenBuilt, storm::exceptions::IllegalFunctionCallException, "Cannot rebuild argument with builder that was already used to build an argument.");
+ STORM_LOG_THROW(!this->hasBeenBuilt, storm::exceptions::IllegalFunctionCallException, "Cannot rebuild argument with builder that was already used to build an argument.");
this->hasBeenBuilt = true;
switch (this->type) {
case ArgumentType::String: {
diff --git a/src/settings/ArgumentType.h b/src/settings/ArgumentType.h
index 843bb10e6..a1424ac73 100644
--- a/src/settings/ArgumentType.h
+++ b/src/settings/ArgumentType.h
@@ -3,7 +3,7 @@
#include <iostream>
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
namespace storm {
namespace settings {
diff --git a/src/settings/ArgumentTypeInferationHelper.cpp b/src/settings/ArgumentTypeInferationHelper.cpp
index 5ab1693fd..940beb800 100644
--- a/src/settings/ArgumentTypeInferationHelper.cpp
+++ b/src/settings/ArgumentTypeInferationHelper.cpp
@@ -5,7 +5,7 @@ namespace storm {
template <typename T>
ArgumentType inferToEnumType() {
- LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer type of argument.");
+ STORM_LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer type of argument.");
}
template <>
@@ -35,56 +35,56 @@ namespace storm {
template <typename T>
std::string const& inferToString(ArgumentType const& argumentType, T const& value) {
- LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer string from non-string argument value.");
+ STORM_LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer string from non-string argument value.");
}
template <>
std::string const& inferToString<std::string>(ArgumentType const& argumentType, std::string const& value) {
- LOG_THROW(argumentType == ArgumentType::String, storm::exceptions::InternalTypeErrorException, "Unable to infer string from non-string argument.");
+ STORM_LOG_THROW(argumentType == ArgumentType::String, storm::exceptions::InternalTypeErrorException, "Unable to infer string from non-string argument.");
return value;
}
template <typename T>
int_fast64_t inferToInteger(ArgumentType const& argumentType, T const& value) {
- LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument value.");
+ STORM_LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument value.");
}
template <>
int_fast64_t inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value) {
- LOG_THROW(argumentType == ArgumentType::Integer, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument.");
+ STORM_LOG_THROW(argumentType == ArgumentType::Integer, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument.");
return value;
}
template <typename T>
uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, T const& value) {
- LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer unsigned integer from non-unsigned argument value.");
+ STORM_LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer unsigned integer from non-unsigned argument value.");
}
template <>
uint_fast64_t inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value) {
- LOG_THROW(argumentType == ArgumentType::UnsignedInteger, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument.");
+ STORM_LOG_THROW(argumentType == ArgumentType::UnsignedInteger, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument.");
return value;
}
template <typename T>
double inferToDouble(ArgumentType const& argumentType, T const& value) {
- LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument value.");
+ STORM_LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument value.");
}
template <>
double inferToDouble<double>(ArgumentType const& argumentType, double const& value) {
- LOG_THROW(argumentType == ArgumentType::Double, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument.");
+ STORM_LOG_THROW(argumentType == ArgumentType::Double, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument.");
return value;
}
template <typename T>
bool inferToBoolean(ArgumentType const& argumentType, T const& value) {
- LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument value.");
+ STORM_LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument value.");
}
template <>
bool inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value) {
- LOG_THROW(argumentType == ArgumentType::Boolean, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument.");
+ STORM_LOG_THROW(argumentType == ArgumentType::Boolean, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument.");
return value;
}
diff --git a/src/settings/ArgumentTypeInferationHelper.h b/src/settings/ArgumentTypeInferationHelper.h
index 3e3b93122..3b29cd184 100644
--- a/src/settings/ArgumentTypeInferationHelper.h
+++ b/src/settings/ArgumentTypeInferationHelper.h
@@ -5,7 +5,7 @@
#include <string>
#include "src/settings/ArgumentType.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InternalTypeErrorException.h"
namespace storm {
diff --git a/src/settings/ArgumentValidators.h b/src/settings/ArgumentValidators.h
index aad349a44..d5ac0dac2 100644
--- a/src/settings/ArgumentValidators.h
+++ b/src/settings/ArgumentValidators.h
@@ -12,7 +12,7 @@
#include <string>
#include "src/settings/Argument.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
@@ -96,7 +96,7 @@ namespace storm {
std::ifstream targetFile(fileName);
bool isFileGood = targetFile.good();
- LOG_THROW(isFileGood, storm::exceptions::IllegalArgumentValueException, "The file " << fileName << " does not exist or is not readable.");
+ STORM_LOG_THROW(isFileGood, storm::exceptions::IllegalArgumentValueException, "The file " << fileName << " does not exist or is not readable.");
return isFileGood;
};
}
@@ -115,7 +115,7 @@ namespace storm {
}
}
- LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Value '" << inputString << "' does not match any entry in the list of valid items.");
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Value '" << inputString << "' does not match any entry in the list of valid items.");
return false;
};
}
@@ -131,7 +131,7 @@ namespace storm {
template<typename T>
static std::function<bool (T const&)> rangeValidatorIncluding(T lowerBound, T upperBound) {
return std::bind([](T lowerBound, T upperBound, T value) -> bool {
- LOG_THROW(lowerBound <= value && value <= upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out range.");
+ STORM_LOG_THROW(lowerBound <= value && value <= upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out range.");
return true;
}, lowerBound, upperBound, std::placeholders::_1);
}
@@ -146,7 +146,7 @@ namespace storm {
template<typename T>
static std::function<bool (T const&)> rangeValidatorExcluding(T lowerBound, T upperBound) {
return std::bind([](T lowerBound, T upperBound, T value) -> bool {
- LOG_THROW(lowerBound < value && value < upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out range.");
+ STORM_LOG_THROW(lowerBound < value && value < upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out range.");
return true;
}, lowerBound, upperBound, std::placeholders::_1);
}
diff --git a/src/settings/Option.h b/src/settings/Option.h
index c061be37a..d8a1d9d02 100644
--- a/src/settings/Option.h
+++ b/src/settings/Option.h
@@ -14,7 +14,7 @@
#include "ArgumentBase.h"
#include "Argument.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/IllegalArgumentException.h"
#include "src/exceptions/OptionUnificationException.h"
@@ -74,13 +74,13 @@ namespace storm {
* @return True iff the given argument is compatible with the current one.
*/
bool isCompatibleWith(Option const& other) {
- LOG_THROW(this->getArgumentCount() == other.getArgumentCount(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their argument count differs.");
+ STORM_LOG_THROW(this->getArgumentCount() == other.getArgumentCount(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their argument count differs.");
for(size_t i = 0; i != this->arguments.size(); i++) {
ArgumentBase const& firstArgument = this->getArgument(i);
ArgumentBase const& secondArgument = other.getArgument(i);
- LOG_THROW(firstArgument.getType() == secondArgument.getType(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their arguments are incompatible.");
+ STORM_LOG_THROW(firstArgument.getType() == secondArgument.getType(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their arguments are incompatible.");
switch (firstArgument.getType()) {
case ArgumentType::String:
@@ -119,7 +119,7 @@ namespace storm {
* @return The i-th argument of this option.
*/
ArgumentBase const& getArgument(uint_fast64_t argumentIndex) const {
- LOG_THROW(argumentIndex < this->getArgumentCount(), storm::exceptions::IllegalArgumentException, "Index of argument is out of bounds.");
+ STORM_LOG_THROW(argumentIndex < this->getArgumentCount(), storm::exceptions::IllegalArgumentException, "Index of argument is out of bounds.");
return *this->arguments.at(argumentIndex);
}
@@ -130,7 +130,7 @@ namespace storm {
* @return The i-th argument of this option.
*/
ArgumentBase& getArgument(uint_fast64_t argumentIndex) {
- LOG_THROW(argumentIndex < this->getArgumentCount(), storm::exceptions::IllegalArgumentException, "Index of argument is out of bounds.");
+ STORM_LOG_THROW(argumentIndex < this->getArgumentCount(), storm::exceptions::IllegalArgumentException, "Index of argument is out of bounds.");
return *this->arguments.at(argumentIndex);
}
@@ -142,7 +142,7 @@ namespace storm {
*/
ArgumentBase const& getArgumentByName(std::string const& argumentName) const {
auto argumentIterator = this->argumentNameMap.find(argumentName);
- LOG_THROW(argumentIterator != this->argumentNameMap.end(), storm::exceptions::IllegalArgumentException, "Unable to retrieve argument with unknown name '" << argumentName << "'.");
+ STORM_LOG_THROW(argumentIterator != this->argumentNameMap.end(), storm::exceptions::IllegalArgumentException, "Unable to retrieve argument with unknown name '" << argumentName << "'.");
return *argumentIterator->second;
}
@@ -281,14 +281,14 @@ namespace storm {
Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>()) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), hasBeenSet(false), arguments(optionArguments), argumentNameMap() {
// First, do some sanity checks.
- LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name.");
- LOG_THROW(!moduleName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty module name.");
+ STORM_LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name.");
+ STORM_LOG_THROW(!moduleName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty module name.");
bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !std::isalpha(c); }) != longName.end();
- LOG_THROW(!longNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal name.");
+ STORM_LOG_THROW(!longNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal name.");
bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !std::isalpha(c); }) != shortName.end();
- LOG_THROW(!shortNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal name.");
+ STORM_LOG_THROW(!shortNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal name.");
// Then index all arguments.
for (auto const& argument : arguments) {
diff --git a/src/settings/OptionBuilder.h b/src/settings/OptionBuilder.h
index 4217d3471..2d7ad9a19 100644
--- a/src/settings/OptionBuilder.h
+++ b/src/settings/OptionBuilder.h
@@ -13,7 +13,7 @@
#include "src/settings/ArgumentBase.h"
#include "src/settings/Option.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/IllegalArgumentException.h"
#include "src/exceptions/IllegalFunctionCallException.h"
@@ -67,11 +67,11 @@ namespace storm {
* @return A reference to the current builder.
*/
OptionBuilder& addArgument(std::shared_ptr<ArgumentBase> argument) {
- LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot add an argument to an option builder that was already used to build the option.");
- LOG_THROW(this->arguments.empty() || !argument->getIsOptional() || this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional.");
+ STORM_LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot add an argument to an option builder that was already used to build the option.");
+ STORM_LOG_THROW(this->arguments.empty() || !argument->getIsOptional() || this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional.");
std::string lowerArgumentName = boost::algorithm::to_lower_copy(argument->getName());
- LOG_THROW(argumentNameSet.find(lowerArgumentName) == argumentNameSet.end(), storm::exceptions::IllegalArgumentException, "Unable to add argument to option, because it already has an argument with the same name.");
+ STORM_LOG_THROW(argumentNameSet.find(lowerArgumentName) == argumentNameSet.end(), storm::exceptions::IllegalArgumentException, "Unable to add argument to option, because it already has an argument with the same name.");
argumentNameSet.insert(lowerArgumentName);
this->arguments.push_back(argument);
@@ -85,7 +85,7 @@ namespace storm {
* @return The resulting option.
*/
std::shared_ptr<Option> build() {
- LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot rebuild an option with one builder.")
+ STORM_LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot rebuild an option with one builder.")
this->isBuild = true;
if (this->hasShortName) {
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index 83c8edd57..de54de36d 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -86,7 +86,7 @@ namespace storm {
// match the long name.
std::string optionName = currentArgument.substr(2);
auto optionIterator = this->longNameToOptions.find(optionName);
- LOG_THROW(optionIterator != this->longNameToOptions.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");
+ STORM_LOG_THROW(optionIterator != this->longNameToOptions.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");
activeOptionIsShortName = false;
activeOptionName = optionName;
} else {
@@ -94,7 +94,7 @@ namespace storm {
// match the short name.
std::string optionName = currentArgument.substr(1);
auto optionIterator = this->shortNameToOptions.find(optionName);
- LOG_THROW(optionIterator != this->shortNameToOptions.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");
+ STORM_LOG_THROW(optionIterator != this->shortNameToOptions.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");
activeOptionIsShortName = true;
activeOptionName = optionName;
}
@@ -102,7 +102,7 @@ namespace storm {
// Add the current argument to the list of arguments for the currently active options.
argumentCache.push_back(currentArgument);
} else {
- LOG_THROW(false, storm::exceptions::OptionParserException, "Found stray argument '" << currentArgument << "' that is not preceeded by a matching option.");
+ STORM_LOG_THROW(false, storm::exceptions::OptionParserException, "Found stray argument '" << currentArgument << "' that is not preceeded by a matching option.");
}
}
@@ -113,7 +113,7 @@ namespace storm {
}
void SettingsManager::setFromConfigurationFile(std::string const& configFilename) {
- LOG_ASSERT(false, "Not yet implemented.");
+ STORM_LOG_ASSERT(false, "Not yet implemented.");
}
void SettingsManager::printHelp(std::string const& hint) const {
@@ -188,7 +188,7 @@ namespace storm {
void SettingsManager::printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength) const {
auto moduleIterator = moduleOptions.find(moduleName);
- LOG_THROW(moduleIterator != moduleOptions.end(), storm::exceptions::IllegalFunctionCallException, "Cannot print help for unknown module '" << moduleName << "'.");
+ STORM_LOG_THROW(moduleIterator != moduleOptions.end(), storm::exceptions::IllegalFunctionCallException, "Cannot print help for unknown module '" << moduleName << "'.");
std::cout << "##### Module '" << moduleName << "' ";
for (uint_fast64_t i = 0; i < std::min(maxLength, maxLength - moduleName.length() - 16); ++i) {
std::cout << "#";
@@ -215,13 +215,13 @@ namespace storm {
uint_fast64_t SettingsManager::getPrintLengthOfLongestOption(std::string const& moduleName) const {
auto moduleIterator = modules.find(moduleName);
- LOG_THROW(moduleIterator != modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve option length of unknown module '" << moduleName << "'.");
+ STORM_LOG_THROW(moduleIterator != modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve option length of unknown module '" << moduleName << "'.");
return moduleIterator->second->getPrintLengthOfLongestOption();
}
void SettingsManager::addModule(std::unique_ptr<modules::ModuleSettings>&& moduleSettings) {
auto moduleIterator = this->modules.find(moduleSettings->getModuleName());
- LOG_THROW(moduleIterator == this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register module '" << moduleSettings->getModuleName() << "' because a module with the same name already exists.");
+ STORM_LOG_THROW(moduleIterator == this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register module '" << moduleSettings->getModuleName() << "' because a module with the same name already exists.");
// Take over the module settings object.
std::string const& moduleName = moduleSettings->getModuleName();
@@ -240,7 +240,7 @@ namespace storm {
void SettingsManager::addOption(std::shared_ptr<Option> const& option) {
// First, we register to which module the given option belongs.
auto moduleOptionIterator = this->moduleOptions.find(option->getModuleName());
- LOG_THROW(moduleOptionIterator != this->moduleOptions.end(), storm::exceptions::IllegalFunctionCallException, "Cannot add option for unknown module '" << option->getModuleName() << "'.");
+ STORM_LOG_THROW(moduleOptionIterator != this->moduleOptions.end(), storm::exceptions::IllegalFunctionCallException, "Cannot add option for unknown module '" << option->getModuleName() << "'.");
moduleOptionIterator->second.emplace_back(option);
// Then, we add the option's name (and possibly short name) to the registered options. If a module prefix is
@@ -248,7 +248,7 @@ namespace storm {
// non-prefixed one.
if (!option->getRequiresModulePrefix()) {
bool isCompatible = this->isCompatible(option, option->getLongName(), this->longNameToOptions);
- LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it.");
+ STORM_LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it.");
addOptionToMap(option->getLongName(), option, this->longNameToOptions);
}
// For the prefixed name, we don't need a compatibility check, because a module is not allowed to register the same option twice.
@@ -258,7 +258,7 @@ namespace storm {
if (option->getHasShortName()) {
if (!option->getRequiresModulePrefix()) {
bool isCompatible = this->isCompatible(option, option->getShortName(), this->shortNameToOptions);
- LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it.");
+ STORM_LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it.");
addOptionToMap(option->getShortName(), option, this->shortNameToOptions);
}
addOptionToMap(option->getModuleName() + ":" + option->getShortName(), option, this->shortNameToOptions);
@@ -267,13 +267,13 @@ namespace storm {
modules::ModuleSettings const& SettingsManager::getModule(std::string const& moduleName) const {
auto moduleIterator = this->modules.find(moduleName);
- LOG_THROW(moduleIterator != this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown module '" << moduleName << "'.");
+ STORM_LOG_THROW(moduleIterator != this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown module '" << moduleName << "'.");
return *moduleIterator->second;
}
modules::ModuleSettings& SettingsManager::getModule(std::string const& moduleName) {
auto moduleIterator = this->modules.find(moduleName);
- LOG_THROW(moduleIterator != this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown module '" << moduleName << "'.");
+ STORM_LOG_THROW(moduleIterator != this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown module '" << moduleName << "'.");
return *moduleIterator->second;
}
@@ -292,12 +292,12 @@ namespace storm {
void SettingsManager::setOptionsArguments(std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache) {
auto optionIterator = optionMap.find(optionName);
- LOG_THROW(optionIterator != optionMap.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");
+ STORM_LOG_THROW(optionIterator != optionMap.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");
// Iterate over all options and set the arguments.
for (auto& option : optionIterator->second) {
option->setHasOptionBeenSet();
- LOG_THROW(argumentCache.size() <= option->getArgumentCount(), storm::exceptions::OptionParserException, "Too many arguments for option '" << optionName << "'.");
+ STORM_LOG_THROW(argumentCache.size() <= option->getArgumentCount(), storm::exceptions::OptionParserException, "Too many arguments for option '" << optionName << "'.");
// Now set the provided argument values one by one.
for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) {
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index b14235a60..94d309813 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -27,7 +27,7 @@
#include "src/settings/modules/GlpkSettings.h"
#include "src/settings/modules/GurobiSettings.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/OptionParserException.h"
namespace storm {
diff --git a/src/settings/modules/CuddSettings.cpp b/src/settings/modules/CuddSettings.cpp
index 6404b77ac..c494b5ca6 100644
--- a/src/settings/modules/CuddSettings.cpp
+++ b/src/settings/modules/CuddSettings.cpp
@@ -85,7 +85,7 @@ namespace storm {
} else if (reorderingTechniqueAsString == "exact") {
return CuddSettings::ReorderingTechnique::Exact;
}
- LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << reorderingTechniqueAsString << "' set as reordering technique of Cudd.");
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << reorderingTechniqueAsString << "' set as reordering technique of Cudd.");
}
} // namespace modules
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 1675f1f48..fb3f89352 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -22,8 +22,11 @@ namespace storm {
const std::string GeneralSettings::symbolicOptionName = "symbolic";
const std::string GeneralSettings::symbolicOptionShortName = "s";
const std::string GeneralSettings::pctlOptionName = "pctl";
+ const std::string GeneralSettings::pctlFileOptionName = "pctlfile";
const std::string GeneralSettings::cslOptionName = "csl";
+ const std::string GeneralSettings::cslFileOptionName = "cslfile";
const std::string GeneralSettings::ltlOptionName = "ltl";
+ const std::string GeneralSettings::ltlFileOptionName = "ltlfile";
const std::string GeneralSettings::transitionRewardsOptionName = "transrew";
const std::string GeneralSettings::stateRewardsOptionName = "staterew";
const std::string GeneralSettings::counterexampleOptionName = "counterexample";
@@ -53,11 +56,17 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
+ this->addOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies a PCTL formula that is to be checked on the model.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, pctlFileOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the PCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "Specifies the CSL formulas that are to be checked on the model.")
+ this->addOption(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "Specifies a CSL formula that is to be checked on the model.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, cslFileOptionName, false, "Specifies the CSL formulas that are to be checked on the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "Specifies the LTL formulas that are to be checked on the model.")
+ this->addOption(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "Specifies an LTL formula that is to be checked on the model.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, ltlFileOptionName, false, "Specifies the LTL formulas that are to be checked on the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").build()).build());
@@ -136,26 +145,50 @@ namespace storm {
return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString();
}
- bool GeneralSettings::isPctlSet() const {
+ bool GeneralSettings::isPctlPropertySet() const {
return this->getOption(pctlOptionName).getHasOptionBeenSet();
}
+ std::string GeneralSettings::getPctlProperty() const {
+ return this->getOption(pctlOptionName).getArgumentByName("formula").getValueAsString();
+ }
+
+ bool GeneralSettings::isPctlFileSet() const {
+ return this->getOption(pctlFileOptionName).getHasOptionBeenSet();
+ }
+
std::string GeneralSettings::getPctlPropertiesFilename() const {
- return this->getOption(pctlOptionName).getArgumentByName("filename").getValueAsString();
+ return this->getOption(pctlFileOptionName).getArgumentByName("filename").getValueAsString();
}
- bool GeneralSettings::isCslSet() const {
+ bool GeneralSettings::isCslPropertySet() const {
return this->getOption(cslOptionName).getHasOptionBeenSet();
}
+ std::string GeneralSettings::getCslProperty() const {
+ return this->getOption(cslOptionName).getArgumentByName("formula").getValueAsString();
+ }
+
+ bool GeneralSettings::isCslFileSet() const {
+ return this->getOption(cslFileOptionName).getHasOptionBeenSet();
+ }
+
std::string GeneralSettings::getCslPropertiesFilename() const {
return this->getOption(cslOptionName).getArgumentByName("filename").getValueAsString();
}
- bool GeneralSettings::isLtlSet() const {
+ bool GeneralSettings::isLtlPropertySet() const {
return this->getOption(ltlOptionName).getHasOptionBeenSet();
}
+ std::string GeneralSettings::getLtlProperty() const {
+ return this->getOption(ltlOptionName).getArgumentByName("formula").getValueAsString();
+ }
+
+ bool GeneralSettings::isLtlFileSet() const {
+ return this->getOption(ltlFileOptionName).getHasOptionBeenSet();
+ }
+
std::string GeneralSettings::getLtlPropertiesFilename() const {
return this->getOption(ltlOptionName).getArgumentByName("filename").getValueAsString();
}
@@ -207,7 +240,7 @@ namespace storm {
} else if (equationSolverName == "native") {
return GeneralSettings::EquationSolver::Native;
}
- LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'.");
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'.");
}
GeneralSettings::LpSolver GeneralSettings::getLpSolver() const {
@@ -217,7 +250,7 @@ namespace storm {
} else if (lpSolverName == "glpk") {
return GeneralSettings::LpSolver::glpk;
}
- LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'.");
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'.");
}
bool GeneralSettings::isConstantsSet() const {
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index faac6492c..e37030385 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -125,7 +125,21 @@ namespace storm {
*
* @return True if the pctl option was set.
*/
- bool isPctlSet() const;
+ bool isPctlPropertySet() const;
+
+ /*!
+ * Retrieves the property specified with the pctl option.
+ *
+ * @return The property specified with the pctl option.
+ */
+ std::string getPctlProperty() const;
+
+ /*!
+ * Retrieves whether the pctl-file option was set.
+ *
+ * @return True iff the pctl-file option was set.
+ */
+ bool isPctlFileSet() const;
/*!
* Retrieves the name of the file that contains the PCTL properties to be checked on the model.
@@ -139,8 +153,22 @@ namespace storm {
*
* @return True if the csl option was set.
*/
- bool isCslSet() const;
+ bool isCslPropertySet() const;
+ /*!
+ * Retrieves the property specified with the csl option.
+ *
+ * @return The property specified with the csl option.
+ */
+ std::string getCslProperty() const;
+
+ /*!
+ * Retrieves whether the csl-file option was set.
+ *
+ * @return True iff the csl-file option was set.
+ */
+ bool isCslFileSet() const;
+
/*!
* Retrieves the name of the file that contains the CSL properties to be checked on the model.
*
@@ -153,8 +181,22 @@ namespace storm {
*
* @return True if the ltl option was set.
*/
- bool isLtlSet() const;
+ bool isLtlPropertySet() const;
+ /*!
+ * Retrieves the property specified with the ltl option.
+ *
+ * @return The property specified with the ltl option.
+ */
+ std::string getLtlProperty() const;
+
+ /*!
+ * Retrieves whether the ltl-file option was set.
+ *
+ * @return True iff the ltl-file option was set.
+ */
+ bool isLtlFileSet() const;
+
/*!
* Retrieves the name of the file that contains the LTL properties to be checked on the model.
*
@@ -291,8 +333,11 @@ namespace storm {
static const std::string symbolicOptionName;
static const std::string symbolicOptionShortName;
static const std::string pctlOptionName;
+ static const std::string pctlFileOptionName;
static const std::string cslOptionName;
+ static const std::string cslFileOptionName;
static const std::string ltlOptionName;
+ static const std::string ltlFileOptionName;
static const std::string transitionRewardsOptionName;
static const std::string stateRewardsOptionName;
static const std::string counterexampleOptionName;
diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp
index 434fc275f..c9c8b1840 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.cpp
+++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp
@@ -43,7 +43,7 @@ namespace storm {
} else if (linearEquationSystemTechniqueAsString == "jacobi") {
return GmmxxEquationSolverSettings::LinearEquationTechnique::Jacobi;
}
- LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
}
GmmxxEquationSolverSettings::PreconditioningTechnique GmmxxEquationSolverSettings::getPreconditioningTechnique() const {
@@ -55,7 +55,7 @@ namespace storm {
} else if (preconditioningTechniqueAsString == "none") {
return GmmxxEquationSolverSettings::PreconditioningTechnique::None;
}
- LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown preconditioning technique '" << preconditioningTechniqueAsString << "' selected.");
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown preconditioning technique '" << preconditioningTechniqueAsString << "' selected.");
}
uint_fast64_t GmmxxEquationSolverSettings::getRestartIterationCount() const {
diff --git a/src/settings/modules/ModuleSettings.cpp b/src/settings/modules/ModuleSettings.cpp
index a45c2f6ad..f29e15109 100644
--- a/src/settings/modules/ModuleSettings.cpp
+++ b/src/settings/modules/ModuleSettings.cpp
@@ -33,13 +33,13 @@ namespace storm {
Option const& ModuleSettings::getOption(std::string const& longName) const {
auto optionIterator = this->optionMap.find(longName);
- LOG_THROW(optionIterator != this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
+ STORM_LOG_THROW(optionIterator != this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
return *optionIterator->second;
}
Option& ModuleSettings::getOption(std::string const& longName) {
auto optionIterator = this->optionMap.find(longName);
- LOG_THROW(optionIterator != this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
+ STORM_LOG_THROW(optionIterator != this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
return *optionIterator->second;
}
@@ -63,7 +63,7 @@ namespace storm {
void ModuleSettings::addOption(std::shared_ptr<Option> const& option) {
auto optionIterator = this->optionMap.find(option->getLongName());
- LOG_THROW(optionIterator == this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register the option '" << option->getLongName() << "' in module '" << this->getModuleName() << "', because an option with this name already exists.");
+ STORM_LOG_THROW(optionIterator == this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register the option '" << option->getLongName() << "' in module '" << this->getModuleName() << "', because an option with this name already exists.");
this->optionMap.emplace(option->getLongName(), option);
this->options.push_back(option);
}
diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp
index cdde61942..b03feece6 100644
--- a/src/settings/modules/NativeEquationSolverSettings.cpp
+++ b/src/settings/modules/NativeEquationSolverSettings.cpp
@@ -29,7 +29,7 @@ namespace storm {
if (linearEquationSystemTechniqueAsString == "jacobi") {
return NativeEquationSolverSettings::LinearEquationTechnique::Jacobi;
}
- LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
}
uint_fast64_t NativeEquationSolverSettings::getMaximalIterationCount() const {
diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp
index b61679929..e902dc8f9 100644
--- a/src/solver/GlpkLpSolver.cpp
+++ b/src/solver/GlpkLpSolver.cpp
@@ -7,7 +7,7 @@
#include "src/storage/expressions/LinearCoefficientVisitor.h"
#include "src/settings/SettingsManager.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidAccessException.h"
#include "src/exceptions/InvalidStateException.h"
@@ -91,13 +91,13 @@ namespace storm {
void GlpkLpSolver::addVariable(std::string const& name, int variableType, int boundType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
// Check whether variable already exists.
auto nameIndexPair = this->variableNameToIndexMap.find(name);
- LOG_THROW(nameIndexPair == this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Variable '" << nameIndexPair->first << "' already exists.");
+ STORM_LOG_THROW(nameIndexPair == this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Variable '" << nameIndexPair->first << "' already exists.");
// Check for valid variable type.
- LOG_ASSERT(variableType == GLP_CV || variableType == GLP_IV || variableType == GLP_BV, "Illegal type '" << variableType << "' for glpk variable.");
+ STORM_LOG_ASSERT(variableType == GLP_CV || variableType == GLP_IV || variableType == GLP_BV, "Illegal type '" << variableType << "' for glpk variable.");
// Check for valid bound type.
- LOG_ASSERT(boundType == GLP_FR || boundType == GLP_UP || boundType == GLP_LO || boundType == GLP_DB, "Illegal bound type for variable '" << name << "'.");
+ STORM_LOG_ASSERT(boundType == GLP_FR || boundType == GLP_UP || boundType == GLP_LO || boundType == GLP_DB, "Illegal bound type for variable '" << name << "'.");
// Finally, create the actual variable.
glp_add_cols(this->lp, 1);
@@ -118,8 +118,8 @@ namespace storm {
glp_add_rows(this->lp, 1);
glp_set_row_name(this->lp, nextConstraintIndex, name.c_str());
- LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
- LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
+ STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
+ STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
std::pair<storm::expressions::SimpleValuation, double> leftCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(0));
std::pair<storm::expressions::SimpleValuation, double> rightCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(1));
@@ -137,7 +137,7 @@ namespace storm {
std::vector<double> coefficients;
for (auto const& identifier : leftCoefficients.first.getDoubleIdentifiers()) {
auto identifierIndexPair = this->variableNameToIndexMap.find(identifier);
- LOG_THROW(identifierIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Constraint contains illegal identifier '" << identifier << "'.");
+ STORM_LOG_THROW(identifierIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Constraint contains illegal identifier '" << identifier << "'.");
variables.push_back(identifierIndexPair->second);
coefficients.push_back(leftCoefficients.first.getDoubleValue(identifier));
}
@@ -160,7 +160,7 @@ namespace storm {
glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_FX, rightCoefficients.second, rightCoefficients.second);
break;
default:
- LOG_ASSERT(false, "Illegal operator in LP solver constraint.");
+ STORM_LOG_ASSERT(false, "Illegal operator in LP solver constraint.");
}
// Record the variables and coefficients in the coefficient matrix.
@@ -206,7 +206,7 @@ namespace storm {
error = glp_simplex(this->lp, nullptr);
}
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to optimize glpk model (" << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to optimize glpk model (" << error << ").");
this->currentModelHasBeenOptimized = true;
}
@@ -250,13 +250,13 @@ namespace storm {
double GlpkLpSolver::getContinuousValue(std::string const& name) const {
if (!this->isOptimal()) {
- LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
- LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
+ STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
+ STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
}
auto variableIndexPair = this->variableNameToIndexMap.find(name);
- LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+ STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
double value = 0;
if (this->modelContainsIntegerVariables) {
@@ -269,13 +269,13 @@ namespace storm {
int_fast64_t GlpkLpSolver::getIntegerValue(std::string const& name) const {
if (!this->isOptimal()) {
- LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
- LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
+ STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
+ STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
}
auto variableIndexPair = this->variableNameToIndexMap.find(name);
- LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+ STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
double value = 0;
if (this->modelContainsIntegerVariables) {
@@ -285,20 +285,20 @@ namespace storm {
}
// Now check the desired precision was actually achieved.
- LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::glpkSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in glpk solution (" << value << ").");
+ STORM_LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::glpkSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in glpk solution (" << value << ").");
return static_cast<int_fast64_t>(value);
}
bool GlpkLpSolver::getBinaryValue(std::string const& name) const {
if (!this->isOptimal()) {
- LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
- LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
+ STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
+ STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
}
auto variableIndexPair = this->variableNameToIndexMap.find(name);
- LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+ STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
double value = 0;
if (this->modelContainsIntegerVariables) {
@@ -307,16 +307,16 @@ namespace storm {
value = glp_get_col_prim(this->lp, static_cast<int>(variableIndexPair->second));
}
- LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::glpkSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for binary variable in glpk solution (" << value << ").");
+ STORM_LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::glpkSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for binary variable in glpk solution (" << value << ").");
return static_cast<bool>(value);
}
double GlpkLpSolver::getObjectiveValue() const {
if (!this->isOptimal()) {
- LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
- LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
+ STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
+ STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
}
double value = 0;
diff --git a/src/solver/GurobiLpSolver.cpp b/src/solver/GurobiLpSolver.cpp
index 519062b28..957c4f8e7 100644
--- a/src/solver/GurobiLpSolver.cpp
+++ b/src/solver/GurobiLpSolver.cpp
@@ -6,7 +6,7 @@
#include "src/storage/expressions/LinearCoefficientVisitor.h"
#include "src/settings/SettingsManager.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/InvalidAccessException.h"
@@ -55,20 +55,20 @@ namespace storm {
// Enable the following line to only print the output of Gurobi if the debug flag is set.
error = GRBsetintparam(env, "OutputFlag", storm::settings::debugSettings().isDebugSet() || storm::settings::gurobiSettings().isOutputSet() ? 1 : 0);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter OutputFlag (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter OutputFlag (" << GRBgeterrormsg(env) << ", error code " << error << ").");
// Enable the following line to restrict Gurobi to one thread only.
error = GRBsetintparam(env, "Threads", storm::settings::gurobiSettings().getNumberOfThreads());
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter Threads (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter Threads (" << GRBgeterrormsg(env) << ", error code " << error << ").");
// Enable the following line to force Gurobi to be as precise about the binary variables as required by the given precision option.
error = GRBsetdblparam(env, "IntFeasTol", storm::settings::gurobiSettings().getIntegerTolerance());
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ").");
}
void GurobiLpSolver::update() const {
int error = GRBupdatemodel(model);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to update Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to update Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
// Since the model changed, we erase the optimality flag.
this->currentModelHasBeenOptimized = false;
@@ -113,22 +113,22 @@ namespace storm {
void GurobiLpSolver::addVariable(std::string const& name, char variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
// Check whether variable already exists.
auto nameIndexPair = this->variableNameToIndexMap.find(name);
- LOG_THROW(nameIndexPair == this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Variable '" << nameIndexPair->first << "' already exists.");
+ STORM_LOG_THROW(nameIndexPair == this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Variable '" << nameIndexPair->first << "' already exists.");
// Check for valid variable type.
- LOG_ASSERT(variableType == GRB_CONTINUOUS || variableType == GRB_INTEGER || variableType == GRB_BINARY, "Illegal type '" << variableType << "' for Gurobi variable.");
+ STORM_LOG_ASSERT(variableType == GRB_CONTINUOUS || variableType == GRB_INTEGER || variableType == GRB_BINARY, "Illegal type '" << variableType << "' for Gurobi variable.");
// Finally, create the actual variable.
int error = 0;
error = GRBaddvar(model, 0, nullptr, nullptr, objectiveFunctionCoefficient, lowerBound, upperBound, variableType, name.c_str());
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not create binary Gurobi variable (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not create binary Gurobi variable (" << GRBgeterrormsg(env) << ", error code " << error << ").");
this->variableNameToIndexMap.emplace(name, nextVariableIndex);
++nextVariableIndex;
}
void GurobiLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) {
- LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
- LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
+ STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
+ STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
std::pair<storm::expressions::SimpleValuation, double> leftCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(0));
std::pair<storm::expressions::SimpleValuation, double> rightCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(1));
@@ -146,7 +146,7 @@ namespace storm {
std::vector<double> coefficients;
for (auto const& identifier : leftCoefficients.first.getDoubleIdentifiers()) {
auto identifierIndexPair = this->variableNameToIndexMap.find(identifier);
- LOG_THROW(identifierIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Constraint contains illegal identifier '" << identifier << "'.");
+ STORM_LOG_THROW(identifierIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Constraint contains illegal identifier '" << identifier << "'.");
variables.push_back(identifierIndexPair->second);
coefficients.push_back(leftCoefficients.first.getDoubleValue(identifier));
}
@@ -170,9 +170,9 @@ namespace storm {
error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_EQUAL, rightCoefficients.second, name == "" ? nullptr : name.c_str());
break;
default:
- LOG_ASSERT(false, "Illegal operator in LP solver constraint.");
+ STORM_LOG_ASSERT(false, "Illegal operator in LP solver constraint.");
}
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not assert constraint (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not assert constraint (" << GRBgeterrormsg(env) << ", error code " << error << ").");
}
void GurobiLpSolver::optimize() const {
@@ -181,11 +181,11 @@ namespace storm {
// Set the most recently set model sense.
int error = GRBsetintattr(model, "ModelSense", this->getModelSense() == ModelSense::Minimize ? 1 : -1);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi model sense (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi model sense (" << GRBgeterrormsg(env) << ", error code " << error << ").");
// Then we actually optimize the model.
error = GRBoptimize(model);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to optimize Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to optimize Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
this->currentModelHasBeenOptimized = true;
}
@@ -198,21 +198,21 @@ namespace storm {
int optimalityStatus = 0;
int error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &optimalityStatus);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
// By default, Gurobi may tell us only that the model is either infeasible or unbounded. To decide which one
// it is, we need to perform an extra step.
if (optimalityStatus == GRB_INF_OR_UNBD) {
error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_DUALREDUCTIONS, 0);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi parameter (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi parameter (" << GRBgeterrormsg(env) << ", error code " << error << ").");
this->optimize();
error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &optimalityStatus);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_DUALREDUCTIONS, 1);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi parameter (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi parameter (" << GRBgeterrormsg(env) << ", error code " << error << ").");
}
return optimalityStatus == GRB_INFEASIBLE;
@@ -226,21 +226,21 @@ namespace storm {
int optimalityStatus = 0;
int error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &optimalityStatus);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
// By default, Gurobi may tell us only that the model is either infeasible or unbounded. To decide which one
// it is, we need to perform an extra step.
if (optimalityStatus == GRB_INF_OR_UNBD) {
error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_DUALREDUCTIONS, 0);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi parameter (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi parameter (" << GRBgeterrormsg(env) << ", error code " << error << ").");
this->optimize();
error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &optimalityStatus);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_DUALREDUCTIONS, 1);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi parameter (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi parameter (" << GRBgeterrormsg(env) << ", error code " << error << ").");
}
return optimalityStatus == GRB_UNBOUNDED;
@@ -253,64 +253,64 @@ namespace storm {
int optimalityStatus = 0;
int error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &optimalityStatus);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
return optimalityStatus == GRB_OPTIMAL;
}
double GurobiLpSolver::getContinuousValue(std::string const& name) const {
if (!this->isOptimal()) {
- LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
- LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
}
auto variableIndexPair = this->variableNameToIndexMap.find(name);
- LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+ STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
double value = 0;
int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableIndexPair->second, &value);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
return value;
}
int_fast64_t GurobiLpSolver::getIntegerValue(std::string const& name) const {
if (!this->isOptimal()) {
- LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
- LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
}
auto variableIndexPair = this->variableNameToIndexMap.find(name);
- LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+ STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
double value = 0;
int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableIndexPair->second, &value);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
- LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::gurobiSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::gurobiSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
return static_cast<int_fast64_t>(value);
}
bool GurobiLpSolver::getBinaryValue(std::string const& name) const {
if (!this->isOptimal()) {
- LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
- LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
}
auto variableIndexPair = this->variableNameToIndexMap.find(name);
- LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+ STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
double value = 0;
int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableIndexPair->second, &value);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
if (value > 0.5) {
- LOG_THROW(std::abs(static_cast<int>(value) - 1) <= storm::settings::gurobiSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
+ STORM_LOG_THROW(std::abs(static_cast<int>(value) - 1) <= storm::settings::gurobiSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
} else {
- LOG_THROW(value <= storm::settings::gurobiSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
+ STORM_LOG_THROW(value <= storm::settings::gurobiSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
}
return static_cast<bool>(value);
@@ -318,14 +318,14 @@ namespace storm {
double GurobiLpSolver::getObjectiveValue() const {
if (!this->isOptimal()) {
- LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
- LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
}
double value = 0;
int error = GRBgetdblattr(model, GRB_DBL_ATTR_OBJVAL, &value);
- LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
return value;
}
diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp
index 11c6bd43f..afe6e1508 100644
--- a/src/solver/Z3SmtSolver.cpp
+++ b/src/solver/Z3SmtSolver.cpp
@@ -15,7 +15,7 @@ namespace storm {
z3::expr z3ExprValuation = m_model.eval(z3Expr, true);
return this->m_adapter.translateExpression(z3ExprValuation).evaluateAsBool();
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -25,7 +25,7 @@ namespace storm {
z3::expr z3ExprValuation = m_model.eval(z3Expr, true);
return this->m_adapter.translateExpression(z3ExprValuation).evaluateAsInt();
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -47,7 +47,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->m_solver.push();
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -56,7 +56,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->m_solver.pop();
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -65,7 +65,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->m_solver.pop((unsigned int)n);
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -74,7 +74,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->m_solver.reset();
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -83,7 +83,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->m_solver.add(m_adapter.translateExpression(e, true));
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -104,7 +104,7 @@ namespace storm {
}
return this->lastResult;
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -131,7 +131,7 @@ namespace storm {
}
return this->lastResult;
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -158,7 +158,7 @@ namespace storm {
}
return this->lastResult;
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -166,11 +166,11 @@ namespace storm {
{
#ifdef STORM_HAVE_Z3
- LOG_THROW(this->lastResult == SmtSolver::CheckResult::SAT, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT.");
+ STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::SAT, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT.");
return this->z3ModelToStorm(this->m_solver.get_model());
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -193,7 +193,7 @@ namespace storm {
stormModel.addDoubleIdentifier(var_i.name().str(), var_i_interp.evaluateAsDouble());
break;
default:
- LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.")
+ STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.")
break;
}
@@ -214,7 +214,7 @@ namespace storm {
return valuations;
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -263,7 +263,7 @@ namespace storm {
return numModels;
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -304,7 +304,7 @@ namespace storm {
return numModels;
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -327,7 +327,7 @@ namespace storm {
return unsatAssumptions;
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
}
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index e52bd87ef..8373d286a 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -9,7 +9,7 @@
#include "src/storage/SparseMatrix.h"
#include "src/exceptions/InvalidStateException.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
@@ -110,16 +110,16 @@ namespace storm {
// In case we did not expect this value, we throw an exception.
if (forceInitialDimensions) {
- LOG_THROW(!initialRowCountSet || lastRow < initialRowCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal row " << lastRow << ".");
- LOG_THROW(!initialColumnCountSet || lastColumn < initialColumnCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal column " << lastColumn << ".");
- LOG_THROW(!initialEntryCountSet || currentEntryCount <= initialEntryCount, storm::exceptions::OutOfRangeException, "Too many entries in matrix, expected only " << initialEntryCount << ".");
+ STORM_LOG_THROW(!initialRowCountSet || lastRow < initialRowCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal row " << lastRow << ".");
+ STORM_LOG_THROW(!initialColumnCountSet || lastColumn < initialColumnCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal column " << lastColumn << ".");
+ STORM_LOG_THROW(!initialEntryCountSet || currentEntryCount <= initialEntryCount, storm::exceptions::OutOfRangeException, "Too many entries in matrix, expected only " << initialEntryCount << ".");
}
}
template<typename ValueType>
void SparseMatrixBuilder<ValueType>::newRowGroup(index_type startingRow) {
- LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping.");
- LOG_THROW(rowGroupIndices.empty() || startingRow >= rowGroupIndices.back(), storm::exceptions::InvalidStateException, "Illegal row group with negative size.");
+ STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping.");
+ STORM_LOG_THROW(rowGroupIndices.empty() || startingRow >= rowGroupIndices.back(), storm::exceptions::InvalidStateException, "Illegal row group with negative size.");
rowGroupIndices.push_back(startingRow);
++currentRowGroup;
}
@@ -128,7 +128,7 @@ namespace storm {
SparseMatrix<ValueType> SparseMatrixBuilder<ValueType>::build(index_type overriddenRowCount, index_type overriddenColumnCount, index_type overriddenRowGroupCount) {
uint_fast64_t rowCount = lastRow + 1;
if (initialRowCountSet && forceInitialDimensions) {
- LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << ".");
+ STORM_LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << ".");
rowCount = std::max(rowCount, initialRowCount);
}
rowCount = std::max(rowCount, overriddenRowCount);
@@ -145,14 +145,14 @@ namespace storm {
uint_fast64_t columnCount = highestColumn + 1;
if (initialColumnCountSet && forceInitialDimensions) {
- LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << ".");
+ STORM_LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << ".");
columnCount = std::max(columnCount, initialColumnCount);
}
columnCount = std::max(columnCount, overriddenColumnCount);
uint_fast64_t entryCount = currentEntryCount;
if (initialEntryCountSet && forceInitialDimensions) {
- LOG_THROW(entryCount == initialEntryCount, storm::exceptions::InvalidStateException, "Expected " << initialEntryCount << " entries, but got " << entryCount << ".");
+ STORM_LOG_THROW(entryCount == initialEntryCount, storm::exceptions::InvalidStateException, "Expected " << initialEntryCount << " entries, but got " << entryCount << ".");
}
// Check whether row groups are missing some entries.
@@ -163,7 +163,7 @@ namespace storm {
} else {
uint_fast64_t rowGroupCount = currentRowGroup;
if (initialRowGroupCountSet && forceInitialDimensions) {
- LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << ".");
+ STORM_LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << ".");
rowGroupCount = std::max(rowGroupCount, initialRowGroupCount);
}
rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount);
diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp
index 4a990746e..dd1f58189 100644
--- a/src/storage/dd/CuddDdForwardIterator.cpp
+++ b/src/storage/dd/CuddDdForwardIterator.cpp
@@ -1,7 +1,7 @@
#include "src/storage/dd/CuddDdForwardIterator.h"
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/DdMetaVariable.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
namespace storm {
namespace dd {
@@ -63,7 +63,7 @@ namespace storm {
}
DdForwardIterator<DdType::CUDD>& DdForwardIterator<DdType::CUDD>::operator++() {
- LOG_ASSERT(!this->isAtEnd, "Illegally incrementing iterator that is already at its end.");
+ STORM_LOG_ASSERT(!this->isAtEnd, "Illegally incrementing iterator that is already at its end.");
// If there were no (relevant) don't cares or we have enumerated all combination, we need to eliminate the
// found solutions and get the next "first" cube.
diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
index cd19fa037..21a1d3d7f 100644
--- a/src/storage/dd/CuddDdManager.cpp
+++ b/src/storage/dd/CuddDdManager.cpp
@@ -3,7 +3,7 @@
#include <algorithm>
#include "src/storage/dd/CuddDdManager.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/settings/SettingsManager.h"
@@ -52,7 +52,7 @@ namespace storm {
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(std::string const& metaVariableName, int_fast64_t value) {
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
- LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << metaVariableName << "'.");
+ STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << metaVariableName << "'.");
// Now compute the encoding relative to the low value of the meta variable.
value -= metaVariable.getLow();
@@ -100,13 +100,13 @@ namespace storm {
void DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
// Check whether the variable name is legal.
- LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
+ STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
// Check whether a meta variable already exists.
- LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
+ STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
// Check that the range is legal.
- LOG_THROW(high != low, storm::exceptions::InvalidArgumentException, "Range of meta variable must be at least 2 elements.");
+ STORM_LOG_THROW(high != low, storm::exceptions::InvalidArgumentException, "Range of meta variable must be at least 2 elements.");
std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
@@ -128,10 +128,10 @@ namespace storm {
void DdManager<DdType::CUDD>::addMetaVariable(std::string const& name) {
// Check whether the variable name is legal.
- LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
+ STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
// Check whether a meta variable already exists.
- LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
+ STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
std::vector<Dd<DdType::CUDD>> variables;
std::vector<Dd<DdType::CUDD>> variablesPrime;
@@ -149,7 +149,7 @@ namespace storm {
auto const& nameVariablePair = metaVariableMap.find(metaVariableName);
// Check whether the meta variable exists.
- LOG_THROW(nameVariablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << metaVariableName << "'.");
+ STORM_LOG_THROW(nameVariablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << metaVariableName << "'.");
return nameVariablePair->second;
}
diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp
index 38a0604e2..753b4a129 100644
--- a/src/storage/expressions/BaseExpression.cpp
+++ b/src/storage/expressions/BaseExpression.cpp
@@ -1,5 +1,5 @@
#include "src/storage/expressions/BaseExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
#include "src/exceptions/InvalidAccessException.h"
@@ -26,15 +26,15 @@ namespace storm {
}
int_fast64_t BaseExpression::evaluateAsInt(Valuation const* valuation) const {
- LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
}
bool BaseExpression::evaluateAsBool(Valuation const* valuation) const {
- LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
}
double BaseExpression::evaluateAsDouble(Valuation const* valuation) const {
- LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
}
uint_fast64_t BaseExpression::getArity() const {
@@ -42,15 +42,15 @@ namespace storm {
}
std::shared_ptr<BaseExpression const> BaseExpression::getOperand(uint_fast64_t operandIndex) const {
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 0.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 0.");
}
std::string const& BaseExpression::getIdentifier() const {
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access identifier of non-constant, non-variable expression.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access identifier of non-constant, non-variable expression.");
}
OperatorType BaseExpression::getOperator() const {
- LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access operator of non-function application expression.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access operator of non-function application expression.");
}
bool BaseExpression::containsVariables() const {
diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
index 061c231af..9a9d81fe5 100644
--- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
+++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
@@ -1,6 +1,6 @@
#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
#include "src/storage/expressions/BooleanLiteralExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
namespace storm {
@@ -24,7 +24,7 @@ namespace storm {
}
bool BinaryBooleanFunctionExpression::evaluateAsBool(Valuation const* valuation) const {
- LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
+ STORM_LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
bool firstOperandEvaluation = this->getFirstOperand()->evaluateAsBool(valuation);
bool secondOperandEvaluation = this->getSecondOperand()->evaluateAsBool(valuation);
diff --git a/src/storage/expressions/BinaryExpression.cpp b/src/storage/expressions/BinaryExpression.cpp
index bdb7fb59f..78fbdaf73 100644
--- a/src/storage/expressions/BinaryExpression.cpp
+++ b/src/storage/expressions/BinaryExpression.cpp
@@ -1,6 +1,6 @@
#include "src/storage/expressions/BinaryExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidAccessException.h"
namespace storm {
@@ -44,7 +44,7 @@ namespace storm {
}
std::shared_ptr<BaseExpression const> BinaryExpression::getOperand(uint_fast64_t operandIndex) const {
- LOG_THROW(operandIndex < 2, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 2.");
+ STORM_LOG_THROW(operandIndex < 2, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 2.");
if (operandIndex == 0) {
return this->getFirstOperand();
} else {
diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
index 7db4fa0cf..18b1d3a71 100644
--- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
+++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
@@ -2,7 +2,7 @@
#include <cmath>
#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
namespace storm {
@@ -28,7 +28,7 @@ namespace storm {
}
int_fast64_t BinaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const {
- LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
+ STORM_LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
int_fast64_t firstOperandEvaluation = this->getFirstOperand()->evaluateAsInt(valuation);
int_fast64_t secondOperandEvaluation = this->getSecondOperand()->evaluateAsInt(valuation);
@@ -44,7 +44,7 @@ namespace storm {
}
double BinaryNumericalFunctionExpression::evaluateAsDouble(Valuation const* valuation) const {
- LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
+ STORM_LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
double firstOperandEvaluation = this->getFirstOperand()->evaluateAsDouble(valuation);
double secondOperandEvaluation = this->getSecondOperand()->evaluateAsDouble(valuation);
diff --git a/src/storage/expressions/BinaryRelationExpression.cpp b/src/storage/expressions/BinaryRelationExpression.cpp
index f31f97fce..4c0a2e1ae 100644
--- a/src/storage/expressions/BinaryRelationExpression.cpp
+++ b/src/storage/expressions/BinaryRelationExpression.cpp
@@ -1,6 +1,6 @@
#include "src/storage/expressions/BinaryRelationExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
namespace storm {
@@ -21,7 +21,7 @@ namespace storm {
}
bool BinaryRelationExpression::evaluateAsBool(Valuation const* valuation) const {
- LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
+ STORM_LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
double firstOperandEvaluated = this->getFirstOperand()->evaluateAsDouble(valuation);
double secondOperandEvaluated = this->getSecondOperand()->evaluateAsDouble(valuation);
diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp
index c61e93b9d..ad74066b3 100644
--- a/src/storage/expressions/Expression.cpp
+++ b/src/storage/expressions/Expression.cpp
@@ -8,7 +8,7 @@
#include "src/storage/expressions/LinearityCheckVisitor.h"
#include "src/storage/expressions/Expressions.h"
#include "src/exceptions/InvalidTypeException.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
namespace storm {
namespace expressions {
@@ -182,57 +182,57 @@ namespace storm {
}
Expression Expression::operator+(Expression const& other) const {
- LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '+' requires numerical operands.");
+ STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '+' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Plus)));
}
Expression Expression::operator-(Expression const& other) const {
- LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '-' requires numerical operands.");
+ STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '-' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Minus)));
}
Expression Expression::operator-() const {
- LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '-' requires numerical operand.");
+ STORM_LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '-' requires numerical operand.");
return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getReturnType(), this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Minus)));
}
Expression Expression::operator*(Expression const& other) const {
- LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '*' requires numerical operands.");
+ STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '*' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Times)));
}
Expression Expression::operator/(Expression const& other) const {
- LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '/' requires numerical operands.");
+ STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '/' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Divide)));
}
Expression Expression::operator^(Expression const& other) const {
- LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '^' requires numerical operands.");
+ STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '^' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Power)));
}
Expression Expression::operator&&(Expression const& other) const {
- LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands.");
+ STORM_LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And)));
}
Expression Expression::operator||(Expression const& other) const {
- LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '||' requires numerical operands.");
+ STORM_LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '||' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Or)));
}
Expression Expression::operator!() const {
- LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '!' requires boolean operand.");
+ STORM_LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '!' requires boolean operand.");
return Expression(std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), UnaryBooleanFunctionExpression::OperatorType::Not)));
}
Expression Expression::operator==(Expression const& other) const {
- LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '==' requires numerical operands.");
+ STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '==' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::Equal)));
}
Expression Expression::operator!=(Expression const& other) const {
- LOG_THROW((this->hasNumericalReturnType() && other.hasNumericalReturnType()) || (this->hasBooleanReturnType() && other.hasBooleanReturnType()), storm::exceptions::InvalidTypeException, "Operator '!=' requires operands of equal type.");
+ STORM_LOG_THROW((this->hasNumericalReturnType() && other.hasNumericalReturnType()) || (this->hasBooleanReturnType() && other.hasBooleanReturnType()), storm::exceptions::InvalidTypeException, "Operator '!=' requires operands of equal type.");
if (this->hasNumericalReturnType() && other.hasNumericalReturnType()) {
return Expression(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::NotEqual)));
} else {
@@ -241,58 +241,58 @@ namespace storm {
}
Expression Expression::operator>(Expression const& other) const {
- LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '>' requires numerical operands.");
+ STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '>' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::Greater)));
}
Expression Expression::operator>=(Expression const& other) const {
- LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '>=' requires numerical operands.");
+ STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '>=' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::GreaterOrEqual)));
}
Expression Expression::operator<(Expression const& other) const {
- LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '<' requires numerical operands.");
+ STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '<' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::Less)));
}
Expression Expression::operator<=(Expression const& other) const {
- LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '<=' requires numerical operands.");
+ STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '<=' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::LessOrEqual)));
}
Expression Expression::minimum(Expression const& lhs, Expression const& rhs) {
- LOG_THROW(lhs.hasNumericalReturnType() && rhs.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'min' requires numerical operands.");
+ STORM_LOG_THROW(lhs.hasNumericalReturnType() && rhs.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'min' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(lhs.getReturnType() == ExpressionReturnType::Int && rhs.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, lhs.getBaseExpressionPointer(), rhs.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Min)));
}
Expression Expression::maximum(Expression const& lhs, Expression const& rhs) {
- LOG_THROW(lhs.hasNumericalReturnType() && rhs.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'max' requires numerical operands.");
+ STORM_LOG_THROW(lhs.hasNumericalReturnType() && rhs.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'max' requires numerical operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(lhs.getReturnType() == ExpressionReturnType::Int && rhs.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, lhs.getBaseExpressionPointer(), rhs.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Max)));
}
Expression Expression::ite(Expression const& thenExpression, Expression const& elseExpression) {
- LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Condition of if-then-else operator must be of boolean type.");
- LOG_THROW(thenExpression.hasBooleanReturnType() && elseExpression.hasBooleanReturnType() || thenExpression.hasNumericalReturnType() && elseExpression.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "'then' and 'else' expression of if-then-else operator must have equal return type.");
+ STORM_LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Condition of if-then-else operator must be of boolean type.");
+ STORM_LOG_THROW(thenExpression.hasBooleanReturnType() && elseExpression.hasBooleanReturnType() || thenExpression.hasNumericalReturnType() && elseExpression.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "'then' and 'else' expression of if-then-else operator must have equal return type.");
return Expression(std::shared_ptr<BaseExpression>(new IfThenElseExpression(thenExpression.hasBooleanReturnType() && elseExpression.hasBooleanReturnType() ? ExpressionReturnType::Bool : (thenExpression.getReturnType() == ExpressionReturnType::Int && elseExpression.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double), this->getBaseExpressionPointer(), thenExpression.getBaseExpressionPointer(), elseExpression.getBaseExpressionPointer())));
}
Expression Expression::implies(Expression const& other) const {
- LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands.");
+ STORM_LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Implies)));
}
Expression Expression::iff(Expression const& other) const {
- LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands.");
+ STORM_LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Iff)));
}
Expression Expression::floor() const {
- LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand.");
+ STORM_LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand.");
return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(ExpressionReturnType::Int, this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Floor)));
}
Expression Expression::ceil() const {
- LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'ceil' requires numerical operand.");
+ STORM_LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'ceil' requires numerical operand.");
return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(ExpressionReturnType::Int, this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil)));
}
diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp
index 50c71af75..fb17fe142 100644
--- a/src/storage/expressions/IfThenElseExpression.cpp
+++ b/src/storage/expressions/IfThenElseExpression.cpp
@@ -1,6 +1,6 @@
#include "src/storage/expressions/IfThenElseExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidAccessException.h"
namespace storm {
@@ -10,7 +10,7 @@ namespace storm {
}
std::shared_ptr<BaseExpression const> IfThenElseExpression::getOperand(uint_fast64_t operandIndex) const {
- LOG_THROW(operandIndex < 3, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 3.");
+ STORM_LOG_THROW(operandIndex < 3, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 3.");
if (operandIndex == 0) {
return this->getCondition();
} else if (operandIndex == 1) {
diff --git a/src/storage/expressions/LinearCoefficientVisitor.cpp b/src/storage/expressions/LinearCoefficientVisitor.cpp
index 7525d6dde..dce0b4ece 100644
--- a/src/storage/expressions/LinearCoefficientVisitor.cpp
+++ b/src/storage/expressions/LinearCoefficientVisitor.cpp
@@ -1,7 +1,7 @@
#include "src/storage/expressions/LinearCoefficientVisitor.h"
#include "src/storage/expressions/Expressions.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
@@ -12,11 +12,11 @@ namespace storm {
}
void LinearCoefficientVisitor::visit(IfThenElseExpression const* expression) {
- LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
}
void LinearCoefficientVisitor::visit(BinaryBooleanFunctionExpression const* expression) {
- LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
}
void LinearCoefficientVisitor::visit(BinaryNumericalFunctionExpression const* expression) {
@@ -67,7 +67,7 @@ namespace storm {
std::pair<SimpleValuation, double>& rightResult = resultStack.top();
// If the expression is linear, either the left or the right side must not contain variables.
- LOG_THROW(leftResult.first.getNumberOfIdentifiers() == 0 || rightResult.first.getNumberOfIdentifiers() == 0, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
+ STORM_LOG_THROW(leftResult.first.getNumberOfIdentifiers() == 0 || rightResult.first.getNumberOfIdentifiers() == 0, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
if (leftResult.first.getNumberOfIdentifiers() == 0) {
for (auto const& identifier : rightResult.first.getDoubleIdentifiers()) {
rightResult.first.setDoubleValue(identifier, leftResult.second * rightResult.first.getDoubleValue(identifier));
@@ -87,7 +87,7 @@ namespace storm {
std::pair<SimpleValuation, double>& rightResult = resultStack.top();
// If the expression is linear, either the left or the right side must not contain variables.
- LOG_THROW(leftResult.first.getNumberOfIdentifiers() == 0 || rightResult.first.getNumberOfIdentifiers() == 0, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
+ STORM_LOG_THROW(leftResult.first.getNumberOfIdentifiers() == 0 || rightResult.first.getNumberOfIdentifiers() == 0, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
if (leftResult.first.getNumberOfIdentifiers() == 0) {
for (auto const& identifier : rightResult.first.getDoubleIdentifiers()) {
rightResult.first.setDoubleValue(identifier, leftResult.second / rightResult.first.getDoubleValue(identifier));
@@ -100,28 +100,28 @@ namespace storm {
rightResult.second = leftResult.second / leftResult.second;
return;
} else {
- LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
}
}
void LinearCoefficientVisitor::visit(BinaryRelationExpression const* expression) {
- LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
}
void LinearCoefficientVisitor::visit(VariableExpression const* expression) {
SimpleValuation valuation;
switch (expression->getReturnType()) {
- case ExpressionReturnType::Bool: LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); break;
+ case ExpressionReturnType::Bool: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); break;
case ExpressionReturnType::Int:
case ExpressionReturnType::Double: valuation.addDoubleIdentifier(expression->getVariableName(), 1); break;
- case ExpressionReturnType::Undefined: LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal expression return type."); break;
+ case ExpressionReturnType::Undefined: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal expression return type."); break;
}
resultStack.push(std::make_pair(valuation, 0));
}
void LinearCoefficientVisitor::visit(UnaryBooleanFunctionExpression const* expression) {
- LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
}
void LinearCoefficientVisitor::visit(UnaryNumericalFunctionExpression const* expression) {
@@ -132,12 +132,12 @@ namespace storm {
valuationConstantPair.first.setDoubleValue(identifier, -valuationConstantPair.first.getDoubleValue(identifier));
}
} else {
- LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
}
}
void LinearCoefficientVisitor::visit(BooleanLiteralExpression const* expression) {
- LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
}
void LinearCoefficientVisitor::visit(IntegerLiteralExpression const* expression) {
diff --git a/src/storage/expressions/LinearityCheckVisitor.cpp b/src/storage/expressions/LinearityCheckVisitor.cpp
index 6f595900a..78b6cf1f4 100644
--- a/src/storage/expressions/LinearityCheckVisitor.cpp
+++ b/src/storage/expressions/LinearityCheckVisitor.cpp
@@ -1,7 +1,7 @@
#include "src/storage/expressions/LinearityCheckVisitor.h"
#include "src/storage/expressions/Expressions.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
namespace storm {
diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp
index f50b1ef49..ae111c653 100644
--- a/src/storage/expressions/SimpleValuation.cpp
+++ b/src/storage/expressions/SimpleValuation.cpp
@@ -3,7 +3,7 @@
#include <set>
#include <boost/functional/hash.hpp>
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidAccessException.h"
@@ -14,17 +14,17 @@ namespace storm {
}
void SimpleValuation::addBooleanIdentifier(std::string const& name, bool initialValue) {
- LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
+ STORM_LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
this->identifierToValueMap.emplace(name, initialValue);
}
void SimpleValuation::addIntegerIdentifier(std::string const& name, int_fast64_t initialValue) {
- LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
+ STORM_LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
this->identifierToValueMap.emplace(name, initialValue);
}
void SimpleValuation::addDoubleIdentifier(std::string const& name, double initialValue) {
- LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
+ STORM_LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
this->identifierToValueMap.emplace(name, initialValue);
}
@@ -42,13 +42,13 @@ namespace storm {
void SimpleValuation::removeIdentifier(std::string const& name) {
auto nameValuePair = this->identifierToValueMap.find(name);
- LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Deleting unknown identifier '" << name << "'.");
+ STORM_LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Deleting unknown identifier '" << name << "'.");
this->identifierToValueMap.erase(nameValuePair);
}
ExpressionReturnType SimpleValuation::getIdentifierType(std::string const& name) const {
auto nameValuePair = this->identifierToValueMap.find(name);
- LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
+ STORM_LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
if (nameValuePair->second.type() == typeid(bool)) {
return ExpressionReturnType::Bool;
} else if (nameValuePair->second.type() == typeid(int_fast64_t)) {
@@ -84,19 +84,19 @@ namespace storm {
bool SimpleValuation::getBooleanValue(std::string const& name) const {
auto nameValuePair = this->identifierToValueMap.find(name);
- LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
+ STORM_LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
return boost::get<bool>(nameValuePair->second);
}
int_fast64_t SimpleValuation::getIntegerValue(std::string const& name) const {
auto nameValuePair = this->identifierToValueMap.find(name);
- LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
+ STORM_LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
return boost::get<int_fast64_t>(nameValuePair->second);
}
double SimpleValuation::getDoubleValue(std::string const& name) const {
auto nameValuePair = this->identifierToValueMap.find(name);
- LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
+ STORM_LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
return boost::get<double>(nameValuePair->second);
}
diff --git a/src/storage/expressions/TypeCheckVisitor.cpp b/src/storage/expressions/TypeCheckVisitor.cpp
index 521453042..11643abce 100644
--- a/src/storage/expressions/TypeCheckVisitor.cpp
+++ b/src/storage/expressions/TypeCheckVisitor.cpp
@@ -1,7 +1,7 @@
#include "src/storage/expressions/TypeCheckVisitor.h"
#include "src/storage/expressions/Expressions.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
namespace storm {
@@ -44,8 +44,8 @@ namespace storm {
template<typename MapType>
void TypeCheckVisitor<MapType>::visit(VariableExpression const* expression) {
auto identifierTypePair = this->identifierToTypeMap.find(expression->getVariableName());
- LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getVariableName() << "'.");
- LOG_THROW(identifierTypePair->second == expression->getReturnType(), storm::exceptions::InvalidTypeException, "Type mismatch for variable '" << expression->getVariableName() << "': expected '" << identifierTypePair->first << "', but found '" << expression->getReturnType() << "'.");
+ STORM_LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getVariableName() << "'.");
+ STORM_LOG_THROW(identifierTypePair->second == expression->getReturnType(), storm::exceptions::InvalidTypeException, "Type mismatch for variable '" << expression->getVariableName() << "': expected '" << identifierTypePair->first << "', but found '" << expression->getReturnType() << "'.");
}
template<typename MapType>
diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp
index 1d9e59119..d696ef22d 100644
--- a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp
+++ b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp
@@ -1,6 +1,6 @@
#include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
#include "src/storage/expressions/BooleanLiteralExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
namespace storm {
@@ -20,7 +20,7 @@ namespace storm {
}
bool UnaryBooleanFunctionExpression::evaluateAsBool(Valuation const* valuation) const {
- LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
+ STORM_LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
bool operandEvaluated = this->getOperand()->evaluateAsBool(valuation);
switch (this->getOperatorType()) {
diff --git a/src/storage/expressions/UnaryExpression.cpp b/src/storage/expressions/UnaryExpression.cpp
index 169466003..3569e5453 100644
--- a/src/storage/expressions/UnaryExpression.cpp
+++ b/src/storage/expressions/UnaryExpression.cpp
@@ -1,6 +1,6 @@
#include "src/storage/expressions/UnaryExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidAccessException.h"
namespace storm {
@@ -34,7 +34,7 @@ namespace storm {
}
std::shared_ptr<BaseExpression const> UnaryExpression::getOperand(uint_fast64_t operandIndex) const {
- LOG_THROW(operandIndex == 0, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 2.");
+ STORM_LOG_THROW(operandIndex == 0, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 2.");
return this->getOperand();
}
}
diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
index 972f2a24a..d90e460a1 100644
--- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
+++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
@@ -1,7 +1,7 @@
#include <cmath>
#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
namespace storm {
@@ -23,7 +23,7 @@ namespace storm {
}
int_fast64_t UnaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const {
- LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
+ STORM_LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
int_fast64_t operandEvaluated = this->getOperand()->evaluateAsInt(valuation);
switch (this->getOperatorType()) {
@@ -34,7 +34,7 @@ namespace storm {
}
double UnaryNumericalFunctionExpression::evaluateAsDouble(Valuation const* valuation) const {
- LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
+ STORM_LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
double operandEvaluated = this->getOperand()->evaluateAsDouble(valuation);
switch (this->getOperatorType()) {
diff --git a/src/storage/expressions/VariableExpression.cpp b/src/storage/expressions/VariableExpression.cpp
index a9f714569..c65e9a47a 100644
--- a/src/storage/expressions/VariableExpression.cpp
+++ b/src/storage/expressions/VariableExpression.cpp
@@ -1,5 +1,5 @@
#include "src/storage/expressions/VariableExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
namespace storm {
@@ -13,29 +13,29 @@ namespace storm {
}
bool VariableExpression::evaluateAsBool(Valuation const* valuation) const {
- LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
- LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as boolean: return type is not a boolean.");
+ STORM_LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
+ STORM_LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as boolean: return type is not a boolean.");
return valuation->getBooleanValue(this->getVariableName());
}
int_fast64_t VariableExpression::evaluateAsInt(Valuation const* valuation) const {
- LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
- LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as integer: return type is not an integer.");
+ STORM_LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
+ STORM_LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as integer: return type is not an integer.");
return valuation->getIntegerValue(this->getVariableName());
}
double VariableExpression::evaluateAsDouble(Valuation const* valuation) const {
- LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
- LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as double: return type is not a double.");
+ STORM_LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
+ STORM_LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as double: return type is not a double.");
switch (this->getReturnType()) {
case ExpressionReturnType::Int: return static_cast<double>(valuation->getIntegerValue(this->getVariableName())); break;
case ExpressionReturnType::Double: valuation->getDoubleValue(this->getVariableName()); break;
default: break;
}
- LOG_ASSERT(false, "Type of variable is required to be numeric.");
+ STORM_LOG_ASSERT(false, "Type of variable is required to be numeric.");
// Silence warning. This point can never be reached.
return 0;
diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp
index c02deea99..d327461a7 100644
--- a/src/storage/prism/Constant.cpp
+++ b/src/storage/prism/Constant.cpp
@@ -1,5 +1,5 @@
#include "src/storage/prism/Constant.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/IllegalFunctionCallException.h"
namespace storm {
@@ -25,7 +25,7 @@ namespace storm {
}
storm::expressions::Expression const& Constant::getExpression() const {
- LOG_THROW(this->isDefined(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve defining expression for undefined constant.");
+ STORM_LOG_THROW(this->isDefined(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve defining expression for undefined constant.");
return this->expression;
}
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index 6f4becb0a..327ffbcc3 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -1,5 +1,5 @@
#include "src/storage/prism/Module.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/OutOfRangeException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidAccessException.h"
@@ -25,7 +25,7 @@ namespace storm {
storm::prism::BooleanVariable const& Module::getBooleanVariable(std::string const& variableName) const {
auto const& nameIndexPair = this->booleanVariableToIndexMap.find(variableName);
- LOG_THROW(nameIndexPair != this->booleanVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown boolean variable '" << variableName << "'.");
+ STORM_LOG_THROW(nameIndexPair != this->booleanVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown boolean variable '" << variableName << "'.");
return this->getBooleanVariables()[nameIndexPair->second];
}
@@ -35,7 +35,7 @@ namespace storm {
storm::prism::IntegerVariable const& Module::getIntegerVariable(std::string const& variableName) const {
auto const& nameIndexPair = this->integerVariableToIndexMap.find(variableName);
- LOG_THROW(nameIndexPair != this->integerVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown integer variable '" << variableName << "'.");
+ STORM_LOG_THROW(nameIndexPair != this->integerVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown integer variable '" << variableName << "'.");
return this->getIntegerVariables()[nameIndexPair->second];
}
@@ -81,12 +81,12 @@ namespace storm {
}
std::string const& Module::getBaseModule() const {
- LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve base module of module that was not created by renaming.");
+ STORM_LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve base module of module that was not created by renaming.");
return this->renamedFromModule;
}
std::map<std::string, std::string> const& Module::getRenaming() const {
- LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve renaming of module that was not created by renaming.");
+ STORM_LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve renaming of module that was not created by renaming.");
return this->renaming;
}
@@ -96,7 +96,7 @@ namespace storm {
return actionsCommandSetPair->second;
}
- LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist in module.");
+ STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist in module.");
}
void Module::createMappings() {
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 617a1c52b..f053c93e8 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -2,7 +2,7 @@
#include <algorithm>
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "exceptions/InvalidArgumentException.h"
#include "src/exceptions/OutOfRangeException.h"
#include "src/exceptions/WrongFormatException.h"
@@ -81,13 +81,13 @@ namespace storm {
BooleanVariable const& Program::getGlobalBooleanVariable(std::string const& variableName) const {
auto const& nameIndexPair = this->globalBooleanVariableToIndexMap.find(variableName);
- LOG_THROW(nameIndexPair != this->globalBooleanVariableToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown boolean variable '" << variableName << "'.");
+ STORM_LOG_THROW(nameIndexPair != this->globalBooleanVariableToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown boolean variable '" << variableName << "'.");
return this->getGlobalBooleanVariables()[nameIndexPair->second];
}
IntegerVariable const& Program::getGlobalIntegerVariable(std::string const& variableName) const {
auto const& nameIndexPair = this->globalIntegerVariableToIndexMap.find(variableName);
- LOG_THROW(nameIndexPair != this->globalIntegerVariableToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown integer variable '" << variableName << "'.");
+ STORM_LOG_THROW(nameIndexPair != this->globalIntegerVariableToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown integer variable '" << variableName << "'.");
return this->getGlobalIntegerVariables()[nameIndexPair->second];
}
@@ -117,7 +117,7 @@ namespace storm {
Module const& Program::getModule(std::string const& moduleName) const {
auto const& nameIndexPair = this->moduleToIndexMap.find(moduleName);
- LOG_THROW(nameIndexPair != this->moduleToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown module '" << moduleName << "'.");
+ STORM_LOG_THROW(nameIndexPair != this->moduleToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown module '" << moduleName << "'.");
return this->getModules()[nameIndexPair->second];
}
@@ -135,13 +135,13 @@ namespace storm {
std::set<uint_fast64_t> const& Program::getModuleIndicesByAction(std::string const& action) const {
auto const& actionModuleSetPair = this->actionsToModuleIndexMap.find(action);
- LOG_THROW(actionModuleSetPair != this->actionsToModuleIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist.");
+ STORM_LOG_THROW(actionModuleSetPair != this->actionsToModuleIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist.");
return actionModuleSetPair->second;
}
uint_fast64_t Program::getModuleIndexByVariable(std::string const& variableName) const {
auto const& variableNameToModuleIndexPair = this->variableToModuleIndexMap.find(variableName);
- LOG_THROW(variableNameToModuleIndexPair != this->variableToModuleIndexMap.end(), storm::exceptions::OutOfRangeException, "Variable '" << variableName << "' does not exist.");
+ STORM_LOG_THROW(variableNameToModuleIndexPair != this->variableToModuleIndexMap.end(), storm::exceptions::OutOfRangeException, "Variable '" << variableName << "' does not exist.");
return variableNameToModuleIndexPair->second;
}
@@ -155,7 +155,7 @@ namespace storm {
storm::prism::RewardModel const& Program::getRewardModel(std::string const& name) const {
auto const& nameIndexPair = this->rewardModelToIndexMap.find(name);
- LOG_THROW(nameIndexPair != this->rewardModelToIndexMap.end(), storm::exceptions::OutOfRangeException, "Reward model '" << name << "' does not exist.");
+ STORM_LOG_THROW(nameIndexPair != this->rewardModelToIndexMap.end(), storm::exceptions::OutOfRangeException, "Reward model '" << name << "' does not exist.");
return this->getRewardModels()[nameIndexPair->second];
}
@@ -238,7 +238,7 @@ namespace storm {
// defining expression
if (constant.isDefined()) {
// Make sure we are not trying to define an already defined constant.
- LOG_THROW(constantDefinitions.find(constant.getName()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'.");
+ STORM_LOG_THROW(constantDefinitions.find(constant.getName()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'.");
// Now replace the occurrences of undefined constants in its defining expression.
newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber());
@@ -253,7 +253,7 @@ namespace storm {
definedUndefinedConstants.insert(constant.getName());
// Make sure the type of the constant is correct.
- LOG_THROW(variableExpressionPair->second.getReturnType() == constant.getType(), storm::exceptions::InvalidArgumentException, "Illegal type of expression defining constant '" << constant.getName() << "'.");
+ STORM_LOG_THROW(variableExpressionPair->second.getReturnType() == constant.getType(), storm::exceptions::InvalidArgumentException, "Illegal type of expression defining constant '" << constant.getName() << "'.");
// Now create the defined constant.
newConstants.emplace_back(constant.getType(), constant.getName(), variableExpressionPair->second, constant.getFilename(), constant.getLineNumber());
@@ -264,7 +264,7 @@ namespace storm {
// As a sanity check, we make sure that the given mapping does not contain any definitions for identifiers
// that are not undefined constants.
for (auto const& constantExpressionPair : constantDefinitions) {
- LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidArgumentException, "Unable to define non-existant constant.");
+ STORM_LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidArgumentException, "Unable to define non-existant constant.");
}
return Program(this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels());
@@ -276,7 +276,7 @@ namespace storm {
std::vector<Constant> newConstants(this->getConstants());
for (uint_fast64_t constantIndex = 0; constantIndex < newConstants.size(); ++constantIndex) {
auto const& constant = newConstants[constantIndex];
- LOG_THROW(constant.isDefined(), storm::exceptions::InvalidArgumentException, "Cannot substitute constants in program that contains undefined constants.");
+ STORM_LOG_THROW(constant.isDefined(), storm::exceptions::InvalidArgumentException, "Cannot substitute constants in program that contains undefined constants.");
// Put the corresponding expression in the substitution.
constantSubstitution.emplace(constant.getName(), constant.getExpression());
@@ -339,19 +339,19 @@ namespace storm {
std::set<std::string> constantNames;
for (auto const& constant : this->getConstants()) {
// Check for duplicate identifiers.
- LOG_THROW(allIdentifiers.find(constant.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": duplicate identifier '" << constant.getName() << "'.");
+ STORM_LOG_THROW(allIdentifiers.find(constant.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": duplicate identifier '" << constant.getName() << "'.");
// Check defining expressions of defined constants.
if (constant.isDefined()) {
std::set<std::string> containedIdentifiers = constant.getExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers.");
// Now check that the constants appear with the right types.
try {
constant.getExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": " << e.what());
}
}
@@ -368,16 +368,16 @@ namespace storm {
std::set<std::string> variableNames;
for (auto const& variable : this->getGlobalBooleanVariables()) {
// Check for duplicate identifiers.
- LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+ STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
// Check the initial value of the variable.
std::set<std::string> containedIdentifiers = variable.getInitialValueExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
try {
variable.getInitialValueExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
}
// Register the type of the constant for later type checks.
@@ -390,35 +390,35 @@ namespace storm {
}
for (auto const& variable : this->getGlobalIntegerVariables()) {
// Check for duplicate identifiers.
- LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+ STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
// Check that bound expressions of the range.
std::set<std::string> containedIdentifiers = variable.getLowerBoundExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants.");
try {
variable.getLowerBoundExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
}
containedIdentifiers = variable.getLowerBoundExpression().getVariables();
isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants.");
try {
variable.getUpperBoundExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
}
// Check the initial value of the variable.
containedIdentifiers = variable.getInitialValueExpression().getVariables();
isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
try {
variable.getInitialValueExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
}
// Register the type of the constant for later type checks.
@@ -434,16 +434,16 @@ namespace storm {
for (auto const& module : this->getModules()) {
for (auto const& variable : module.getBooleanVariables()) {
// Check for duplicate identifiers.
- LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+ STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
// Check the initial value of the variable.
std::set<std::string> containedIdentifiers = variable.getInitialValueExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
try {
variable.getInitialValueExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
}
// Register the type of the constant for later type checks.
@@ -455,7 +455,7 @@ namespace storm {
}
for (auto const& variable : module.getIntegerVariables()) {
// Check for duplicate identifiers.
- LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+ STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
// Register the type of the constant for later type checks.
identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int);
@@ -463,30 +463,30 @@ namespace storm {
// Check that bound expressions of the range.
std::set<std::string> containedIdentifiers = variable.getLowerBoundExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants.");
try {
variable.getLowerBoundExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
}
containedIdentifiers = variable.getLowerBoundExpression().getVariables();
isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants.");
try {
variable.getUpperBoundExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
}
// Check the initial value of the variable.
containedIdentifiers = variable.getInitialValueExpression().getVariables();
isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
try {
variable.getInitialValueExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
}
// Record the new identifier for future checks.
@@ -513,23 +513,23 @@ namespace storm {
// Check the guard.
std::set<std::string> containedIdentifiers = command.getGuardExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard refers to unknown identifiers.");
try {
command.getGuardExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": " << e.what());
}
- LOG_THROW(command.getGuardExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'.");
+ STORM_LOG_THROW(command.getGuardExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'.");
// Check all updates.
for (auto const& update : command.getUpdates()) {
containedIdentifiers = update.getLikelihoodExpression().getVariables();
isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers.");
try {
update.getLikelihoodExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": " << e.what());
}
// Check all assignments.
@@ -537,22 +537,22 @@ namespace storm {
for (auto const& assignment : update.getAssignments()) {
if (legalIdentifiers.find(assignment.getVariableName()) == legalIdentifiers.end()) {
if (allIdentifiers.find(assignment.getVariableName()) != allIdentifiers.end()) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment illegally refers to variable '" << assignment.getVariableName() << "'.");
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment illegally refers to variable '" << assignment.getVariableName() << "'.");
} else {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment refers to unknown variable '" << assignment.getVariableName() << "'.");
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment refers to unknown variable '" << assignment.getVariableName() << "'.");
}
}
- LOG_THROW(alreadyAssignedIdentifiers.find(assignment.getVariableName()) == alreadyAssignedIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'.");
+ STORM_LOG_THROW(alreadyAssignedIdentifiers.find(assignment.getVariableName()) == alreadyAssignedIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'.");
auto variableTypePair = identifierToTypeMap.find(assignment.getVariableName());
- LOG_THROW(variableTypePair->second == assignment.getExpression().getReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getReturnType() << "' to variable '" << variableTypePair->first << "' of type '" << variableTypePair->second << "'.");
+ STORM_LOG_THROW(variableTypePair->second == assignment.getExpression().getReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getReturnType() << "' to variable '" << variableTypePair->first << "' of type '" << variableTypePair->second << "'.");
containedIdentifiers = assignment.getExpression().getVariables();
isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers.");
try {
assignment.getExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": " << e.what());
}
// Add the current variable to the set of assigned variables (of this update).
@@ -567,87 +567,87 @@ namespace storm {
for (auto const& stateReward : rewardModel.getStateRewards()) {
std::set<std::string> containedIdentifiers = stateReward.getStatePredicateExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
try {
stateReward.getStatePredicateExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": " << e.what());
}
- LOG_THROW(stateReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
+ STORM_LOG_THROW(stateReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
containedIdentifiers = stateReward.getRewardValueExpression().getVariables();
isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
try {
stateReward.getRewardValueExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": " << e.what());
}
- LOG_THROW(stateReward.getRewardValueExpression().hasNumericalReturnType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": reward value expression must evaluate to numerical type.");
+ STORM_LOG_THROW(stateReward.getRewardValueExpression().hasNumericalReturnType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": reward value expression must evaluate to numerical type.");
}
for (auto const& transitionReward : rewardModel.getTransitionRewards()) {
std::set<std::string> containedIdentifiers = transitionReward.getStatePredicateExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
try {
transitionReward.getStatePredicateExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": " << e.what());
}
- LOG_THROW(transitionReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
+ STORM_LOG_THROW(transitionReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
containedIdentifiers = transitionReward.getRewardValueExpression().getVariables();
isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
try {
transitionReward.getRewardValueExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": " << e.what());
}
- LOG_THROW(transitionReward.getRewardValueExpression().hasNumericalReturnType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": reward value expression must evaluate to numerical type.");
+ STORM_LOG_THROW(transitionReward.getRewardValueExpression().hasNumericalReturnType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": reward value expression must evaluate to numerical type.");
}
}
// Check the initial states expression.
std::set<std::string> containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": initial expression refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": initial expression refers to unknown identifiers.");
try {
this->getInitialConstruct().getInitialStatesExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": " << e.what());
}
// Check the labels.
for (auto const& label : this->getLabels()) {
// Check for duplicate identifiers.
- LOG_THROW(allIdentifiers.find(label.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": duplicate identifier '" << label.getName() << "'.");
+ STORM_LOG_THROW(allIdentifiers.find(label.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": duplicate identifier '" << label.getName() << "'.");
std::set<std::string> containedIdentifiers = label.getStatePredicateExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label expression refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label expression refers to unknown identifiers.");
try {
label.getStatePredicateExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": " << e.what());
}
- LOG_THROW(label.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label predicate must evaluate to type 'bool'.");
+ STORM_LOG_THROW(label.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label predicate must evaluate to type 'bool'.");
}
// Check the formulas.
for (auto const& formula : this->getFormulas()) {
// Check for duplicate identifiers.
- LOG_THROW(allIdentifiers.find(formula.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": duplicate identifier '" << formula.getName() << "'.");
+ STORM_LOG_THROW(allIdentifiers.find(formula.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": duplicate identifier '" << formula.getName() << "'.");
std::set<std::string> containedIdentifiers = formula.getExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
- LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers.");
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers.");
try {
formula.getExpression().check(identifierToTypeMap);
} catch (storm::exceptions::InvalidTypeException const& e) {
- LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": " << e.what());
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": " << e.what());
}
// Record the new identifier for future checks.
diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp
index 9082bc6f1..c2fb2ccf5 100644
--- a/src/storage/prism/Update.cpp
+++ b/src/storage/prism/Update.cpp
@@ -1,5 +1,5 @@
#include "Update.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/OutOfRangeException.h"
namespace storm {
@@ -22,7 +22,7 @@ namespace storm {
storm::prism::Assignment const& Update::getAssignment(std::string const& variableName) const {
auto const& variableIndexPair = this->variableToAssignmentIndexMap.find(variableName);
- LOG_THROW(variableIndexPair != this->variableToAssignmentIndexMap.end(), storm::exceptions::OutOfRangeException, "Variable '" << variableName << "' is not assigned in update.");
+ STORM_LOG_THROW(variableIndexPair != this->variableToAssignmentIndexMap.end(), storm::exceptions::OutOfRangeException, "Variable '" << variableName << "' is not assigned in update.");
return this->getAssignments()[variableIndexPair->second];
}
diff --git a/src/storm.cpp b/src/storm.cpp
index 502e28c93..6b84773b2 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -1,328 +1,29 @@
-
-/*
- * STORM - a C++ Rebuild of MRMC
- *
- * STORM (Stochastic Reward Model Checker) is a model checker for discrete-time and continuous-time Markov
- * reward models. It supports reward extensions of PCTL and CSL (PRCTL
- * and CSRL), and allows for the automated verification of properties
- * concerning long-run and instantaneous rewards as well as cumulative
- * rewards.
- *
- * Authors: Philipp Berger
- *
- * Description: Central part of the application containing the main() Method
- */
-
-#include "src/utility/Initialize.h"
-#include <fstream>
-#include <cstdio>
-#include <climits>
-#include <sstream>
-#include <vector>
-#include <chrono>
-#include <iostream>
-#include <iomanip>
-
-
-
-
+// Include generated headers.
#include "storm-config.h"
#include "storm-version.h"
-#include "src/models/Dtmc.h"
-#include "src/models/MarkovAutomaton.h"
-#include "src/storage/SparseMatrix.h"
-#include "src/storage/MaximalEndComponentDecomposition.h"
-#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
-#include "src/models/AtomicPropositionsLabeling.h"
-#include "src/modelchecker/prctl/CreatePrctlModelChecker.h"
-#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
-#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
-#include "src/modelchecker/reachability/SparseSccModelChecker.h"
-#include "src/solver/GmmxxLinearEquationSolver.h"
-#include "src/solver/NativeLinearEquationSolver.h"
-#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
-#include "src/solver/GurobiLpSolver.h"
-// #include "src/counterexamples/GenerateCounterexample.h"
-#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
-#include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
-#include "src/counterexamples/PathBasedSubsystemGenerator.h"
-#include "src/parser/AutoParser.h"
-#include "src/parser/MarkovAutomatonParser.h"
-#include "src/parser/PrctlParser.h"
-#include "src/utility/ErrorHandling.h"
-#include "src/properties/Prctl.h"
-#include "src/utility/vector.h"
-#include "src/utility/CLI.h"
-
-
-#include "src/parser/PrctlFileParser.h"
-#include "src/parser/LtlFileParser.h"
-
-#include "src/parser/PrismParser.h"
-#include "src/adapters/ExplicitModelAdapter.h"
-// #include "src/adapters/SymbolicModelAdapter.h"
-
-#include "src/exceptions/InvalidSettingsException.h"
-
-
+// Include other headers.
+#include "src/exceptions/BaseException.h"
+#include "src/utility/macros.h"
+#include "src/utility/cli.h"
/*!
- * Checks the PRCTL formulae provided on the command line on the given model checker.
- *
- * @param modelchecker The model checker that is to be invoked on all given formulae.
+ * Main entry point of the executable storm.
*/
-void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double> const& modelchecker) {
- storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
- if (settings.isPctlSet()) {
- std::string chosenPrctlFile = settings.getPctlPropertiesFilename();
- LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << ".");
- std::list<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile);
+int main(const int argc, const char** argv) {
+ try {
+ storm::utility::cli::setUp();
+ storm::utility::cli::printHeader(argc, argv);
+ storm::utility::cli::parseOptions(argc, argv);
- for (auto formula : formulaList) {
- std::chrono::high_resolution_clock::time_point startTime = std::chrono::high_resolution_clock::now();
- formula->check(modelchecker);
- std::chrono::high_resolution_clock::time_point endTime = std::chrono::high_resolution_clock::now();
- std::cout << "Checking the formula took " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
- }
- }
-}
-
-/*!
- * Main entry point.
- */
-int main(const int argc, const char* argv[]) {
- // Register a signal handler to catch signals and display a backtrace.
- installSignalHandler();
-
- // Print an information header.
- printHeader(argc, argv);
-
- // Initialize the logging engine and perform other initalizations.
- initializeLogger();
- setUp();
-
-// try {
- LOG4CPLUS_INFO(logger, "StoRM was invoked.");
-
- // Parse options.
- if (!parseOptions(argc, argv)) {
- // If parsing failed or the option to see the usage was set, program execution stops here.
- return 0;
- }
-
- storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
-
- // If requested by the user, we install a timeout signal to abort computation.
- if (settings.isTimeoutSet()) {
- stormSetAlarm(settings.getTimeoutInSeconds());
- }
-
- // Execution Time measurement, start
- std::chrono::high_resolution_clock::time_point executionStart = std::chrono::high_resolution_clock::now();
-
- // Now, the settings are received and the specified model is parsed. The actual actions taken depend on whether
- // the model was provided in explicit or symbolic format.
- if (settings.isExplicitSet()) {
- std::string const chosenTransitionSystemFile = settings.getTransitionFilename();
- std::string const chosenLabelingFile = settings.getLabelingFilename();
-
- std::string chosenStateRewardsFile = "";
- if (settings.isStateRewardsSet()) {
- chosenStateRewardsFile = settings.getStateRewardsFilename();
- }
- std::string chosenTransitionRewardsFile = "";
- if (settings.isTransitionRewardsSet()) {
- chosenTransitionRewardsFile = settings.getTransitionRewardsFilename();
- }
-
- std::shared_ptr<storm::models::AbstractModel<double>> model = storm::parser::AutoParser::parseModel(chosenTransitionSystemFile, chosenLabelingFile, chosenStateRewardsFile, chosenTransitionRewardsFile);
-
- // Model Parsing Time Measurement, End
- std::chrono::high_resolution_clock::time_point parsingEnd = std::chrono::high_resolution_clock::now();
- std::cout << "Parsing the given model took " << std::chrono::duration_cast<std::chrono::milliseconds>(parsingEnd - executionStart).count() << " milliseconds." << std::endl;
-
- if (settings.isExportDotSet()) {
- std::ofstream outputFileStream;
- outputFileStream.open(settings.getExportDotFilename(), std::ofstream::out);
- model->writeDotToStream(outputFileStream);
- outputFileStream.close();
- }
-
- // Should there be a counterexample generated in case the formula is not satisfied?
- if(settings.isCounterexampleSet()) {
- // Counterexample Time Measurement, Start
- std::chrono::high_resolution_clock::time_point counterexampleStart = std::chrono::high_resolution_clock::now();
-
- // generateCounterExample(model);
-
- // Counterexample Time Measurement, End
- std::chrono::high_resolution_clock::time_point counterexampleEnd = std::chrono::high_resolution_clock::now();
- std::cout << "Generating the counterexample took " << std::chrono::duration_cast<std::chrono::milliseconds>(counterexampleEnd - counterexampleStart).count() << " milliseconds." << std::endl;
- } else {
- // Depending on the model type, the appropriate model checking procedure is chosen.
- storm::modelchecker::prctl::AbstractModelChecker<double>* modelchecker = nullptr;
- model->printModelInformationToStream(std::cout);
-
- // Modelchecking Time Measurement, Start
- std::chrono::high_resolution_clock::time_point modelcheckingStart = std::chrono::high_resolution_clock::now();
-
- switch (model->getType()) {
- case storm::models::DTMC:
- LOG4CPLUS_INFO(logger, "Model is a DTMC.");
- modelchecker = createPrctlModelChecker(*model->as<storm::models::Dtmc<double>>());
- checkPrctlFormulae(*modelchecker);
- break;
- case storm::models::MDP:
- LOG4CPLUS_INFO(logger, "Model is an MDP.");
- modelchecker = createPrctlModelChecker(*model->as<storm::models::Mdp<double>>());
- checkPrctlFormulae(*modelchecker);
- break;
- case storm::models::CTMC:
- LOG4CPLUS_INFO(logger, "Model is a CTMC.");
- LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
- break;
- case storm::models::CTMDP:
- LOG4CPLUS_INFO(logger, "Model is a CTMDP.");
- LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
- break;
- case storm::models::MA: {
- LOG4CPLUS_INFO(logger, "Model is a Markov automaton.");
- storm::models::MarkovAutomaton<double> markovAutomaton = *model->as<storm::models::MarkovAutomaton<double>>();
- markovAutomaton.close();
- storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker<double> mc(markovAutomaton);
-// std::cout << mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")) << std::endl;
-// std::cout << mc.checkExpectedTime(false, markovAutomaton->getLabeledStates("goal")) << std::endl;
- std::cout << mc.checkLongRunAverage(true, markovAutomaton.getLabeledStates("goal")) << std::endl;
- std::cout << mc.checkLongRunAverage(false, markovAutomaton.getLabeledStates("goal")) << std::endl;
-// std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 0, 1) << std::endl;
-// std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 1, 2) << std::endl;
- break;
- }
- case storm::models::Unknown:
- default:
- LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");
- break;
- }
-
- if (modelchecker != nullptr) {
- delete modelchecker;
- }
-
- // Modelchecking Time Measurement, End
- std::chrono::high_resolution_clock::time_point modelcheckingEnd = std::chrono::high_resolution_clock::now();
- std::cout << "Running the ModelChecker took " << std::chrono::duration_cast<std::chrono::milliseconds>(modelcheckingEnd - modelcheckingStart).count() << " milliseconds." << std::endl;
- }
- } else if (settings.isSymbolicSet()) {
- // Program Translation Time Measurement, Start
- std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now();
-
- // First, we build the model using the given symbolic model description and constant definitions.
- std::string const& programFile = settings.getSymbolicModelFilename();
- std::string const& constants = settings.getConstantDefinitionString();
- storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
- std::shared_ptr<storm::models::AbstractModel<double>> model = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, constants);
- model->printModelInformationToStream(std::cout);
-
- // Program Translation Time Measurement, End
- std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
- std::cout << "Parsing and translating the Symbolic Input took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl;
-
- storm::modelchecker::reachability::SparseSccModelChecker<double> modelChecker;
- storm::storage::BitVector trueStates(model->getNumberOfStates(), true);
- storm::storage::BitVector targetStates = model->getLabeledStates("observe0Greater1");
-// storm::storage::BitVector targetStates = model->getLabeledStates("one");
-// storm::storage::BitVector targetStates = model->getLabeledStates("elected");
- double value = modelChecker.computeReachabilityProbability(*model->as<storm::models::Dtmc<double>>(), trueStates, targetStates);
- std::cout << "computed value " << value << std::endl;
-
- if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandGenerationSet()) {
- if (model->getType() != storm::models::MDP) {
- LOG4CPLUS_ERROR(logger, "Minimal command counterexample generation is only supported for models of type MDP.");
- throw storm::exceptions::InternalTypeErrorException() << "Minimal command counterexample generation is only supported for models of type MDP.";
- }
-
- std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
-
- // Determine whether we are required to use the MILP-version or the SAT-version.
- bool useMILP = storm::settings::counterexampleGeneratorSettings().isUseMilpBasedMinimalCommandSetGenerationSet();
-
- // MinCMD Time Measurement, Start
- std::chrono::high_resolution_clock::time_point minCmdStart = std::chrono::high_resolution_clock::now();
-
- // Now parse the property file and receive the list of parsed formulas.
- std::string const& propertyFile = storm::settings::generalSettings().getPctlPropertiesFilename();
- std::list<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(propertyFile);
-
- // Now generate the counterexamples for each formula.
- for (auto formulaPtr : formulaList) {
- if (useMILP) {
- storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(program, *mdp, formulaPtr->getChild());
- } else {
- // storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, constants, *mdp, formulaPtr->getChild());
- }
- }
-
- // MinCMD Time Measurement, End
- std::chrono::high_resolution_clock::time_point minCmdEnd = std::chrono::high_resolution_clock::now();
- std::cout << "Minimal command Counterexample generation took " << std::chrono::duration_cast<std::chrono::milliseconds>(minCmdEnd - minCmdStart).count() << " milliseconds." << std::endl;
- } else if (settings.isPctlSet()) {
-// // Depending on the model type, the appropriate model checking procedure is chosen.
-// storm::modelchecker::prctl::AbstractModelChecker<double>* modelchecker = nullptr;
-//
- // Modelchecking Time Measurement, Start
- std::chrono::high_resolution_clock::time_point modelcheckingStart = std::chrono::high_resolution_clock::now();
-//
-// switch (model->getType()) {
-// case storm::models::DTMC:
-// LOG4CPLUS_INFO(logger, "Model is a DTMC.");
-// modelchecker = createPrctlModelChecker(*model->as<storm::models::Dtmc<double>>());
-// checkPrctlFormulae(*modelchecker);
-// break;
-// case storm::models::MDP:
-// LOG4CPLUS_INFO(logger, "Model is an MDP.");
-// modelchecker = createPrctlModelChecker(*model->as<storm::models::Mdp<double>>());
-// checkPrctlFormulae(*modelchecker);
-// break;
-// case storm::models::CTMC:
-// LOG4CPLUS_INFO(logger, "Model is a CTMC.");
-// LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
-// break;
-// case storm::models::CTMDP:
-// LOG4CPLUS_INFO(logger, "Model is a CTMDP.");
-// LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
-// break;
-// case storm::models::MA:
-// LOG4CPLUS_INFO(logger, "Model is a Markov automaton.");
-// break;
-// case storm::models::Unknown:
-// default:
-// LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");
-// break;
-// }
-//
-// if (modelchecker != nullptr) {
-// delete modelchecker;
-// }
-
- // Modelchecking Time Measurement, End
- std::chrono::high_resolution_clock::time_point modelcheckingEnd = std::chrono::high_resolution_clock::now();
- std::cout << "Running the PRCTL ModelChecker took " << std::chrono::duration_cast<std::chrono::milliseconds>(modelcheckingEnd - modelcheckingStart).count() << " milliseconds." << std::endl;
- }
- }
-
- // Execution Time Measurement, End
- std::chrono::high_resolution_clock::time_point executionEnd = std::chrono::high_resolution_clock::now();
- std::cout << "Complete execution took " << std::chrono::duration_cast<std::chrono::milliseconds>(executionEnd - executionStart).count() << " milliseconds." << std::endl;
+ // From this point on we are ready to carry out the actual computations.
+ storm::utility::cli::processOptions();
- // Perform clean-up and terminate.
- cleanUp();
- printUsage();
- LOG4CPLUS_INFO(logger, "StoRM terminating.");
- return 0;
-// } catch (std::exception& e) {
-// LOG4CPLUS_FATAL(logger, "An exception was thrown. Terminating.");
-// LOG4CPLUS_FATAL(logger, "\t" << e.what());
-// }
- return 1;
+ // All operations have now been performed, so we clean up everything and terminate.
+ storm::utility::cli::cleanUp();
+ } catch (storm::exceptions::BaseException const& exception) {
+ STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is " << exception.what());
+ } catch (std::exception const& exception) {
+ STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM to terminate. The message of this exception is: " << exception.what());
+ }
}
diff --git a/src/utility/CLI.h b/src/utility/CLI.h
deleted file mode 100644
index a94caa94a..000000000
--- a/src/utility/CLI.h
+++ /dev/null
@@ -1,166 +0,0 @@
-#ifndef STORM_UTILITY_CLI_H_
-#define STORM_UTILITY_CLI_H_
-
-#include <iostream>
-#include <fstream>
-#include <cstdio>
-#include <sstream>
-
-
-#include "src/utility/OsDetection.h"
-
-// Includes for the linked libraries and versions header
-#ifdef STORM_HAVE_INTELTBB
-# include "tbb/tbb_stddef.h"
-#endif
-#ifdef STORM_HAVE_GLPK
-# include "glpk.h"
-#endif
-#ifdef STORM_HAVE_GUROBI
-# include "gurobi_c.h"
-#endif
-#ifdef STORM_HAVE_Z3
-# include "z3.h"
-#endif
-
-/*!
-* Gives the current working directory
-*
-* @return std::string The path of the current working directory
-*/
-std::string getCurrentWorkingDirectory() {
- char temp[512];
- return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string(""));
-}
-
-
-void printUsage() {
-#ifndef WINDOWS
- struct rusage ru;
- getrusage(RUSAGE_SELF, &ru);
-
- std::cout << "===== Statistics ==============================" << std::endl;
- std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl;
- std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl;
- std::cout << "===============================================" << std::endl;
-#else
- HANDLE hProcess = GetCurrentProcess ();
- FILETIME ftCreation, ftExit, ftUser, ftKernel;
- PROCESS_MEMORY_COUNTERS pmc;
- if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
- std::cout << "Memory Usage: " << std::endl;
- std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl;
- std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl;
- std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl;
- std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl;
- std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl;
- std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl;
- std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl;
- std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl;
- std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl;
- }
-
- GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser);
-
- ULARGE_INTEGER uLargeInteger;
- uLargeInteger.LowPart = ftKernel.dwLowDateTime;
- uLargeInteger.HighPart = ftKernel.dwHighDateTime;
- double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
- uLargeInteger.LowPart = ftUser.dwLowDateTime;
- uLargeInteger.HighPart = ftUser.dwHighDateTime;
- double userTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0;
-
- std::cout << "CPU Time: " << std::endl;
- std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl;
- std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl;
-#endif
-}
-
-
-
-/*!
- * Prints the header.
- */
-void printHeader(const int argc, const char* argv[]) {
- std::cout << "StoRM" << std::endl;
- std::cout << "-----" << std::endl << std::endl;
-
- std::cout << "Version: " << STORM_CPP_VERSION_MAJOR << "." << STORM_CPP_VERSION_MINOR << "." << STORM_CPP_VERSION_PATCH;
- if (STORM_CPP_VERSION_COMMITS_AHEAD != 0) {
- std::cout << " (+" << STORM_CPP_VERSION_COMMITS_AHEAD << " commits)";
- }
- std::cout << " build from revision " << STORM_CPP_VERSION_HASH;
- if (STORM_CPP_VERSION_DIRTY == 1) {
- std::cout << " (DIRTY)";
- }
- std::cout << "." << std::endl;
-
-#ifdef STORM_HAVE_INTELTBB
- std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
-#endif
-#ifdef STORM_HAVE_GLPK
- std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl;
-#endif
-#ifdef STORM_HAVE_GUROBI
- std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl;
-#endif
-#ifdef STORM_HAVE_Z3
- unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
- Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
- std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl;
-#endif
-
- // "Compute" the command line argument string with which STORM was invoked.
- std::stringstream commandStream;
- for (int i = 0; i < argc; ++i) {
- commandStream << argv[i] << " ";
- }
- std::cout << "Command line: " << commandStream.str() << std::endl << std::endl;
- std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
-}
-
-/*!
- * Parses the given command line arguments.
- *
- * @param argc The argc argument of main().
- * @param argv The argv argument of main().
- * @return True iff the program should continue to run after parsing the options.
- */
-bool parseOptions(const int argc, const char* argv[]) {
- storm::settings::SettingsManager& manager = storm::settings::mutableManager();
- try {
- manager.setFromCommandLine(argc, argv);
- } catch (storm::exceptions::OptionParserException& e) {
- std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
- std::cout << std::endl;
- manager.printHelp();
- return false;
- }
-
- if (storm::settings::generalSettings().isHelpSet()) {
- storm::settings::manager().printHelp(storm::settings::generalSettings().getHelpModuleName());
- return false;
- }
-
- if (storm::settings::generalSettings().isVerboseSet()) {
- logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
- LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console.");
- }
- if (storm::settings::debugSettings().isDebugSet()) {
- logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL);
- logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL);
- LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console.");
- }
- if (storm::settings::debugSettings().isTraceSet()) {
- logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL);
- logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL);
- LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console.");
- }
- if (storm::settings::debugSettings().isLogfileSet()) {
- setUpFileLogging();
- }
- return true;
-}
-
-
-#endif
\ No newline at end of file
diff --git a/src/utility/Initialize.h b/src/utility/Initialize.h
deleted file mode 100644
index cf2facda5..000000000
--- a/src/utility/Initialize.h
+++ /dev/null
@@ -1,22 +0,0 @@
-#ifndef STORM_UTILITY_INITIALIZE_H_
-#define STORM_UTILITY_INITIALIZE_H_
-
-#include "InitializeLogging.h"
-
-/*!
- * Performs some necessary initializations.
- */
-void setUp() {
- // Increase the precision of output.
- std::cout.precision(10);
-}
-
-/*!
- * Performs some necessary clean-up.
- */
-void cleanUp() {
- // Intentionally left empty.
-}
-
-
-#endif
\ No newline at end of file
diff --git a/src/utility/InitializeLogging.h b/src/utility/InitializeLogging.h
deleted file mode 100644
index ea8394705..000000000
--- a/src/utility/InitializeLogging.h
+++ /dev/null
@@ -1,37 +0,0 @@
-#ifndef STORM_UTILITY_INITIALIZELOGGING_H_
-#define STORM_UTILITY_INITIALIZELOGGING_H_
-
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-#include "log4cplus/consoleappender.h"
-#include "log4cplus/fileappender.h"
-
-#include "src/settings/SettingsManager.h"
-
-log4cplus::Logger logger;
-
-/*!
- * Initializes the logging framework and sets up logging to console.
- */
-void initializeLogger() {
- logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main"));
- logger.setLogLevel(log4cplus::INFO_LOG_LEVEL);
- log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender());
- consoleLogAppender->setName("mainConsoleAppender");
- consoleLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL);
- consoleLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n")));
- logger.addAppender(consoleLogAppender);
-}
-
-/*!
- * Sets up the logging to file.
- */
-void setUpFileLogging() {
- log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(storm::settings::debugSettings().getLogfilename()));
- fileLogAppender->setName("mainFileAppender");
- fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n")));
- logger.addAppender(fileLogAppender);
-}
-
-
-#endif
\ No newline at end of file
diff --git a/src/utility/PrismUtility.h b/src/utility/PrismUtility.h
index de8bcb2c7..5dda96313 100644
--- a/src/utility/PrismUtility.h
+++ b/src/utility/PrismUtility.h
@@ -3,7 +3,7 @@
#include "src/storage/LabeledValues.h"
#include "src/storage/prism/Program.h"
-#include "src/exceptions/ExceptionMacros.h"
+#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
@@ -217,8 +217,8 @@ namespace storm {
if (program.hasConstant(constantName)) {
// Get the actual constant and check whether it's in fact undefined.
auto const& constant = program.getConstant(constantName);
- LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'.");
- LOG_THROW(definedConstants.find(constantName) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
+ STORM_LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'.");
+ STORM_LOG_THROW(definedConstants.find(constantName) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
definedConstants.insert(constantName);
if (constant.getType() == storm::expressions::ExpressionReturnType::Bool) {
diff --git a/src/utility/cli.h b/src/utility/cli.h
new file mode 100644
index 000000000..f097a6a7c
--- /dev/null
+++ b/src/utility/cli.h
@@ -0,0 +1,222 @@
+#ifndef STORM_UTILITY_CLI_H_
+#define STORM_UTILITY_CLI_H_
+
+#include <iostream>
+#include <iomanip>
+#include <fstream>
+#include <cstdio>
+#include <sstream>
+
+#include "src/utility/OsDetection.h"
+#include "src/settings/SettingsManager.h"
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+#include "log4cplus/consoleappender.h"
+#include "log4cplus/fileappender.h"
+log4cplus::Logger logger;
+
+// Includes for the linked libraries and versions header
+#ifdef STORM_HAVE_INTELTBB
+# include "tbb/tbb_stddef.h"
+#endif
+#ifdef STORM_HAVE_GLPK
+# include "glpk.h"
+#endif
+#ifdef STORM_HAVE_GUROBI
+# include "gurobi_c.h"
+#endif
+#ifdef STORM_HAVE_Z3
+# include "z3.h"
+#endif
+
+namespace storm {
+ namespace utility {
+ namespace cli {
+
+ /*!
+ * Initializes the logging framework and sets up logging to console.
+ */
+ void initializeLogger() {
+ logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main"));
+ logger.setLogLevel(log4cplus::INFO_LOG_LEVEL);
+ log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender());
+ consoleLogAppender->setName("mainConsoleAppender");
+ consoleLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL);
+ consoleLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n")));
+ logger.addAppender(consoleLogAppender);
+ }
+
+ /*!
+ * Performs some necessary initializations.
+ */
+ void setUp() {
+ initializeLogger();
+ std::cout.precision(10);
+ }
+
+ /*!
+ * Performs some necessary clean-up.
+ */
+ void cleanUp() {
+ // Intentionally left empty.
+ }
+
+ /*!
+ * Sets up the logging to file.
+ */
+ void setUpFileLogging() {
+ log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(storm::settings::debugSettings().getLogfilename()));
+ fileLogAppender->setName("mainFileAppender");
+ fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n")));
+ logger.addAppender(fileLogAppender);
+ }
+
+ /*!
+ * Gives the current working directory
+ *
+ * @return std::string The path of the current working directory
+ */
+ std::string getCurrentWorkingDirectory() {
+ char temp[512];
+ return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string(""));
+ }
+
+
+ void printUsage() {
+#ifndef WINDOWS
+ struct rusage ru;
+ getrusage(RUSAGE_SELF, &ru);
+
+ std::cout << "===== Statistics ==============================" << std::endl;
+ std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl;
+ std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl;
+ std::cout << "===============================================" << std::endl;
+#else
+ HANDLE hProcess = GetCurrentProcess ();
+ FILETIME ftCreation, ftExit, ftUser, ftKernel;
+ PROCESS_MEMORY_COUNTERS pmc;
+ if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
+ std::cout << "Memory Usage: " << std::endl;
+ std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl;
+ std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl;
+ std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl;
+ std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl;
+ std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl;
+ std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl;
+ std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl;
+ std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl;
+ std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl;
+ }
+
+ GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser);
+
+ ULARGE_INTEGER uLargeInteger;
+ uLargeInteger.LowPart = ftKernel.dwLowDateTime;
+ uLargeInteger.HighPart = ftKernel.dwHighDateTime;
+ double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
+ uLargeInteger.LowPart = ftUser.dwLowDateTime;
+ uLargeInteger.HighPart = ftUser.dwHighDateTime;
+ double userTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0;
+
+ std::cout << "CPU Time: " << std::endl;
+ std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl;
+ std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl;
+#endif
+ }
+
+
+
+ /*!
+ * Prints the header.
+ */
+ void printHeader(const int argc, const char* argv[]) {
+ std::cout << "StoRM" << std::endl;
+ std::cout << "-----" << std::endl << std::endl;
+
+ std::cout << "Version: " << STORM_CPP_VERSION_MAJOR << "." << STORM_CPP_VERSION_MINOR << "." << STORM_CPP_VERSION_PATCH;
+ if (STORM_CPP_VERSION_COMMITS_AHEAD != 0) {
+ std::cout << " (+" << STORM_CPP_VERSION_COMMITS_AHEAD << " commits)";
+ }
+ std::cout << " build from revision " << STORM_CPP_VERSION_HASH;
+ if (STORM_CPP_VERSION_DIRTY == 1) {
+ std::cout << " (DIRTY)";
+ }
+ std::cout << "." << std::endl;
+
+#ifdef STORM_HAVE_INTELTBB
+ std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
+#endif
+#ifdef STORM_HAVE_GLPK
+ std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl;
+#endif
+#ifdef STORM_HAVE_GUROBI
+ std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl;
+#endif
+#ifdef STORM_HAVE_Z3
+ unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
+ Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
+ std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl;
+#endif
+
+ // "Compute" the command line argument string with which STORM was invoked.
+ std::stringstream commandStream;
+ for (int i = 0; i < argc; ++i) {
+ commandStream << argv[i] << " ";
+ }
+ std::cout << "Command line: " << commandStream.str() << std::endl;
+ std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
+ }
+
+ /*!
+ * Parses the given command line arguments.
+ *
+ * @param argc The argc argument of main().
+ * @param argv The argv argument of main().
+ * @return True iff the program should continue to run after parsing the options.
+ */
+ bool parseOptions(const int argc, const char* argv[]) {
+ storm::settings::SettingsManager& manager = storm::settings::mutableManager();
+ try {
+ manager.setFromCommandLine(argc, argv);
+ } catch (storm::exceptions::OptionParserException& e) {
+ std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
+ std::cout << std::endl;
+ manager.printHelp();
+ return false;
+ }
+
+ if (storm::settings::generalSettings().isHelpSet()) {
+ storm::settings::manager().printHelp(storm::settings::generalSettings().getHelpModuleName());
+ return false;
+ }
+
+ if (storm::settings::generalSettings().isVerboseSet()) {
+ logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
+ LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console.");
+ }
+ if (storm::settings::debugSettings().isDebugSet()) {
+ logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL);
+ logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL);
+ LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console.");
+ }
+ if (storm::settings::debugSettings().isTraceSet()) {
+ logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL);
+ logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL);
+ LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console.");
+ }
+ if (storm::settings::debugSettings().isLogfileSet()) {
+ setUpFileLogging();
+ }
+ return true;
+ }
+
+ void processOptions() {
+
+ }
+
+ }
+ }
+}
+
+#endif
\ No newline at end of file
diff --git a/src/utility/macros.h b/src/utility/macros.h
new file mode 100644
index 000000000..511fdcc12
--- /dev/null
+++ b/src/utility/macros.h
@@ -0,0 +1,57 @@
+#ifndef STORM_UTILITY_MACROS_H_
+#define STORM_UTILITY_MACROS_H_
+
+#include <cassert>
+
+// Include the parts necessary for Log4cplus.
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+extern log4cplus::Logger logger;
+
+/*!
+ * Define the macros STORM_LOG_ASSERT and STORM_LOG_DEBUG to be silent in non-debug mode and log the message in case the condition
+ * fails to evaluate to true.
+ */
+#ifndef NDEBUG
+#define STORM_LOG_ASSERT(cond, message) \
+{ \
+ if (!(cond)) { \
+ LOG4CPLUS_ERROR(logger, message); \
+ assert(cond); \
+ } \
+} while (false)
+#define STORM_LOG_DEBUG(message) \
+{ \
+ LOG4CPLUS_DEBUG(logger, message); \
+} while (false)
+#else
+#define STORM_LOG_ASSERT(cond, message) /* empty */
+#define STORM_LOG_DEBUG(message) /* empty */
+#endif
+
+// Define STORM_LOG_THROW to always throw the exception with the given message if the condition fails to hold.
+#define STORM_LOG_THROW(cond, exception, message) \
+{ \
+ if (!(cond)) { \
+ LOG4CPLUS_ERROR(logger, message); \
+ throw exception() << message; \
+ } \
+} while (false)
+
+// Define STORM_LOG_WARN, STORM_LOG_ERROR and STORM_LOG_INFO to log the given message with the corresponding log levels.
+#define STORM_LOG_WARN(message) \
+{ \
+ LOG4CPLUS_WARN(logger, message); \
+} while (false)
+
+#define STORM_LOG_INFO(message) \
+{ \
+ LOG4CPLUS_INFO(logger, message); \
+} while (false)
+
+#define STORM_LOG_ERROR(message) \
+{ \
+ LOG4CPLUS_ERROR(logger, message); \
+} while (false)
+
+#endif /* STORM_UTILITY_MACROS_H_ */
\ No newline at end of file