From eed0a9889948a55712bb1189cd2e2e9f7e544445 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 7 Sep 2016 21:58:03 +0200 Subject: [PATCH] commit to switch workplace Former-commit-id: da2d6f8af30905171448c10ca352ed6f4630be61 [formerly f2157cac64652f329887fd114296904b9fbee9f7] Former-commit-id: 1b7b4b649664dbbb6653e122fb868fdcaad6d664 --- src/builder/DdJaniModelBuilder.cpp | 4 +-- src/generator/JaniNextStateGenerator.cpp | 32 ++++++++++++++++++++++-- src/generator/JaniNextStateGenerator.h | 4 +++ src/parser/JaniParser.cpp | 2 +- src/storage/jani/Assignment.cpp | 2 +- src/storage/jani/Automaton.cpp | 4 +++ src/storage/jani/Automaton.h | 5 ++++ src/storage/jani/Model.cpp | 17 +++++++++++++ src/storage/jani/Model.h | 15 +++++++++++ src/storage/jani/Variable.cpp | 2 +- src/storage/jani/Variable.h | 2 +- src/storage/jani/VariableSet.cpp | 11 +++++++- src/storage/jani/VariableSet.h | 5 ++++ 13 files changed, 96 insertions(+), 9 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 4909245fa..f62afa00f 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -261,7 +261,7 @@ namespace storm { storm::dd::Bdd globalVariableRanges = result.manager->getBddOne(); for (auto const& variable : this->model.getGlobalVariables()) { // Only create the variable if it's non-transient. - if (variable.isTransientVariable()) { + if (variable.isTransient()) { continue; } @@ -284,7 +284,7 @@ namespace storm { // Then create variables for the variables of the automaton. for (auto const& variable : automaton.getVariables()) { // Only create the variable if it's non-transient. - if (variable.isTransientVariable()) { + if (variable.isTransient()) { continue; } diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index ba76f4e86..f6dbfa618 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -11,6 +11,7 @@ #include "src/utility/solver.h" #include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/WrongFormatException.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace generator { @@ -21,11 +22,38 @@ namespace storm { } template - JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(model.getExpressionManager(), VariableInformation(model), options), model(model) { + JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(model.getExpressionManager(), VariableInformation(model), options), model(model), rewardVariables() { STORM_LOG_THROW(model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); - STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models."); + STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables."); STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); + if (this->options.isBuildAllRewardModelsSet()) { + for (auto const& variable : model.getGlobalVariables()) { + if (variable.isTransient()) { + rewardVariables.push_back(variable.getExpressionVariable()); + } + } + } else { + // Extract the reward models from the program based on the names we were given. + for (auto const& rewardModelName : this->options.getRewardModelNames()) { + auto const& globalVariables = model.getGlobalVariables(); + if (globalVariables.hasVariable(rewardModelName)) { + rewardVariables.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."); + STORM_LOG_THROW(this->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(this->program.getRewardModel(0)); + } + } + + // If there are terminal states we need to handle, we now need to translate all labels to expressions. if (this->options.hasTerminalStates()) { for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h index 316d6e074..be6033ebc 100644 --- a/src/generator/JaniNextStateGenerator.h +++ b/src/generator/JaniNextStateGenerator.h @@ -91,6 +91,10 @@ namespace storm { /// The model used for the generation of next states. storm::jani::Model model; + + // The transient variables of reward models that need to be considered. + std::vector rewardVariables; + }; } diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 806a26a1f..b4d67fce2 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -571,7 +571,7 @@ namespace storm { STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to"); STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value"); storm::jani::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')"); - STORM_LOG_THROW(lhs.isTransientVariable(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); + STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); transientAssignments.emplace_back(lhs, rhs); } diff --git a/src/storage/jani/Assignment.cpp b/src/storage/jani/Assignment.cpp index 559fc685b..0e1720a8d 100644 --- a/src/storage/jani/Assignment.cpp +++ b/src/storage/jani/Assignment.cpp @@ -28,7 +28,7 @@ namespace storm { } bool Assignment::isTransientAssignment() const { - return this->variable.get().isTransientVariable(); + return this->variable.get().isTransient(); } void Assignment::substitute(std::map const& substitution) { diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 1a38adea8..9e288695f 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -97,6 +97,10 @@ namespace storm { return variables; } + bool Automaton::hasTransientVariable() const { + return variables.hasTransientVariable(); + } + bool Automaton::hasLocation(std::string const& name) const { return locationToIndex.find(name) != locationToIndex.end(); } diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index d023fa36c..9ef3c57f2 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -135,6 +135,11 @@ namespace storm { */ VariableSet const& getVariables() const; + /*! + * Retrieves whether this automaton has a transient variable. + */ + bool hasTransientVariable() const; + /*! * Retrieves whether the automaton has a location with the given name. */ diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 9d0dcb7d0..0bec35317 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -143,6 +143,23 @@ namespace storm { return globalVariables; } + bool Model::hasGlobalVariable(std::string const& name) const { + return globalVariables.hasVariable(name); + } + + Variable const& Model::getGlobalVariable(std::string const& name) const { + return globalVariables.getVariable(name); + } + + bool Model::hasNonGlobalTransientVariable() const { + for (auto const& automaton : automata) { + if (automaton.hasTransientVariable()) { + return true; + } + } + return false; + } + storm::expressions::ExpressionManager& Model::getExpressionManager() { return *expressionManager; } diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 20ca41486..946871cc5 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -141,6 +141,21 @@ namespace storm { * Retrieves the variables of this automaton. */ VariableSet const& getGlobalVariables() const; + + /*! + * Retrieves whether this model has a global variable with the given name. + */ + bool hasGlobalVariable(std::string const& name) const; + + /*! + * Retrieves the global variable with the given name if one exists. + */ + Variable const& getGlobalVariable(std::string const& name) const; + + /*! + * Retrieves whether this model has a non-global transient variable. + */ + bool hasNonGlobalTransientVariable() const; /*! * Retrieves the manager responsible for the expressions in the JANI model. diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp index 763179013..9280b7c8e 100644 --- a/src/storage/jani/Variable.cpp +++ b/src/storage/jani/Variable.cpp @@ -40,7 +40,7 @@ namespace storm { return false; } - bool Variable::isTransientVariable() const { + bool Variable::isTransient() const { return transient; } diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h index fa56e0a8d..1add2768b 100644 --- a/src/storage/jani/Variable.h +++ b/src/storage/jani/Variable.h @@ -61,7 +61,7 @@ namespace storm { virtual bool isUnboundedIntegerVariable() const; virtual bool isRealVariable() const; - virtual bool isTransientVariable() const; + virtual bool isTransient() const; // Methods to get the variable as a different type. BooleanVariable& asBooleanVariable(); diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp index 7b304e68d..c138686e8 100644 --- a/src/storage/jani/VariableSet.cpp +++ b/src/storage/jani/VariableSet.cpp @@ -158,6 +158,15 @@ namespace storm { return variableToVariable.find(variable) != variableToVariable.end(); } + bool VariableSet::hasTransientVariable() const { + for (auto const& variable : variables) { + if (variable->isTransient()) { + return true; + } + } + return false; + } + bool VariableSet::containsBooleanVariable() const { return !booleanVariables.empty(); } @@ -176,7 +185,7 @@ namespace storm { bool VariableSet::containsNonTransientRealVariables() const { for (auto const& variable : realVariables) { - if (!variable->isTransientVariable()) { + if (!variable->isTransient()) { std::cout << "var " << variable->getName() << "is non-transient " << std::endl; return true; } diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h index 4156faec1..777292ba9 100644 --- a/src/storage/jani/VariableSet.h +++ b/src/storage/jani/VariableSet.h @@ -148,6 +148,11 @@ namespace storm { */ Variable const& getVariable(storm::expressions::Variable const& variable) const; + /*! + * Retrieves whether this variable set contains a transient variable. + */ + bool hasTransientVariable() const; + /*! * Retrieves an iterator to the variables in this set. */