From adfe82d0d678fe7b36b69c5701fa6dba31b8099f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 4 Jul 2019 10:18:12 +0200 Subject: [PATCH 1/4] Fixed typo to void --- src/storm/builder/DdJaniModelBuilder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; } From 685b5c6b27499f4a21413d9022fc660ad2902337 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 4 Jul 2019 11:19:24 +0200 Subject: [PATCH 2/4] Throw exceptions after switch/case to silence compiler warnings about not returning anything --- src/storm-pomdp/storage/PomdpMemory.cpp | 4 +++- src/storm/logic/Bound.h | 4 +++- src/storm/logic/ComparisonType.h | 5 +++++ src/storm/modelchecker/results/FilterType.cpp | 3 +++ src/storm/solver/LinearEquationSolverRequirements.cpp | 4 ++++ .../solver/MinMaxLinearEquationSolverRequirements.cpp | 4 ++++ src/storm/solver/Multiplier.cpp | 2 ++ src/storm/storage/dd/bisimulation/SignatureComputer.cpp | 2 ++ src/storm/storage/jani/JSONExporter.cpp | 8 +++----- src/storm/utility/builder.cpp | 5 ++++- 10 files changed, 33 insertions(+), 8 deletions(-) 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/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..b0b315e8a 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) { @@ -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 +} From 7fb660227f4906be2cd304b50c47fb5d7855aa61 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 4 Jul 2019 11:20:04 +0200 Subject: [PATCH 3/4] Replaced assert(false) by throwing an exception --- src/storm-gspn/adapters/XercesAdapter.h | 15 ++++++--------- .../builder/JaniProgramGraphBuilder.cpp | 7 +++---- src/storm/analysis/GraphConditions.cpp | 7 ++++--- src/storm/storage/jani/JSONExporter.cpp | 2 +- src/storm/utility/shortestPaths.cpp | 4 ++-- 5 files changed, 16 insertions(+), 19 deletions(-) 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/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/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index b0b315e8a..2975f9ff3 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -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; } 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)); From 9c52d0d2ab1ad9b0326fbc4af3946e18e9b1892a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 9 Jul 2019 10:24:07 +0200 Subject: [PATCH 4/4] Workaround for IntelTBB linker issue by CMake/Regex magic. IntelTBB does not use symlinks (as commonly used) to reference its libraries but instead uses linker scripts. These linker scripts do not work with GCC and linking fails. As a workaround we manually set the correct library in CMake after extracting the path from the linker script with regex magic. This workaround is highly hackish and might break in the future. --- resources/3rdparty/CMakeLists.txt | 32 ++++++++++++++++++++++++++++--- 1 file changed, 29 insertions(+), 3 deletions(-) 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)