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<Type> 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<typename ValueType, typename StateType>
- JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), VariableInformation(model), options), model(model) {
+ JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(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<storm::expressions::Variable> 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<storm::expressions::Variable, storm::expressions::Expression> 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.
*/