From c8ea0f60dafa7ed5c67b13d85d7e4f66e097a348 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 28 May 2019 13:22:32 +0200
Subject: [PATCH] JaniBuilder: Fixed several issues that occurred with branch
reward expressions over non-transient variables, including GitHub issue #47
---
src/storm/builder/DdJaniModelBuilder.cpp | 5 +-
.../generator/JaniNextStateGenerator.cpp | 62 +++++++++++++------
src/storm/generator/JaniNextStateGenerator.h | 6 ++
src/storm/storage/jani/Model.cpp | 11 +++-
src/storm/storage/jani/Model.h | 16 ++++-
5 files changed, 74 insertions(+), 26 deletions(-)
diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index 699787ee8..27e1e586e 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -1975,13 +1975,13 @@ namespace storm {
std::vector<storm::expressions::Variable> rewardVariables;
if (options.isBuildAllRewardModelsSet()) {
for (auto const& rewExpr : model.getAllRewardModelExpressions()) {
- STORM_LOG_ERROR_COND(rewExpr.second.isVariable(), "The DD-builder can not build the non-trivial reward expression '" << rewExpr.second << "'.");
+ STORM_LOG_THROW(!model.isNonTrivialRewardModelExpression(rewExpr.first), storm::exceptions::NotSupportedException, "The DD-builder can not build the non-trivial reward expression '" << rewExpr.second << "'.");
rewardVariables.push_back(rewExpr.second.getBaseExpression().asVariableExpression().getVariable());
}
} else {
for (auto const& rewardModelName : options.getRewardModelNames()) {
+ STORM_LOG_THROW(!model.isNonTrivialRewardModelExpression(rewardModelName), storm::exceptions::NotSupportedException, "The DD-builder can not build the non-trivial reward expression '" << rewardModelName << "'.");
auto const& rewExpr = model.getRewardModelExpression(rewardModelName);
- STORM_LOG_ERROR_COND(rewExpr.isVariable(), "The DD-builder can not build the non-trivial reward expression '" << rewExpr << "'.");
rewardVariables.push_back(rewExpr.getBaseExpression().asVariableExpression().getVariable());
}
}
@@ -2070,6 +2070,7 @@ namespace storm {
// Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway).
if (preparedModel.hasTransientEdgeDestinationAssignments()) {
+ // This operation is correct as we are asserting that there are no assignment levels and no non-trivial reward expressions.
preparedModel.liftTransientEdgeDestinationAssignments();
}
diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index 185ebfa44..4f12d8d32 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -40,7 +40,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), options), model(model), rewardExpressions(), hasStateActionRewards(false) {
+ JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), options), model(model), rewardExpressions(), hasStateActionRewards(false), evaluateRewardExpressionsAtEdges(false), evaluateRewardExpressionsAtDestinations(false) {
STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
auto features = this->model.getModelFeatures();
@@ -54,11 +54,26 @@ namespace storm {
}
STORM_LOG_THROW(features.empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator does not support the following model feature(s): " << features.toString() << ".");
- // Preprocess the edge assignments:
- if (this->model.usesAssignmentLevels()) {
+ // Get the reward expressions to be build. Also find out whether there is a non-trivial one.
+ bool hasNonTrivialRewardExpressions = false;
+ if (this->options.isBuildAllRewardModelsSet()) {
+ rewardExpressions = this->model.getAllRewardModelExpressions();
+ hasNonTrivialRewardExpressions = this->model.hasNonTrivialRewardExpression();
+ } else {
+ // Extract the reward models from the model based on the names we were given.
+ for (auto const& rewardModelName : this->options.getRewardModelNames()) {
+ rewardExpressions.emplace_back(rewardModelName, this->model.getRewardModelExpression(rewardModelName));
+ hasNonTrivialRewardExpressions = hasNonTrivialRewardExpressions || this->model.isNonTrivialRewardModelExpression(rewardModelName);
+ }
+ }
+
+ // We try to lift the edge destination assignments to the edges as this reduces the number of evaluator calls.
+ // However, this will only be helpful if there are no assignment levels and only trivial reward expressions.
+ if (hasNonTrivialRewardExpressions || this->model.usesAssignmentLevels()) {
this->model.pushEdgeAssignmentsToDestinations();
} else {
this->model.liftTransientEdgeDestinationAssignments(storm::jani::AssignmentLevelFinder().getLowestAssignmentLevel(this->model));
+ evaluateRewardExpressionsAtEdges = true;
}
// Create all synchronization-related information, e.g. the automata that are put in parallel.
@@ -71,18 +86,10 @@ namespace storm {
this->transientVariableInformation = TransientVariableInformation<ValueType>(this->model, this->parallelAutomata);
this->transientVariableInformation.registerArrayVariableReplacements(arrayEliminatorData);
- // Create a proper evalator.
+ // Create a proper evaluator.
this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(this->model.getManager());
this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
- if (this->options.isBuildAllRewardModelsSet()) {
- rewardExpressions = this->model.getAllRewardModelExpressions();
- } else {
- // Extract the reward models from the model based on the names we were given.
- for (auto const& rewardModelName : this->options.getRewardModelNames()) {
- rewardExpressions.emplace_back(rewardModelName, this->model.getRewardModelExpression(rewardModelName));
- }
- }
// Build the information structs for the reward models.
buildRewardModelInformation();
@@ -541,18 +548,19 @@ namespace storm {
}
Choice<ValueType> choice(edge.getActionIndex(), static_cast<bool>(exitRate));
+ std::vector<ValueType> stateActionRewards;
// Perform the transient edge assignments and create the state action rewards
TransientVariableValuation<ValueType> transientVariableValuation;
- if (!edge.getAssignments().empty()) {
+ if (!evaluateRewardExpressionsAtEdges || edge.getAssignments().empty()) {
+ stateActionRewards.resize(rewardModelInformation.size(), storm::utility::zero<ValueType>());
+ } else {
for (int64_t assignmentLevel = edge.getAssignments().getLowestLevel(true); assignmentLevel <= edge.getAssignments().getHighestLevel(true); ++assignmentLevel) {
transientVariableValuation.clear();
applyTransientUpdate(transientVariableValuation, edge.getAssignments().getTransientAssignments(assignmentLevel), *this->evaluator);
transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet());
}
- }
- std::vector<ValueType> stateActionRewards = evaluateRewardExpressions();
- if (!edge.getAssignments().empty()) {
+ stateActionRewards = evaluateRewardExpressions();
transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
}
@@ -591,8 +599,11 @@ namespace storm {
}
}
}
-
- addEvaluatedRewardExpressions(stateActionRewards, probability);
+ if (evaluateRewardExpressionsAtDestinations) {
+ unpackStateIntoEvaluator(newState, this->variableInformation, *this->evaluator);
+ evaluatorChanged = true;
+ addEvaluatedRewardExpressions(stateActionRewards, probability);
+ }
if (evaluatorChanged) {
// Restore the old variable valuation
@@ -650,7 +661,7 @@ namespace storm {
// Perform the edge assignments (if there are any)
TransientVariableValuation<ValueType> transientVariableValuation;
- if (lowestEdgeAssignmentLevel <= highestEdgeAssignmentLevel) {
+ if (evaluateRewardExpressionsAtEdges && lowestEdgeAssignmentLevel <= highestEdgeAssignmentLevel) {
for (int64_t assignmentLevel = lowestEdgeAssignmentLevel; assignmentLevel <= highestEdgeAssignmentLevel; ++assignmentLevel) {
transientVariableValuation.clear();
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
@@ -718,7 +729,11 @@ namespace storm {
evaluatorChanged = true;
transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet());
}
- addEvaluatedRewardExpressions(stateActionRewards, successorProbability);
+ if (evaluateRewardExpressionsAtDestinations) {
+ unpackStateIntoEvaluator(successorState, this->variableInformation, *this->evaluator);
+ evaluatorChanged = true;
+ addEvaluatedRewardExpressions(stateActionRewards, successorProbability);
+ }
if (evaluatorChanged) {
// Restore the old state information
unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator);
@@ -977,11 +992,18 @@ namespace storm {
storm::jani::RewardModelInformation info(this->model, rewardModel.second);
rewardModelInformation.emplace_back(rewardModel.first, info.hasStateRewards(), false, false);
STORM_LOG_THROW(this->options.isScaleAndLiftTransitionRewardsSet() || !info.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are not supported and a reduction to action-based rewards was not possible.");
+ if (info.hasTransitionRewards()) {
+ evaluateRewardExpressionsAtDestinations = true;
+ }
if (info.hasActionRewards() || (this->options.isScaleAndLiftTransitionRewardsSet() && info.hasTransitionRewards())) {
hasStateActionRewards = true;
rewardModelInformation.back().setHasStateActionRewards();
}
}
+ if (!hasStateActionRewards) {
+ evaluateRewardExpressionsAtDestinations = false;
+ evaluateRewardExpressionsAtEdges = false;
+ }
}
template<typename ValueType, typename StateType>
diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h
index 350429944..a5bcb0450 100644
--- a/src/storm/generator/JaniNextStateGenerator.h
+++ b/src/storm/generator/JaniNextStateGenerator.h
@@ -167,6 +167,12 @@ namespace storm {
/// A flag that stores whether at least one of the selected reward models has state-action rewards.
bool hasStateActionRewards;
+ /// A flag that stores whether we shall evaluate reward expressions at edges
+ bool evaluateRewardExpressionsAtEdges;
+
+ /// A flag that stores whether we shall evaluate reward expressions at edge destinations
+ bool evaluateRewardExpressionsAtDestinations;
+
/// Data from eliminated array expressions. These are required to keep references to array variables in LValues alive.
storm::jani::ArrayEliminatorData arrayEliminatorData;
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 3aa05a20c..9d61a10cc 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -789,10 +789,19 @@ namespace storm {
return *expressionManager;
}
+ bool Model::hasNonTrivialRewardExpression() const {
+ return !nonTrivialRewardModels.empty();
+ }
+
+ bool Model::isNonTrivialRewardModelExpression(std::string const& identifier) const {
+ return nonTrivialRewardModels.count(identifier) > 0;
+ }
+
bool Model::addNonTrivialRewardExpression(std::string const& identifier, storm::expressions::Expression const& rewardExpression) {
- if (nonTrivialRewardModels.count(identifier) > 0) {
+ if (isNonTrivialRewardModelExpression(identifier)) {
return false;
} else {
+ STORM_LOG_THROW(!globalVariables.hasVariable(identifier) || !globalVariables.getVariable(identifier).isTransient(), storm::exceptions::InvalidArgumentException, "Non trivial reward expression with identifier '" << identifier << "' clashes with global transient variable of the same name.");
nonTrivialRewardModels.emplace(identifier, rewardExpression);
return true;
}
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index 5db1551d5..c96611940 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -285,9 +285,19 @@ namespace storm {
* Retrieves the manager responsible for the expressions in the JANI model.
*/
storm::expressions::ExpressionManager& getExpressionManager() const;
-
+
+ /*!
+ * Returns true iff there is a non-trivial reward model, i.e., a reward model that does not consist of a single, global, numerical, transient variable.
+ */
+ bool hasNonTrivialRewardExpression() const;
+
+ /*!
+ * Returns true iff the given identifier corresponds to a non-trivial reward expression i.e., a reward model that does not consist of a single, global, numerical, transient variable.
+ */
+ bool isNonTrivialRewardModelExpression(std::string const& identifier) const;
+
/*!
- * Adds a (non-trivial) reward model, i.e., a reward model that does not consist of a single, global, numerical variable.
+ * Adds a reward expression, i.e., a reward model that does not consist of a single, global, numerical, transient variable.
* @return true if a new reward model was added and false if a reward model with this identifier is already present in the model (in which case no reward model is added)
*/
bool addNonTrivialRewardExpression(std::string const& identifier, storm::expressions::Expression const& rewardExpression);
@@ -577,7 +587,7 @@ namespace storm {
bool undefinedConstantsAreGraphPreserving() const;
/*!
- * Lifts the common edge destination assignments to edge assignments.
+ * Lifts the common edge destination assignments of transient variables to edge assignments.
* @param maxLevel the maximum level of assignments that are to be lifted.
*/
void liftTransientEdgeDestinationAssignments(int64_t maxLevel = 0);