diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 5fc6d8275..4e46c4c3b 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -562,9 +562,35 @@ if (STORM_USE_INTELTBB) message(STATUS "Storm - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.") message(STATUS "Storm - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.") set(STORM_HAVE_INTELTBB ON) - link_directories(${TBB_LIBRARY_DIRS}) - include_directories(${TBB_INCLUDE_DIRS}) - list(APPEND STORM_LINK_LIBRARIES tbb tbbmalloc) + # Under Linux libtbb.so contains a linker script to libtbb.so.2 instead of a symlink. + # This breaks CMake. + # As a workaround we manually try to add the necessary suffix ".2" to the so file and hope for the best. + if (LINUX) + # Check if the library is a linker script which only links to the correct library + # Read first bytes of file + file(READ "${TBB_LIBRARY}" TMPTXT LIMIT 128) + # Check if file starts with "INPUT (libtbb.so.2)" + if("${TMPTXT}" MATCHES "INPUT \\(libtbb\\.so\\.(.*)\\)") + # Manually set library by adding the suffix from the linker script. + # CMAKE_MATCH_1 contains the parsed suffix. + set(TBB_LIB_LINUX "${TBB_LIBRARY}.${CMAKE_MATCH_1}") + set(TBB_MALLOC_LIB_LINUX "${TBB_MALLOC_LIBRARY}.${CMAKE_MATCH_1}") + if (EXISTS "${TBB_LIB_LINUX}") + set(TBB_LIBRARY ${TBB_LIB_LINUX}) + message(STATUS "Storm - Using Intel TBB library in manually set path ${TBB_LIBRARY}.") + endif() + if (EXISTS "${TBB_MALLOC_LIB_LINUX}") + set(TBB_MALLOC_LIBRARY ${TBB_MALLOC_LIB_LINUX}) + message(STATUS "Storm - Using Intel TBB malloc library in manually set path ${TBB_MALLOC_LIBRARY}.") + endif() + endif() + endif() + + add_imported_library(tbb SHARED ${TBB_LIBRARY} ${TBB_INCLUDE_DIRS}) + list(APPEND STORM_DEP_TARGETS tbb_SHARED) + add_imported_library(tbb_malloc SHARED ${TBB_MALLOC_LIBRARY} ${TBB_INCLUDE_DIRS}) + list(APPEND STORM_DEP_TARGETS tbb_malloc_SHARED) + else(TBB_FOUND) message(FATAL_ERROR "Storm - TBB was requested, but not found.") endif(TBB_FOUND) diff --git a/src/storm-gspn/adapters/XercesAdapter.h b/src/storm-gspn/adapters/XercesAdapter.h index 0a39c8f2e..c7f22846f 100644 --- a/src/storm-gspn/adapters/XercesAdapter.h +++ b/src/storm-gspn/adapters/XercesAdapter.h @@ -10,7 +10,8 @@ #include #include - +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace adapters { @@ -27,16 +28,12 @@ namespace storm { auto elementNode = (xercesc::DOMElement *) node; return XMLtoString(elementNode->getTagName()); } - case xercesc::DOMNode::NodeType::TEXT_NODE: { + case xercesc::DOMNode::NodeType::TEXT_NODE: return XMLtoString(node->getNodeValue()); - } - case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: { + case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: return XMLtoString(node->getNodeName()); - } - default: { - assert(false); - return ""; - } + default: + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown DOMNode type"); } } } diff --git a/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp b/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp index bcb569917..361a4ce25 100644 --- a/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp +++ b/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp @@ -1,6 +1,7 @@ #include "JaniProgramGraphBuilder.h" #include "storm/storage/jani/EdgeDestination.h" +#include "storm/exceptions/NotSupportedException.h" namespace storm { namespace builder { @@ -23,12 +24,10 @@ namespace storm { variables.emplace(v.first, janiVar); automaton.addVariable(*janiVar); } else { - // Not yet supported. - assert(false); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unbounded right bound is not supported yet"); } } else { - // Not yet supported. - assert(false); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unbounded left bound is not supported yet"); } } else { storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), isRewardVariable(v.first)); diff --git a/src/storm-pomdp/storage/PomdpMemory.cpp b/src/storm-pomdp/storage/PomdpMemory.cpp index 1c5f74cf4..161f89f8c 100644 --- a/src/storm-pomdp/storage/PomdpMemory.cpp +++ b/src/storm-pomdp/storage/PomdpMemory.cpp @@ -2,6 +2,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace storage { @@ -110,6 +111,7 @@ namespace storm { case PomdpMemoryPattern::Full: return buildFullyConnectedMemory(numStates); } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown PomdpMemoryPattern"); } PomdpMemory PomdpMemoryBuilder::buildTrivialMemory() const { @@ -177,4 +179,4 @@ namespace storm { return PomdpMemory(transitions, 0); } } -} \ No newline at end of file +} diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 2152adfe7..246f256be 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -4,6 +4,7 @@ #include "GraphConditions.h" #include "storm/utility/constants.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/UnexpectedException.h" #include "storm/models/sparse/StandardRewardModel.h" namespace storm { @@ -44,7 +45,7 @@ namespace storm { } else if (entry.denominator().constantPart() < 0) { wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { - assert(false); // Should fail before. + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before."); } } else { wellformedConstraintSet.emplace(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); @@ -111,7 +112,7 @@ namespace storm { } else if (transition.getValue().denominator().constantPart() < 0) { wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { - assert(false); // Should fail before. + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before."); } } else { wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); @@ -147,7 +148,7 @@ namespace storm { } else if (entry.getValue().denominator().constantPart() < 0) { wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { - assert(false); // Should fail before. + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before."); } } else { wellformedConstraintSet.emplace(entry.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 27e1e586e..a9b4f62b9 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -733,7 +733,7 @@ namespace storm { // Intentionally left empty. } - bool setMarkovian(bool markovian) { + void setMarkovian(bool markovian) { this->markovian = markovian; } diff --git a/src/storm/logic/Bound.h b/src/storm/logic/Bound.h index 0b152ea06..e429dbc6e 100644 --- a/src/storm/logic/Bound.h +++ b/src/storm/logic/Bound.h @@ -1,10 +1,11 @@ #ifndef STORM_LOGIC_BOUND_H_ #define STORM_LOGIC_BOUND_H_ +#include "storm/exceptions/IllegalArgumentException.h" #include "storm/logic/ComparisonType.h" #include "storm/storage/expressions/Expression.h" #include "storm/utility/constants.h" - +#include "storm/utility/macros.h" namespace storm { namespace logic { @@ -29,6 +30,7 @@ namespace storm { case ComparisonType::LessEqual: return compareValue <= thresholdAsValueType; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); } friend std::ostream& operator<<(std::ostream& out, Bound const& bound); diff --git a/src/storm/logic/ComparisonType.h b/src/storm/logic/ComparisonType.h index 19475960f..c47fb2786 100644 --- a/src/storm/logic/ComparisonType.h +++ b/src/storm/logic/ComparisonType.h @@ -3,6 +3,9 @@ #include +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" + namespace storm { namespace logic { enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual }; @@ -26,6 +29,7 @@ namespace storm { case ComparisonType::GreaterEqual: return ComparisonType::Less; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); } inline ComparisonType invertPreserveStrictness(ComparisonType t) { @@ -39,6 +43,7 @@ namespace storm { case ComparisonType::GreaterEqual: return ComparisonType::LessEqual; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); } std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); diff --git a/src/storm/modelchecker/results/FilterType.cpp b/src/storm/modelchecker/results/FilterType.cpp index 17a69063e..e7eac999b 100644 --- a/src/storm/modelchecker/results/FilterType.cpp +++ b/src/storm/modelchecker/results/FilterType.cpp @@ -1,5 +1,7 @@ #include "FilterType.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace modelchecker { @@ -27,6 +29,7 @@ namespace storm { case FilterType::VALUES: return "the values"; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType"); } } } diff --git a/src/storm/solver/LinearEquationSolverRequirements.cpp b/src/storm/solver/LinearEquationSolverRequirements.cpp index 445e776d7..e4075b1e1 100644 --- a/src/storm/solver/LinearEquationSolverRequirements.cpp +++ b/src/storm/solver/LinearEquationSolverRequirements.cpp @@ -1,5 +1,8 @@ #include "storm/solver/LinearEquationSolverRequirements.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" + namespace storm { namespace solver { @@ -36,6 +39,7 @@ namespace storm { case Element::LowerBounds: return lowerBounds(); break; case Element::UpperBounds: return upperBounds(); break; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ElementType"); } void LinearEquationSolverRequirements::clearLowerBounds() { diff --git a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp index 3e5e867ab..3d7cdc607 100644 --- a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp @@ -1,5 +1,8 @@ #include "storm/solver/MinMaxLinearEquationSolverRequirements.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" + namespace storm { namespace solver { @@ -56,6 +59,7 @@ namespace storm { case Element::LowerBounds: return lowerBounds(); break; case Element::UpperBounds: return upperBounds(); break; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ElementType"); } void MinMaxLinearEquationSolverRequirements::clearUniqueSolution() { diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 3347ef2dc..abcb53f3d 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -12,6 +12,7 @@ #include "storm/solver/NativeMultiplier.h" #include "storm/solver/GmmxxMultiplier.h" #include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace solver { @@ -79,6 +80,7 @@ namespace storm { case MultiplierType::Native: return std::make_unique>(matrix); } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown MultiplierType"); } template class Multiplier; diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp index 89345ee9d..407ed33b9 100644 --- a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp @@ -6,6 +6,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/OutOfRangeException.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace dd { @@ -23,6 +24,7 @@ namespace storm { case SignatureMode::Eager: return position < 1; case SignatureMode::Lazy: return position < 2; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown SignatureMode"); } template diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index be2c98e9f..2975f9ff3 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -12,6 +12,7 @@ #include "storm/exceptions/InvalidJaniException.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/IllegalArgumentException.h" #include "storm/storage/expressions/RationalLiteralExpression.h" #include "storm/storage/expressions/IntegerLiteralExpression.h" @@ -120,9 +121,8 @@ namespace storm { return ">"; case storm::logic::ComparisonType::GreaterEqual: return "≥"; - default: - assert(false); } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); } modernjson::json numberToJson(storm::RationalNumber rn) { @@ -796,7 +796,7 @@ namespace storm { typeDescr["kind"] = "array"; typeDescr["base"] = buildTypeDescription(type.getElementType()); } else { - assert(false); + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown expression type."); } return typeDescr; } @@ -1104,10 +1104,8 @@ namespace storm { return "argmax"; case storm::modelchecker::FilterType::VALUES: return "values"; - default: - assert(false); - } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType"); } modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) { diff --git a/src/storm/utility/builder.cpp b/src/storm/utility/builder.cpp index a6b85e9b1..481ed8020 100644 --- a/src/storm/utility/builder.cpp +++ b/src/storm/utility/builder.cpp @@ -7,6 +7,8 @@ #include "storm/models/sparse/Pomdp.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/exceptions/InvalidModelException.h" + namespace storm { namespace utility { namespace builder { @@ -27,6 +29,7 @@ namespace storm { case storm::models::ModelType::S2pg: return std::make_shared>(std::move(components)); } + STORM_LOG_THROW(false, storm::exceptions::InvalidModelException, "Unknown model type"); } template std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); @@ -35,4 +38,4 @@ namespace storm { template std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); } } -} \ No newline at end of file +} diff --git a/src/storm/utility/shortestPaths.cpp b/src/storm/utility/shortestPaths.cpp index b18e309d4..dccfa43f4 100644 --- a/src/storm/utility/shortestPaths.cpp +++ b/src/storm/utility/shortestPaths.cpp @@ -9,6 +9,7 @@ #include "storm/utility/graph.h" #include "storm/utility/macros.h" #include "storm/utility/shortestPaths.h" +#include "storm/exceptions/UnexpectedException.h" // FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required! // (Also, did I document this? I think so, somewhere. I went with k>=1 because @@ -247,8 +248,7 @@ namespace storm { // there is no such edge // let's disallow that for now, because I'm not expecting it to happen - assert(false); - return zero(); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should not happen."); } else { // edge must be "virtual edge" to meta-target assert(isMetaTargetPredecessor(tailNode));