From 9f6bd1805f8e9b79e7fd5ecb4bc2d7e6224e01c8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 9 Jun 2016 09:51:46 +0200 Subject: [PATCH] modified the entry point code to deal with the new generator-builder-structure Former-commit-id: f01a19e3468dd052e6e8f1974f968014cc018f2f --- src/builder/ExplicitModelBuilder.cpp | 2 +- src/generator/PrismNextStateGenerator.cpp | 15 ++++++++++++++- src/utility/storm.h | 20 +++++++++----------- 3 files changed, 24 insertions(+), 13 deletions(-) diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index b1d67bee2..d1265df9a 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -32,7 +32,7 @@ namespace storm { template class RewardModelBuilder { public: - RewardModelBuilder(storm::generator::RewardModelInformation const& rewardModelInformation) : rewardModelName(rewardModelInformation.getName()), stateRewards(rewardModelInformation.hasStateRewards()), stateRewardVector(), stateActionRewards(rewardModelInformation.hasStateActionRewards()), stateActionRewardVector() { + RewardModelBuilder(storm::generator::RewardModelInformation const& rewardModelInformation) : rewardModelName(rewardModelInformation.getName()), stateRewards(rewardModelInformation.hasStateRewards()), stateActionRewards(rewardModelInformation.hasStateActionRewards()), stateRewardVector(), stateActionRewardVector() { STORM_LOG_THROW(!rewardModelInformation.hasTransitionRewards(), storm::exceptions::InvalidArgumentException, "Unable to treat transition rewards."); } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index da83134ef..1ec8c3243 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -8,6 +8,7 @@ #include "src/utility/constants.h" #include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/WrongFormatException.h" namespace storm { @@ -19,7 +20,19 @@ namespace storm { // Extract the reward models from the program based on the names we were given. for (auto const& rewardModelName : this->options.getRewardModelNames()) { - rewardModels.push_back(program.getRewardModel(rewardModelName)); + if (program.hasRewardModel(rewardModelName)) { + rewardModels.push_back(program.getRewardModel(rewardModelName)); + } else { + STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'."); + STORM_LOG_THROW(program.getNumberOfRewardModels() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous."); + STORM_LOG_THROW(program.getNumberOfRewardModels() > 0, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is invalid, because there is no reward model."); + } + } + + // If no reward model was yet added, but there was one that was given in the options, we try to build + // standard reward model. + if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) { + rewardModels.push_back(program.getRewardModel(0)); } // If there are terminal states we need to handle, we now need to translate all labels to expressions. diff --git a/src/utility/storm.h b/src/utility/storm.h index 91047f751..fff7e8576 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -72,7 +72,8 @@ #include "src/counterexamples/MILPMinimalLabelSetGenerator.h" #include "src/counterexamples/SMTMinimalCommandSetGenerator.h" -// Headers related to program preprocessing. +// Headers related to PRISM model building. +#include "src/generator/PrismNextStateGenerator.h" #include "src/utility/prism.h" // Headers related to exception handling. @@ -99,25 +100,23 @@ namespace storm { template storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { storm::storage::ModelFormulasPair result; - storm::prism::Program translatedProgram; - + // Get the string that assigns values to the unknown currently undefined constants in the model. std::string constantDefinitionString = storm::settings::getModule().getConstantDefinitionString(); - translatedProgram = storm::utility::prism::preprocess(program, constantDefinitionString); - std::map constantsSubstitution = translatedProgram.getConstantsSubstitution(); + storm::prism::Program preprocessedProgram = storm::utility::prism::preprocess(program, constantDefinitionString); + std::map constantsSubstitution = preprocessedProgram.getConstantsSubstitution(); // Customize and perform model-building. if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse) { - typename storm::builder::ExplicitModelBuilder>::Options options; - options = typename storm::builder::ExplicitModelBuilder>::Options(formulas); - options.addConstantDefinitionsFromString(program, constants); + storm::generator::NextStateGeneratorOptions options(formulas); // Generate command labels if we are going to build a counterexample later. if (storm::settings::getModule().isMinimalCommandSetGenerationSet()) { - options.buildCommandLabels = true; + options.setBuildChoiceLabels(true); } - storm::builder::ExplicitModelBuilder builder(program, options); + std::shared_ptr> generator = std::make_shared>(preprocessedProgram, options); + storm::builder::ExplicitModelBuilder builder(generator); result.model = builder.translate(); } else if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Dd || storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) { typename storm::builder::DdPrismModelBuilder::Options options; @@ -126,7 +125,6 @@ namespace storm { storm::builder::DdPrismModelBuilder builder; result.model = builder.translateProgram(program, options); - translatedProgram = builder.getTranslatedProgram(); } // There may be constants of the model appearing in the formulas, so we replace all their occurrences