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_ */ 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)); } 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()); 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_ */ diff --git a/src/utility/storm.h b/src/utility/storm.h index a341f5b32..83afad43a 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -115,10 +115,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); }