From 4063d88913d6c6f31dfc125f928e3cb4912bfd92 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 9 Jun 2016 10:51:19 +0200 Subject: [PATCH] added option to build all labels/reward models for next-state generators Former-commit-id: cfb9787d6c940bd60f79e9929d3a9b4c3a4c3a01 --- src/builder/DdPrismModelBuilder.cpp | 28 ++------------ src/generator/NextStateGenerator.cpp | 38 ++++++++++++++----- src/generator/NextStateGenerator.h | 19 ++++++++-- src/generator/PrismNextStateGenerator.cpp | 46 ++++++++++++++--------- src/utility/storm.h | 1 - 5 files changed, 77 insertions(+), 55 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index ac02b9761..dae747228 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -473,18 +473,18 @@ namespace storm { }; template - DdPrismModelBuilder::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), buildAllLabels(true), labelsToBuild(), terminalStates(), negatedTerminalStates() { // Intentionally left empty. } template - DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set()), terminalStates(), negatedTerminalStates() { this->preserveFormula(formula); this->setTerminalStatesFromFormula(formula); } template - DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; @@ -554,22 +554,6 @@ namespace storm { } } - template - void DdPrismModelBuilder::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) { - std::map newConstantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); - - // If there is at least one constant that is defined, and the constant definition map does not yet exist, - // we need to create it. - if (!constantDefinitions && !newConstantDefinitions.empty()) { - constantDefinitions = std::map(); - } - - // Now insert all the entries that need to be defined. - for (auto const& entry : newConstantDefinitions) { - constantDefinitions.get().insert(entry); - } - } - template struct DdPrismModelBuilder::SystemResult { SystemResult(storm::dd::Add const& allTransitionsDd, DdPrismModelBuilder::ModuleDecisionDiagram const& globalModule, storm::dd::Add const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) { @@ -1248,11 +1232,7 @@ namespace storm { template std::shared_ptr> DdPrismModelBuilder::build(storm::prism::Program const& program, Options const& options) { - if (options.constantDefinitions) { - preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get()); - } else { - preparedProgram = program; - } + preparedProgram = program; if (preparedProgram->hasUndefinedConstants()) { std::vector> undefinedConstants = preparedProgram->getUndefinedConstants(); diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index 26563d408..05cdf7f1d 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -5,7 +5,7 @@ #include "src/logic/Formulas.h" #include "src/utility/macros.h" -#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/InvalidSettingsException.h" namespace storm { namespace generator { @@ -34,16 +34,16 @@ namespace storm { return boost::get(labelOrExpression); } - NextStateGeneratorOptions::NextStateGeneratorOptions() : buildChoiceLabels(false) { + NextStateGeneratorOptions::NextStateGeneratorOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false) { // Intentionally left empty. } - NextStateGeneratorOptions::NextStateGeneratorOptions(storm::logic::Formula const& formula) { + NextStateGeneratorOptions::NextStateGeneratorOptions(storm::logic::Formula const& formula) : NextStateGeneratorOptions() { this->preserveFormula(formula); this->setTerminalStatesFromFormula(formula); } - NextStateGeneratorOptions::NextStateGeneratorOptions(std::vector> const& formulas) { + NextStateGeneratorOptions::NextStateGeneratorOptions(std::vector> const& formulas) : NextStateGeneratorOptions() { if (!formulas.empty()) { for (auto const& formula : formulas) { this->preserveFormula(*formula); @@ -112,8 +112,8 @@ namespace storm { return rewardModelNames; } - std::set const& NextStateGeneratorOptions::getLabels() const { - return labels; + std::set const& NextStateGeneratorOptions::getLabelNames() const { + return labelNames; } std::vector const& NextStateGeneratorOptions::getExpressionLabels() const { @@ -135,19 +135,39 @@ namespace storm { bool NextStateGeneratorOptions::isBuildChoiceLabelsSet() const { return buildChoiceLabels; } + + bool NextStateGeneratorOptions::isBuildAllRewardModelsSet() const { + return buildAllRewardModels; + } + + bool NextStateGeneratorOptions::isBuildAllLabelsSet() const { + return buildAllLabels; + } + NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildAllRewardModels() { + buildAllRewardModels = true; + return *this; + } + NextStateGeneratorOptions& NextStateGeneratorOptions::addRewardModel(std::string const& rewardModelName) { + STORM_LOG_THROW(!buildAllRewardModels, storm::exceptions::InvalidSettingsException, "Cannot add reward model, because all reward models are built anyway."); rewardModelNames.emplace_back(rewardModelName); return *this; } - + + NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildAllLabels() { + buildAllLabels = true; + return *this; + } + NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(storm::expressions::Expression const& expression) { expressionLabels.emplace_back(expression); return *this; } - NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(std::string const& label) { - labels.insert(label); + NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(std::string const& labelName) { + STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway."); + labelNames.insert(labelName); return *this; } diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index 1b9c7a374..a88285be8 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -48,7 +48,7 @@ namespace storm { /*! * Creates an object representing the default options. */ - NextStateGeneratorOptions(); + NextStateGeneratorOptions(bool buildAllRewardModels = false, bool buildAllLabels = false); /*! * Creates an object representing the suggested building options assuming that the given formula is the @@ -85,26 +85,37 @@ namespace storm { void setTerminalStatesFromFormula(storm::logic::Formula const& formula); std::vector const& getRewardModelNames() const; - std::set const& getLabels() const; + std::set const& getLabelNames() const; std::vector const& getExpressionLabels() const; std::vector> const& getTerminalStates() const; bool hasTerminalStates() const; void clearTerminalStates(); bool isBuildChoiceLabelsSet() const; + bool isBuildAllRewardModelsSet() const; + bool isBuildAllLabelsSet() const; + NextStateGeneratorOptions& setBuildAllRewardModels(); NextStateGeneratorOptions& addRewardModel(std::string const& rewardModelName); + NextStateGeneratorOptions& setBuildAllLabels(); NextStateGeneratorOptions& addLabel(storm::expressions::Expression const& expression); - NextStateGeneratorOptions& addLabel(std::string const& label); + NextStateGeneratorOptions& addLabel(std::string const& labelName); NextStateGeneratorOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); NextStateGeneratorOptions& addTerminalLabel(std::string const& label, bool value); NextStateGeneratorOptions& setBuildChoiceLabels(bool newValue); private: + /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are + /// to be ignored. + bool buildAllRewardModels; + /// The names of the reward models to generate. std::vector rewardModelNames; + /// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored. + bool buildAllLabels; + /// A set of labels to build. - std::set labels; + std::set labelNames; /// The expression that are to be used for creating the state labeling. std::vector expressionLabels; diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 1ec8c3243..30dc232fa 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -18,21 +18,27 @@ namespace storm { PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : NextStateGenerator(options), program(program), rewardModels(), variableInformation(program), evaluator(program.getManager()), state(nullptr), comparator() { STORM_LOG_THROW(!program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); - // Extract the reward models from the program based on the names we were given. - for (auto const& rewardModelName : this->options.getRewardModelNames()) { - 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 (this->options.isBuildAllRewardModelsSet()) { + for (auto const& rewardModel : program.getRewardModels()) { + rewardModels.push_back(rewardModel); + } + } else { + // Extract the reward models from the program based on the names we were given. + for (auto const& rewardModelName : this->options.getRewardModelNames()) { + 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 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. @@ -467,10 +473,16 @@ namespace storm { storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices) { // Gather a vector of labels and their expressions so we can iterate it over it a lot. std::vector> labels; - for (auto const& label : this->options.getLabels()) { - labels.push_back(std::make_pair(label, program.getLabelExpression(label))); + if (this->options.isBuildAllLabelsSet()) { + for (auto const& label : program.getLabels()) { + labels.push_back(std::make_pair(label.getName(), label.getStatePredicateExpression())); + } + } else { + for (auto const& labelName : this->options.getLabelNames()) { + labels.push_back(std::make_pair(labelName, program.getLabelExpression(labelName))); + } } - + // Make the labels unique. std::sort(labels.begin(), labels.end(), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; } ); auto it = std::unique(labels.begin(), labels.end(), [] (std::pair const& a, std::pair const& b) { return a.first == b.first; } ); diff --git a/src/utility/storm.h b/src/utility/storm.h index 0676cf1ef..3e7a5d992 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -121,7 +121,6 @@ namespace storm { } 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; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); - options.addConstantDefinitionsFromString(program, constantDefinitionString); storm::builder::DdPrismModelBuilder builder; result.model = builder.build(program, options);