From 62757e28f735df9c28a2caf82f9c176e18af7686 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 9 Jul 2020 22:00:26 -0700 Subject: [PATCH 01/12] parametric pomdps? --- src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp | 1 + src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp | 1 + src/storm-pomdp/transformer/MakePOMDPCanonic.cpp | 1 + src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp | 1 + 4 files changed, 4 insertions(+) diff --git a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp index b0f1837cb..7d290a6da 100644 --- a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp +++ b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp @@ -133,5 +133,6 @@ namespace storm { template class ApplyFiniteSchedulerToPomdp; + template class ApplyFiniteSchedulerToPomdp; } } \ No newline at end of file diff --git a/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp b/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp index 385e415f1..358ad3041 100644 --- a/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp +++ b/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp @@ -173,5 +173,6 @@ namespace storm { template class BinaryPomdpTransformer; + template class BinaryPomdpTransformer; } } \ No newline at end of file diff --git a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp index 3cd17c25d..28f0d8c30 100644 --- a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp +++ b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp @@ -289,5 +289,6 @@ namespace storm { template class MakePOMDPCanonic; template class MakePOMDPCanonic; + template class MakePOMDPCanonic; } } \ No newline at end of file diff --git a/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp b/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp index 1f7235108..086a1e389 100644 --- a/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp +++ b/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp @@ -187,6 +187,7 @@ namespace storm { } template class PomdpMemoryUnfolder; + template class PomdpMemoryUnfolder; template class PomdpMemoryUnfolder; From d76bcc4d103294591baeb3acae60661e65a0b3a9 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 9 Jul 2020 23:00:10 -0700 Subject: [PATCH 02/12] pPOMDP support --- .../ApplyFiniteSchedulerToPomdp.cpp | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp index 7d290a6da..a125289bf 100644 --- a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp +++ b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp @@ -19,7 +19,7 @@ namespace storm { } struct RationalFunctionConstructor { - RationalFunctionConstructor() : cache(std::make_shared()) { + RationalFunctionConstructor(std::shared_ptr const& cache) : cache(cache) { } @@ -31,11 +31,25 @@ namespace storm { std::shared_ptr cache; }; + template + std::shared_ptr getCache(storm::models::sparse::Pomdp const& model) { + return std::make_shared(); + } + + template<> + std::shared_ptr getCache(storm::models::sparse::Pomdp const& model) { + for (auto const& entry : model.getTransitionMatrix()) { + if(!entry.getValue().isConstant()) { + return entry.getValue().nominatorAsPolynomial().pCache(); + } + } + return std::make_shared(); + } template std::unordered_map> ApplyFiniteSchedulerToPomdp::getObservationChoiceWeights(PomdpFscApplicationMode applicationMode ) const { std::unordered_map> res; - RationalFunctionConstructor ratFuncConstructor; + RationalFunctionConstructor ratFuncConstructor(getCache(pomdp)); for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { auto observation = pomdp.getObservation(state); From 3282bf895c093e05da6075ec4d13865f7d7e1202 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 12 Jul 2020 21:58:19 -0700 Subject: [PATCH 03/12] more support for the modulo expression --- src/storm/storage/expressions/Expression.cpp | 4 ++++ src/storm/storage/expressions/Expression.h | 1 + src/test/storm/storage/ExpressionTest.cpp | 4 ++++ 3 files changed, 9 insertions(+) diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index 520bf1db4..873e21fc2 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/src/storm/storage/expressions/Expression.cpp @@ -449,6 +449,10 @@ namespace storm { Expression sum(std::vector const& expressions) { return applyAssociative(expressions, [] (Expression const& e1, Expression const& e2) { return e1 + e2; }); } + + Expression modulo(Expression const& first, Expression const& second) { + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().minimumMaximum(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo))); + } Expression apply(std::vector const& expressions, std::function const& function) { STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException, "Cannot build function application of empty expression list."); diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h index f8741440e..22b07734e 100644 --- a/src/storm/storage/expressions/Expression.h +++ b/src/storm/storage/expressions/Expression.h @@ -436,6 +436,7 @@ namespace storm { Expression floor(Expression const& first); Expression ceil(Expression const& first); Expression round(Expression const& first); + Expression modulo(Expression const& first, Expression const& second); Expression minimum(Expression const& first, Expression const& second); Expression maximum(Expression const& first, Expression const& second); Expression disjunction(std::vector const& expressions); diff --git a/src/test/storm/storage/ExpressionTest.cpp b/src/test/storm/storage/ExpressionTest.cpp index 8eef6195b..beadd6e94 100644 --- a/src/test/storm/storage/ExpressionTest.cpp +++ b/src/test/storm/storage/ExpressionTest.cpp @@ -257,6 +257,10 @@ TEST(Expression, OperatorTest) { EXPECT_TRUE(tempExpression.hasIntegerType()); ASSERT_NO_THROW(tempExpression = intVarExpression ^ rationalVarExpression); EXPECT_TRUE(tempExpression.hasRationalType()); + + STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::modulo(trueExpression, piExpression), storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(threeExpression, threeExpression)); + EXPECT_TRUE(tempExpression.hasIntegerType()); } TEST(Expression, SubstitutionTest) { From 5b7bc4319ad288660cdb47df9db0a849def09d2e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 13 Jul 2020 15:05:16 +0200 Subject: [PATCH 04/12] Missing pragma once --- src/storm-gspn/parser/GspnParser.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm-gspn/parser/GspnParser.h b/src/storm-gspn/parser/GspnParser.h index 512f0ddd6..b27c8975a 100644 --- a/src/storm-gspn/parser/GspnParser.h +++ b/src/storm-gspn/parser/GspnParser.h @@ -1,3 +1,5 @@ +#pragma once + #include "storm-gspn/storage/gspn/GSPN.h" namespace storm { From 8b2b0008da8cdcf44c484d6e637a086279230279 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 15 Jul 2020 09:51:00 +0200 Subject: [PATCH 05/12] The stack check issue has been fixed in newer AppleClang versions. Thus, we no longer have to disable stack checks for AppleClang 11.0.3 or higher. --- CMakeLists.txt | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 704396626..4847f91c0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -194,10 +194,9 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang") # using AppleClang if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 7.3) message(FATAL_ERROR "AppleClang version must be at least 7.3.") - elseif ((CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 11.0) OR (CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 11.0)) - message(WARNING "Temporarily disabling stack checks for AppleClang 11.0 or higher.") - # TODO: In release mode, stack checks currently fail at runtime. Might be a compiler bug as there does not seem to be faulty behavior. - # TODO: This seems to be fixed for clang 11.0.3 (bundled with XCode 11.5). Check again, if the clang version coming with the command line tools is greater than 11.0.0. + elseif ((CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 11.0.0) OR ((CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 11.0.0) AND (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 11.0.3))) + message(WARNING "Disabling stack checks for AppleClang versions between 11.0.0 and 11.0.2.") + # With these compiler versions, stack checks fail in release mode (most likely due to a bug in these versions). set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fno-stack-check") endif() From 1343ae5c19e731573568dd6a3cfcbd06b722f9b5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 15 Jul 2020 09:53:54 +0200 Subject: [PATCH 06/12] Fixed 'boost/optional.hpp file not found' error in storm-version library (simply by not using boost). --- CMakeLists.txt | 6 +++--- src/storm-version-info/storm-version.cpp.in | 2 +- src/storm-version-info/storm-version.h | 24 ++++++++++----------- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 4847f91c0..751e5a7e0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -439,15 +439,15 @@ set(STORM_VERSION_APPENDIX "${CMAKE_MATCH_5}") # might be empty if (STORM_GIT_VERSION_STRING MATCHES "NOTFOUND") set(STORM_VERSION_SOURCE "VersionSource::Static") set(STORM_VERSION_COMMITS_AHEAD 0) - set(STORM_VERSION_DIRTY boost::none) + set(STORM_VERSION_DIRTY DirtyState:Unknown) include(version.cmake) message(WARNING "Storm - Git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.") else() set(STORM_VERSION_SOURCE "VersionSource::Git") if ("${STORM_VERSION_APPENDIX}" MATCHES "^.*dirty.*$") - set(STORM_VERSION_DIRTY "true") + set(STORM_VERSION_DIRTY "DirtyState::Dirty") else() - set(STORM_VERSION_DIRTY "false") + set(STORM_VERSION_DIRTY "DirtyState::Clean") endif() endif() diff --git a/src/storm-version-info/storm-version.cpp.in b/src/storm-version-info/storm-version.cpp.in index dea052831..c63deab0f 100644 --- a/src/storm-version-info/storm-version.cpp.in +++ b/src/storm-version-info/storm-version.cpp.in @@ -11,7 +11,7 @@ namespace storm { const StormVersion::VersionSource StormVersion::versionSource = @STORM_VERSION_SOURCE@; const std::string StormVersion::gitRevisionHash = "@STORM_VERSION_GIT_HASH@"; const unsigned StormVersion::commitsAhead = @STORM_VERSION_COMMITS_AHEAD@; - const boost::optional StormVersion::dirty = @STORM_VERSION_DIRTY@; + const StormVersion::DirtyState StormVersion::dirty = @STORM_VERSION_DIRTY@; const std::string StormVersion::systemName = "@CMAKE_SYSTEM_NAME@"; const std::string StormVersion::systemVersion = "@CMAKE_SYSTEM_VERSION@"; const std::string StormVersion::cxxCompiler = "@STORM_COMPILER_ID@ @CMAKE_CXX_COMPILER_VERSION@"; diff --git a/src/storm-version-info/storm-version.h b/src/storm-version-info/storm-version.h index 297361fbb..5f07d5a22 100644 --- a/src/storm-version-info/storm-version.h +++ b/src/storm-version-info/storm-version.h @@ -3,8 +3,6 @@ #include #include -#include - namespace storm { struct StormVersion { @@ -36,8 +34,14 @@ namespace storm { /// How many commits passed since the tag was last set. const static unsigned commitsAhead; - /// 0 iff there no files were modified in the checkout, 1 otherwise. If none, no information about dirtyness is given. - const static boost::optional dirty; + enum class DirtyState { + Clean, /// no files were modified in the checkout + Dirty, /// some files were modified + Unknown /// No information about dirtyness is given. + }; + + /// Indicates whether files were modified + const static DirtyState dirty; /// The system which has compiled Storm. const static std::string systemName; @@ -77,14 +81,10 @@ namespace storm { } else { sstream << " built from archive"; } - if (dirty) { - if (dirty.get()) { - sstream << " (dirty)"; - } else { - sstream << " (clean)"; - } - } else { - sstream << " (potentially dirty)"; + switch (dirty) { + case DirtyState::Clean: sstream << " (clean)"; break; + case DirtyState::Dirty: sstream << " (dirty)"; break; + default: sstream << " (potentially dirty)"; break; } return sstream.str(); } From 03e0b01ae2fe366bc9e91cb2d1969579bcde356b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 16 Jul 2020 20:52:54 -0700 Subject: [PATCH 07/12] Making POMDPs simple now does not introduce further initial states --- src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp b/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp index 358ad3041..baace3c5f 100644 --- a/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp +++ b/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp @@ -141,8 +141,11 @@ namespace storm { for (auto const& labelName : pomdp.getStateLabeling().getLabels()) { storm::storage::BitVector newStates = pomdp.getStateLabeling().getStates(labelName); newStates.resize(data.simpleMatrix.getRowGroupCount(), false); - for (uint64_t newState = pomdp.getNumberOfStates(); newState < data.simpleMatrix.getRowGroupCount(); ++newState ) { - newStates.set(newState, newStates[data.simpleStateToOriginalState[newState]]); + if (labelName != "init") { + for (uint64_t newState = pomdp.getNumberOfStates(); + newState < data.simpleMatrix.getRowGroupCount(); ++newState) { + newStates.set(newState, newStates[data.simpleStateToOriginalState[newState]]); + } } labeling.addLabel(labelName, std::move(newStates)); From b3e37c1eb836082cf31340684d743f57d8642040 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 16 Jul 2020 23:41:39 -0700 Subject: [PATCH 08/12] partial (parametric) model instantiators --- src/storm-pars/utility/ModelInstantiator.cpp | 11 +++++---- src/storm-pars/utility/ModelInstantiator.h | 24 +++++++++++++++++++- src/storm-pars/utility/parametric.cpp | 8 ++++++- src/storm-pars/utility/parametric.h | 8 ++++++- 4 files changed, 44 insertions(+), 7 deletions(-) diff --git a/src/storm-pars/utility/ModelInstantiator.cpp b/src/storm-pars/utility/ModelInstantiator.cpp index f59649ab7..719427529 100644 --- a/src/storm-pars/utility/ModelInstantiator.cpp +++ b/src/storm-pars/utility/ModelInstantiator.cpp @@ -137,10 +137,7 @@ namespace storm { template ConstantSparseModelType const& ModelInstantiator::instantiate(storm::utility::parametric::Valuation const& valuation){ //Write results into the placeholders - for(auto& functionResult : this->functions){ - functionResult.second=storm::utility::convertNumber( - storm::utility::parametric::evaluate(functionResult.first, valuation)); - } + instantiate_helper(valuation); //Write the instantiated values to the matrices and vectors according to the stored mappings for(auto& entryValuePair : this->matrixMapping){ @@ -170,6 +167,12 @@ namespace storm { template class ModelInstantiator, storm::models::sparse::Ctmc>; template class ModelInstantiator, storm::models::sparse::MarkovAutomaton>; template class ModelInstantiator, storm::models::sparse::StochasticTwoPlayerGame>; + + // For stormpy: + template class ModelInstantiator, storm::models::sparse::Dtmc>; + template class ModelInstantiator, storm::models::sparse::Mdp>; + template class ModelInstantiator, storm::models::sparse::Ctmc>; + template class ModelInstantiator, storm::models::sparse::MarkovAutomaton>; #endif } //namespace utility } //namespace storm diff --git a/src/storm-pars/utility/ModelInstantiator.h b/src/storm-pars/utility/ModelInstantiator.h index e96a4dda8..cba624074 100644 --- a/src/storm-pars/utility/ModelInstantiator.h +++ b/src/storm-pars/utility/ModelInstantiator.h @@ -117,7 +117,29 @@ namespace storm { this->instantiatedModel = std::make_shared(std::move(components)); } - + + template + typename std::enable_if< + std::is_same::value + >::type + instantiate_helper(storm::utility::parametric::Valuation const& valuation) { + for(auto& functionResult : this->functions){ + functionResult.second= + storm::utility::parametric::substitute(functionResult.first, valuation); + } + } + + template + typename std::enable_if< + !std::is_same::value + >::type + instantiate_helper(storm::utility::parametric::Valuation const& valuation) { + for(auto& functionResult : this->functions){ + functionResult.second=storm::utility::convertNumber( + storm::utility::parametric::evaluate(functionResult.first, valuation)); + } + } + /*! * Creates a matrix that has entries at the same position as the given matrix. * The returned matrix is a stochastic matrix, i.e., the rows sum up to one. diff --git a/src/storm-pars/utility/parametric.cpp b/src/storm-pars/utility/parametric.cpp index 3b6934a3e..96c30e78e 100644 --- a/src/storm-pars/utility/parametric.cpp +++ b/src/storm-pars/utility/parametric.cpp @@ -21,7 +21,13 @@ namespace storm { typename CoefficientType::type evaluate(storm::RationalFunction const& function, Valuation const& valuation){ return function.evaluate(valuation); } - + + template<> + typename storm::RationalFunction substitute(storm::RationalFunction const& function, Valuation const& valuation){ + return function.substitute(valuation); + } + + template<> void gatherOccurringVariables(storm::RationalFunction const& function, std::set::type>& variableSet){ function.gatherVariables(variableSet); diff --git a/src/storm-pars/utility/parametric.h b/src/storm-pars/utility/parametric.h index 77a58e7f8..31a81f1a7 100644 --- a/src/storm-pars/utility/parametric.h +++ b/src/storm-pars/utility/parametric.h @@ -35,7 +35,13 @@ namespace storm { */ template typename CoefficientType::type evaluate(FunctionType const& function, Valuation const& valuation); - + + /*! + * Evaluates the given function wrt. the given valuation + */ + template + FunctionType substitute(FunctionType const& function, Valuation const& valuation); + /*! * Add all variables that occur in the given function to the the given set */ From c6fd7423f2db1e33c76f15ab4ff85d669f73900f Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 20 Jul 2020 10:13:18 +0200 Subject: [PATCH 09/12] Disabling stack checks once again for all clang versions >= 11.0.0 because they somehow interfere with exception handling in the PrismParser. (most likely a clang bug). --- CMakeLists.txt | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 751e5a7e0..0a88333f6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -194,9 +194,11 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang") # using AppleClang if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 7.3) message(FATAL_ERROR "AppleClang version must be at least 7.3.") - elseif ((CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 11.0.0) OR ((CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 11.0.0) AND (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 11.0.3))) - message(WARNING "Disabling stack checks for AppleClang versions between 11.0.0 and 11.0.2.") - # With these compiler versions, stack checks fail in release mode (most likely due to a bug in these versions). + elseif ((CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 11.0.0) OR (CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 11.0.0)) + message(WARNING "Disabling stack checks for AppleClang version 11.0.0 or higher.") + # Stack checks are known to produce errors with the following Clang versions: + # 11.0.0: Runtime errors (stack_not_16_byte_aligned_error) when invoking storm in release mode + # 11.0.3: Catching exceptions thrown within PRISM parser does not work (The exception just falls through) set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fno-stack-check") endif() From 17a1d02757d2d4e5e6683704e05d3595c0d37a02 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 20 Jul 2020 10:47:35 +0200 Subject: [PATCH 10/12] Cmake: Detection for the old in-source "storm-version.cpp" file. The file will now be deleted (if found) to prevent build issues for people that upgraded from older storm versions. --- src/storm/CMakeLists.txt | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index dcd1bb9f9..de0a9bd8d 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -1,3 +1,15 @@ +# Storm versions before 1.6.0 generated an in-source .cpp file containing version information. +# When users upgrade from such a version, the generated file will still be there. +# We now delete this file to prevent building issues as there is no corresponding .h file (anymore). +if ((EXISTS "${PROJECT_SOURCE_DIR}/src/storm/utility/storm-version.cpp")) + file(READ "${PROJECT_SOURCE_DIR}/src/storm/utility/storm-version.cpp" STORM_OLD_VERSION_FILE) + string(FIND "${STORM_OLD_VERSION_FILE}" "// AUTO GENERATED -- DO NOT CHANGE" STORM_OLD_VERSION_FILE_DETECTED) + if (STORM_OLD_VERSION_FILE_DETECTED EQUAL 0) + message(WARNING "Storm - The file ${PROJECT_SOURCE_DIR}/src/storm/utility/storm-version.cpp was probably generated by an old Storm version and will be deleted now.") + file(REMOVE "${PROJECT_SOURCE_DIR}/src/storm/utility/storm-version.cpp") + endif(STORM_OLD_VERSION_FILE_DETECTED EQUAL 0) +endif() + file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm/*.h ${PROJECT_SOURCE_DIR}/src/storm/*.cpp) register_source_groups_from_filestructure("${ALL_FILES}" storm) From 8d75b84ba6e5d39e4fe153b604932a1be69c8129 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 20 Jul 2020 11:30:08 +0200 Subject: [PATCH 11/12] Throw error when using ThinLTO and GCC --- CMakeLists.txt | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 0a88333f6..cbab845cc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -277,13 +277,17 @@ elseif (STORM_COMPILER_GCC) endif () if (STORM_USE_THIN_LTO) - set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto=thin") - message(STATUS "Storm - Enabling link-time optimizations using ThinLTO.") + if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG) + set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto=thin") + message(STATUS "Storm - Enabling link-time optimizations using ThinLTO.") + else() + message(FATAL_ERROR "Storm - ThinLTO only supported for Clang. Use regular LTO instead.") + endif() elseif (STORM_USE_LTO) set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto") # Fix for problems that occurred when using LTO on gcc. This should be removed when it - # is not needed anymore as it makes the the already long link-step potentially longer. + # is not needed anymore as it makes the already long link-step potentially longer. if (STORM_COMPILER_GCC) set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto-partition=none") endif() From 5722c1258c99a5a35fd26974ea44f1626580afff Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 20 Jul 2020 17:14:24 -0700 Subject: [PATCH 12/12] pipe all rf-variable creations through a single object file --- .../transformer/ApplyFiniteSchedulerToPomdp.cpp | 2 +- src/storm/adapters/RationalFunctionAdapter.cpp | 7 +++++++ src/storm/adapters/RationalFunctionAdapter.h | 2 ++ src/storm/builder/DdPrismModelBuilder.cpp | 2 +- .../storage/expressions/ToRationalFunctionVisitor.cpp | 2 +- 5 files changed, 12 insertions(+), 3 deletions(-) create mode 100644 src/storm/adapters/RationalFunctionAdapter.cpp diff --git a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp index a125289bf..00e443efe 100644 --- a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp +++ b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp @@ -60,7 +60,7 @@ namespace storm { storm::RationalFunction lastWeight = storm::utility::one(); for (uint64_t a = 0; a < pomdp.getNumberOfChoices(state) - 1; ++a) { std::string varName = "p" + std::to_string(observation) + "_" + std::to_string(a); - storm::RationalFunction var = ratFuncConstructor.translate(carl::freshRealVariable(varName)); + storm::RationalFunction var = ratFuncConstructor.translate(storm::createRFVariable(varName)); if (applicationMode == PomdpFscApplicationMode::SIMPLE_LINEAR) { weights.push_back(collected * var); collected *= storm::utility::one() - var; diff --git a/src/storm/adapters/RationalFunctionAdapter.cpp b/src/storm/adapters/RationalFunctionAdapter.cpp new file mode 100644 index 000000000..7218c4454 --- /dev/null +++ b/src/storm/adapters/RationalFunctionAdapter.cpp @@ -0,0 +1,7 @@ +#include "storm/adapters/RationalFunctionAdapter.h" + +namespace storm { + RationalFunctionVariable createRFVariable(std::string const& name) { + return carl::freshRealVariable(name); + } +} \ No newline at end of file diff --git a/src/storm/adapters/RationalFunctionAdapter.h b/src/storm/adapters/RationalFunctionAdapter.h index 9ecf8b579..0387aae63 100644 --- a/src/storm/adapters/RationalFunctionAdapter.h +++ b/src/storm/adapters/RationalFunctionAdapter.h @@ -41,6 +41,8 @@ namespace carl { namespace storm { typedef carl::Variable RationalFunctionVariable; + RationalFunctionVariable createRFVariable(std::string const& name); + #if defined(STORM_HAVE_CLN) && defined(STORM_USE_CLN_RF) typedef cln::cl_RA RationalFunctionCoefficient; #elif defined(STORM_HAVE_GMP) && !defined(STORM_USE_CLN_RF) diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 9e907a857..b08e9295d 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -56,7 +56,7 @@ namespace storm { void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter& rowExpressionAdapter) { for (auto const& constant : program.getConstants()) { if (!constant.isDefined()) { - storm::RationalFunctionVariable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName()); + storm::RationalFunctionVariable carlVariable = storm::createRFVariable(constant.getExpressionVariable().getName()); parameters.insert(carlVariable); auto rf = convertVariableToPolynomial(carlVariable); rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf); diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp index 21ee060ea..21aeddce8 100644 --- a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp @@ -82,7 +82,7 @@ namespace storm { if (variablePair != variableToVariableMap.end()) { return convertVariableToPolynomial(variablePair->second); } else { - storm::RationalFunctionVariable carlVariable = carl::freshRealVariable(expression.getVariableName()); + storm::RationalFunctionVariable carlVariable = storm::createRFVariable(expression.getVariableName()); variableToVariableMap.emplace(expression.getVariable(), carlVariable); return convertVariableToPolynomial(carlVariable); }