From 2a7e4a3c55705661f6329996535ec2d6ce9b14cd Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 12 Sep 2016 13:41:49 +0200 Subject: [PATCH] towards DD-based JANI rewards Former-commit-id: 36d6cfbca394e6973275ce26607276b3ccf8091b [formerly c9d50742926cad18333a8fdbf8f358f1acc85734] Former-commit-id: b8fe7376b328e1a485f38f7d70a46ca5ac5d6a48 --- src/builder/DdJaniModelBuilder.cpp | 78 ++++++++++++++++++++++-- src/builder/DdJaniModelBuilder.h | 10 +++ src/generator/JaniNextStateGenerator.cpp | 9 ++- 3 files changed, 91 insertions(+), 6 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index a2b837080..1a61b51c0 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -102,6 +102,16 @@ namespace storm { } } + template + std::set const& DdJaniModelBuilder::Options::getRewardModelNames() const { + return rewardModelsToBuild; + } + + template + bool DdJaniModelBuilder::Options::isBuildAllRewardModelsSet() const { + return buildAllRewardModels; + } + template struct CompositionVariables { CompositionVariables() : manager(std::make_shared>()), @@ -356,7 +366,7 @@ namespace storm { template class SystemComposer : public storm::jani::CompositionVisitor { public: - SystemComposer(storm::jani::Model const& model, CompositionVariables const& variables) : model(model), variables(variables) { + SystemComposer(storm::jani::Model const& model, CompositionVariables const& variables, std::vector const& transientVariables) : model(model), variables(variables), transientVariables(transientVariables) { // Intentionally left empty. } @@ -368,6 +378,9 @@ namespace storm { // The variable to use when building an automaton. CompositionVariables const& variables; + + // The transient variables to consider during system composition. + std::vector transientVariables; }; // This structure represents an edge destination. @@ -906,7 +919,7 @@ namespace storm { public: // This structure represents an edge. struct EdgeDd { - EdgeDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::set const& writtenGlobalVariables = {}) : guard(guard), transitions(transitions), writtenGlobalVariables(writtenGlobalVariables) { + EdgeDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::map> const& transientVariableAssignments = {}, std::set const& writtenGlobalVariables = {}) : guard(guard), transitions(transitions), transientVariableAssignments(transientVariableAssignments), writtenGlobalVariables(writtenGlobalVariables) { // Intentionally left empty. } @@ -916,6 +929,9 @@ namespace storm { // A DD that represents the transitions of this edge. storm::dd::Add transitions; + // A mapping from transient variables to the DDs representing their value assignments. + std::map> transientVariableAssignments; + // The set of global variables written by this edge. std::set writtenGlobalVariables; }; @@ -994,7 +1010,7 @@ namespace storm { }; - CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables) : SystemComposer(model, variables) { + CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables) { // Intentionally left empty. } @@ -1307,6 +1323,27 @@ namespace storm { transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); } + // Finally treat the transient assignments. + if (!this->transientVariables.empty()) { + auto transientAssignments = edge.getAssignments().getTransientAssignments(); + + auto transientVariableIt = this->transientVariables.begin(); + auto transientVariableIte = this->transientVariables.end(); + for (auto const& assignment : transientAssignments) { + while (transientVariableIt != transientVariableIte && *transientVariableIt < assignment.getExpressionVariable()) { +// callback(storm::utility::zero()); + ++transientVariableIt; + } + if (transientVariableIt == transientVariableIte) { + break; + } + if (*transientVariableIt == assignment.getExpressionVariable()) { +// callback(ValueType(this->evaluator.asRational(assignment.getAssignedExpression()))); + ++transientVariableIt; + } + } + } + return EdgeDd(guard, guard * transitions, globalVariablesInSomeDestination); } else { return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); @@ -1715,6 +1752,36 @@ namespace storm { return deadlockStates; } + template + std::vector selectRewardVariables(storm::jani::Model const& model, typename DdJaniModelBuilder::Options const& options) { + std::vector result; + if (options.isBuildAllRewardModelsSet()) { + for (auto const& variable : model.getGlobalVariables()) { + if (variable.isTransient()) { + result.push_back(variable.getExpressionVariable()); + } + } + } else { + auto const& globalVariables = model.getGlobalVariables(); + for (auto const& rewardModelName : options.getRewardModelNames()) { + if (globalVariables.hasVariable(rewardModelName)) { + result.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable()); + } else { + STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'."); + STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous."); + } + } + + // If no reward model was yet added, but there was one that was given in the options, we try to build the + // standard reward model. + if (result.empty() && !options.getRewardModelNames().empty()) { + result.push_back(globalVariables.getTransientVariables().front()->getExpressionVariable()); + } + } + + return result; + } + template std::shared_ptr> DdJaniModelBuilder::build(storm::jani::Model const& model, Options const& options) { if (model.hasUndefinedConstants()) { @@ -1732,9 +1799,12 @@ namespace storm { CompositionVariableCreator variableCreator(model); CompositionVariables variables = variableCreator.create(); + // Determine which transient assignments need to be considered in the building process. + std::vector rewardVariables = selectRewardVariables(model, options); + // Create a builder to compose and build the model. // SeparateEdgesSystemComposer composer(model, variables); - CombinedEdgesSystemComposer composer(model, variables); + CombinedEdgesSystemComposer composer(model, variables, rewardVariables); ComposerResult system = composer.compose(); // Postprocess the variables in place. diff --git a/src/builder/DdJaniModelBuilder.h b/src/builder/DdJaniModelBuilder.h index f1b16af1a..dd99f5fcb 100644 --- a/src/builder/DdJaniModelBuilder.h +++ b/src/builder/DdJaniModelBuilder.h @@ -59,6 +59,16 @@ namespace storm { */ void setTerminalStatesFromFormula(storm::logic::Formula const& formula); + /*! + * Retrieves the names of the reward models to build. + */ + std::set const& getRewardModelNames() const; + + /*! + * Retrieves whether the flag to build all reward models is set. + */ + bool isBuildAllRewardModelsSet() const; + // A flag that indicates whether or not all reward models are to be build. bool buildAllRewardModels; diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index c0ae75160..23a3a7068 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -34,9 +34,8 @@ namespace storm { } } } else { - auto const& globalVariables = model.getGlobalVariables(); - // Extract the reward models from the program based on the names we were given. + auto const& globalVariables = model.getGlobalVariables(); for (auto const& rewardModelName : this->options.getRewardModelNames()) { if (globalVariables.hasVariable(rewardModelName)) { rewardVariables.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable()); @@ -536,6 +535,12 @@ namespace storm { template void JaniNextStateGenerator::performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, std::function const& callback) { + // If there are no reward variables, there is no need to iterate at all. + if (rewardVariables.empty()) { + return; + } + + // Otherwise, perform the callback for all selected reward variables. auto rewardVariableIt = rewardVariables.begin(); auto rewardVariableIte = rewardVariables.end(); for (auto const& assignment : transientAssignments) {