From 1cf8674fa5e6bd515712ef365701c764b4b89a80 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 27 Oct 2014 02:05:41 +0100 Subject: [PATCH 1/8] Added noexcept Destructors to the exceptions to fix the picky Clang3.5 compiler errors. Former-commit-id: f620e5ed7deccafa3aa8115fe3883bd97323b527 --- src/exceptions/BaseException.cpp | 4 ++++ src/exceptions/BaseException.h | 5 +++++ src/exceptions/ExceptionMacros.h | 2 ++ 3 files changed, 11 insertions(+) diff --git a/src/exceptions/BaseException.cpp b/src/exceptions/BaseException.cpp index 0acae02ac..8a295b541 100644 --- a/src/exceptions/BaseException.cpp +++ b/src/exceptions/BaseException.cpp @@ -13,6 +13,10 @@ namespace storm { BaseException::BaseException(char const* cstr) { stream << cstr; } + + BaseException::~BaseException() { + // Intentionally left empty. + } const char* BaseException::what() const throw() { std::string errorString = this->stream.str(); diff --git a/src/exceptions/BaseException.h b/src/exceptions/BaseException.h index 8bf12ea23..f6fb488a0 100644 --- a/src/exceptions/BaseException.h +++ b/src/exceptions/BaseException.h @@ -29,6 +29,11 @@ namespace storm { */ BaseException(char const* cstr); + /*! + * Declare a destructor to counter the "looser throw specificator" error + */ + virtual ~BaseException() throw(); + /*! * Retrieves the message associated with this exception. * diff --git a/src/exceptions/ExceptionMacros.h b/src/exceptions/ExceptionMacros.h index 943990ae7..e7bfe5885 100644 --- a/src/exceptions/ExceptionMacros.h +++ b/src/exceptions/ExceptionMacros.h @@ -13,6 +13,8 @@ exception_name(char const* cstr) : BaseException(cstr) { \ } \ exception_name(exception_name const& cp) : BaseException(cp) { \ } \ +~exception_name() throw() { \ +} \ template \ exception_name& operator<<(T const& var) { \ this->stream << var; \ From 9fc68a554c0cae1354b5e26aa0a6278d0d13d0a9 Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 29 Oct 2014 22:50:22 +0100 Subject: [PATCH 2/8] Cherry-picked a fix for GCC from branch. Former-commit-id: 98f7c52b346623f3de8a5f90b9a99e973ea7a25b --- src/storage/DeterministicModelBisimulationDecomposition.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 7ad0bd8ec..ccb33a153 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -763,8 +763,8 @@ namespace storm { std::sort(partition.getBegin(block), partition.getEnd(block), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; }); // Convert the state-value-pairs to states only. - auto lambda = [] (std::pair const& a) -> storm::storage::sparse::state_type { return a.first; }; - this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), lambda), boost::make_transform_iterator(partition.getEnd(block), lambda), true); + std::function const&)> projection = [](std::pair const& a) -> storm::storage::sparse::state_type { return a.first; }; + this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), projection), boost::make_transform_iterator(partition.getEnd(block), projection), true); } // If we are required to build the quotient model, do so now. From a0b54fbca45f5dd584180618929344a775b13f05 Mon Sep 17 00:00:00 2001 From: svkurowski Date: Mon, 24 Nov 2014 23:04:53 +0100 Subject: [PATCH 3/8] Add src/utility/storm-version.cpp to ignored files This file is generated by CMake. A more robust solution would be to configure this file out-of-source much like build/include/storm-config.h. Former-commit-id: 05eacc7a5bb3797bda09599654d9c93d41a78545 --- .gitignore | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.gitignore b/.gitignore index aa15c7b9a..03286848f 100644 --- a/.gitignore +++ b/.gitignore @@ -43,3 +43,5 @@ build//CMakeLists.txt #Temp texteditor files *.orig *.*~ +# CMake generated/configured files +src/utility/storm-version.cpp From 2f20abf47f8d60fa599dc512a2f9a98af50303c3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 27 Nov 2014 11:33:32 +0100 Subject: [PATCH 4/8] The user can now select on the command line which reward model of a symbolic model is to be used (as a second [optional] argument to --symbolic). Former-commit-id: 02f998e5dd59fec893602fc0c59d54c0b5c5235b --- src/adapters/ExplicitModelAdapter.h | 24 +++++++++--------------- src/settings/modules/GeneralSettings.cpp | 11 ++++++++++- src/settings/modules/GeneralSettings.h | 15 ++++++++++++++- src/storage/prism/Program.cpp | 9 +++++++++ src/storage/prism/Program.h | 15 +++++++++++++++ src/storage/prism/RewardModel.cpp | 4 ++++ src/storage/prism/RewardModel.h | 7 +++++++ src/utility/cli.h | 2 +- 8 files changed, 69 insertions(+), 18 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index edde6925d..38758fce7 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -95,12 +95,10 @@ namespace storm { * @param program The program to translate. * @param constantDefinitionString A string that contains a comma-separated definition of all undefined * constants in the model. - * @param rewardModelName The name of reward model to be added to the model. This must be either a reward - * model of the program or the empty string. In the latter case, the constructed model will contain no - * rewards. + * @param rewardModel The reward model that is to be built. * @return The explicit model that was given by the probabilistic program. */ - static std::unique_ptr> translateProgram(storm::prism::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") { + static std::unique_ptr> translateProgram(storm::prism::Program program, storm::prism::RewardModel const& rewardModel = storm::prism::RewardModel(), std::string const& constantDefinitionString = "") { // Start by defining the undefined constants in the model. // First, we need to parse the constant definition string. std::map constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); @@ -113,21 +111,21 @@ namespace storm { // constants in the state (i.e., valuation). preparedProgram = preparedProgram.substituteConstants(); - ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModelName); + ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel); std::unique_ptr> result; switch (program.getModelType()) { case storm::prism::Program::ModelType::DTMC: - result = std::unique_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::CTMC: - result = std::unique_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::MDP: - result = std::unique_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::CTMDP: - result = std::unique_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; default: LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type."); @@ -634,11 +632,10 @@ namespace storm { * Explores the state space of the given program and returns the components of the model as a result. * * @param program The program whose state space to explore. - * @param rewardModelName The name of the reward model that is to be considered. If empty, no reward model - * is considered. + * @param rewardModel The reward model that is to be considered. * @return A structure containing the components of the resulting model. */ - static ModelComponents buildModelComponents(storm::prism::Program const& program, std::string const& rewardModelName) { + static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel) { ModelComponents modelComponents; VariableInformation variableInformation; @@ -654,9 +651,6 @@ namespace storm { // Create the structure for storing the reachable state space. StateInformation stateInformation; - // Get the selected reward model or create an empty one if none is selected. - storm::prism::RewardModel const& rewardModel = rewardModelName != "" ? program.getRewardModel(rewardModelName) : storm::prism::RewardModel(); - // Determine whether we have to combine different choices to one or whether this model can have more than // one choice per state. bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC; diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index d04ec0d25..ece0d9a00 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -61,7 +61,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("rewardmodel", "The name of the reward model to use.").setDefaultValueString("").setIsOptional(true).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies a PCTL formula that is to be checked on the model.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, pctlFileOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.") @@ -154,6 +155,14 @@ namespace storm { return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString(); } + bool GeneralSettings::isSymbolicRewardModelNameSet() const { + return this->getOption(symbolicOptionName).getArgumentByName("rewardmodel").getHasBeenSet(); + } + + std::string GeneralSettings::getSymbolicRewardModelName() const { + return this->getOption(symbolicOptionName).getArgumentByName("rewardmodel").getValueAsString(); + } + bool GeneralSettings::isPctlPropertySet() const { return this->getOption(pctlOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index c65ab57a2..22f8fe58f 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -39,7 +39,6 @@ namespace storm { */ bool isVersionSet() const; - /*! * Retrieves the name of the module for which to show the help or "all" to indicate that the full help * needs to be shown. @@ -127,6 +126,20 @@ namespace storm { * @return The name of the file that contains the symbolic model specification. */ std::string getSymbolicModelFilename() const; + + /*! + * Retrieves whether the name of a reward model was passed to the symbolic option. + * + * @return True iff the name of a reward model was passed to the symbolic option. + */ + bool isSymbolicRewardModelNameSet() const; + + /*! + * Retrieves the name of the reward model if one was set using the symbolic option. + * + * @return The name of the selected reward model. + */ + std::string getSymbolicRewardModelName() const; /*! * Retrieves whether the pctl option was set. diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index f053c93e8..5392a7949 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -145,6 +145,10 @@ namespace storm { return variableNameToModuleIndexPair->second; } + bool Program::hasRewardModel() const { + return !this->rewardModels.empty(); + } + std::vector const& Program::getRewardModels() const { return this->rewardModels; } @@ -159,6 +163,11 @@ namespace storm { return this->getRewardModels()[nameIndexPair->second]; } + RewardModel const& Program::getRewardModel(uint_fast64_t index) const { + STORM_LOG_THROW(this->getNumberOfRewardModels() > index, storm::exceptions::OutOfRangeException, "Reward model with index " << index << " does not exist."); + return this->rewardModels[index]; + } + std::vector