From 556b8e872641686e76545098ad3156ba75962f66 Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Wed, 29 Jun 2016 17:15:20 +0200 Subject: [PATCH 1/5] Return reference to settings module, not a copy Former-commit-id: 0a5befee57d1f264268f19085aa859dad9987963 --- src/settings/SettingsManager.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 11c9d78d6..6b1afe5db 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -260,7 +260,7 @@ namespace storm { * @return The module. */ template - SettingsType getModule() { + SettingsType const& getModule() { static_assert(std::is_base_of::value, "Template argument must be derived from ModuleSettings"); return dynamic_cast(manager().getModule(SettingsType::moduleName)); } From a2140141a3bba6d628c5bd61b0cbcf09aaebe813 Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Wed, 29 Jun 2016 18:05:56 +0200 Subject: [PATCH 2/5] Fix virtual destructor Former-commit-id: ff3ee6cafac3985054bedc09593d6c645dd4c0b1 --- src/settings/modules/ModuleSettings.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/settings/modules/ModuleSettings.h b/src/settings/modules/ModuleSettings.h index 08c92909d..2145d5267 100644 --- a/src/settings/modules/ModuleSettings.h +++ b/src/settings/modules/ModuleSettings.h @@ -30,6 +30,7 @@ namespace storm { * @param moduleName The name of the module for which to build the settings. */ ModuleSettings(std::string const& moduleName); + virtual ~ModuleSettings() {} /*! * Checks whether the settings are consistent. If they are inconsistent, an exception is thrown. @@ -140,4 +141,4 @@ namespace storm { } // namespace settings } // namespace storm -#endif /* STORM_SETTINGS_MODULES_MODULESETTINGS_H_ */ \ No newline at end of file +#endif /* STORM_SETTINGS_MODULES_MODULESETTINGS_H_ */ From ffe325b1964a63198d68e1521ff94c0c92496471 Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Thu, 30 Jun 2016 11:29:00 +0200 Subject: [PATCH 3/5] Fix unitialized data in coresettings Former-commit-id: 7c0dac26ba4df2e22f5296a45862d3a6392c87b3 --- src/settings/modules/CoreSettings.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/settings/modules/CoreSettings.cpp b/src/settings/modules/CoreSettings.cpp index 5617d959c..b42a301c8 100644 --- a/src/settings/modules/CoreSettings.cpp +++ b/src/settings/modules/CoreSettings.cpp @@ -32,7 +32,7 @@ namespace storm { const std::string CoreSettings::cudaOptionName = "cuda"; const std::string CoreSettings::minMaxEquationSolvingTechniqueOptionName = "ndmethod"; - CoreSettings::CoreSettings() : ModuleSettings(moduleName) { + CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(CoreSettings::Engine::Sparse) { 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.").setDefaultValueString("-").setIsOptional(true).build()).setShortName(counterexampleOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build()); From 8546786e1757e6140b64795dac29447ea6342ede Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Thu, 30 Jun 2016 17:11:54 +0200 Subject: [PATCH 4/5] Fix missing template argument in builder utility Former-commit-id: 23d683f29ced31bd7a84061252fcbd62a609c476 --- src/utility/storm.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/utility/storm.h b/src/utility/storm.h index 41a17a4c7..49ef4bf04 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -113,10 +113,10 @@ namespace storm { template std::shared_ptr> buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - typename storm::builder::DdPrismModelBuilder::Options options; - options = typename storm::builder::DdPrismModelBuilder::Options(formulas); + typename storm::builder::DdPrismModelBuilder::Options options; + options = typename storm::builder::DdPrismModelBuilder::Options(formulas); - storm::builder::DdPrismModelBuilder builder; + storm::builder::DdPrismModelBuilder builder; return builder.build(program, options); } From f2035523afb472ae26b0a8d43c1d5eda773593b7 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 30 Jun 2016 21:50:33 +0200 Subject: [PATCH 5/5] Fixed a bug in rewardModel's reduceToStateBasedRewards. Also added a function to check whether all rewards are zero. Former-commit-id: 4dabd07c6693a51c25babb7c73d47dca18ff4a1c --- src/models/sparse/StandardRewardModel.cpp | 14 +++++++++++--- src/models/sparse/StandardRewardModel.h | 9 ++++++++- 2 files changed, 19 insertions(+), 4 deletions(-) diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp index 3bd624d3d..c8fd2aa8f 100644 --- a/src/models/sparse/StandardRewardModel.cpp +++ b/src/models/sparse/StandardRewardModel.cpp @@ -145,15 +145,15 @@ namespace storm { if (this->hasTransitionRewards()) { if (this->hasStateActionRewards()) { storm::utility::vector::addVectors(this->getStateActionRewardVector(), transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()), this->getStateActionRewardVector()); - this->optionalStateActionRewardVector = boost::none; + this->optionalTransitionRewardMatrix = boost::none; } else { this->optionalStateActionRewardVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); } } if (reduceToStateRewards && this->hasStateActionRewards()) { + STORM_LOG_THROW(transitionMatrix.getRowGroupCount() == this->getStateActionRewardVector().size(), storm::exceptions::InvalidOperationException, "The reduction to state rewards is only possible if the size of the action reward vector equals the number of states."); if (this->hasStateRewards()) { - STORM_LOG_THROW(this->getStateRewardVector().size() == this->getStateActionRewardVector().size(), storm::exceptions::InvalidOperationException, "The reduction to state rewards is only possible of both the state and the state-action rewards have the same dimension."); storm::utility::vector::addVectors(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector()); } else { this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector); @@ -242,6 +242,14 @@ namespace storm { bool StandardRewardModel::empty() const { return !(static_cast(this->optionalStateRewardVector) || static_cast(this->optionalStateActionRewardVector) || static_cast(this->optionalTransitionRewardMatrix)); } + + template + bool StandardRewardModel::isAllZero() const { + if(hasStateRewards() && !std::all_of(getStateRewardVector().begin(), getStateRewardVector().end(), storm::utility::isZero)) { + return false; + } + return !(static_cast(this->optionalStateRewardVector) || static_cast(this->optionalStateActionRewardVector) || static_cast(this->optionalTransitionRewardMatrix)); + } @@ -335,4 +343,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/models/sparse/StandardRewardModel.h b/src/models/sparse/StandardRewardModel.h index 6e153fa07..985f4189c 100644 --- a/src/models/sparse/StandardRewardModel.h +++ b/src/models/sparse/StandardRewardModel.h @@ -253,6 +253,13 @@ namespace storm { * @return True iff the reward model is empty. */ bool empty() const; + + /*! + * Retrieves whether every reward defined by this reward model is zero + * + * @return True iff every reward defined by this reward model is zero. + */ + bool isAllZero() const; /*! * Checks whether the reward model is compatible with key model characteristics. @@ -293,4 +300,4 @@ namespace storm { } } -#endif /* STORM_MODELS_SPARSE_STANDARDREWARDMODEL_H_ */ \ No newline at end of file +#endif /* STORM_MODELS_SPARSE_STANDARDREWARDMODEL_H_ */