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 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 - JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator(model.getExpressionManager(), options), model(model), rewardExpressions(), hasStateActionRewards(false) { + JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator(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(this->model, this->parallelAutomata); this->transientVariableInformation.registerArrayVariableReplacements(arrayEliminatorData); - // Create a proper evalator. + // Create a proper evaluator. this->evaluator = std::make_unique>(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 choice(edge.getActionIndex(), static_cast(exitRate)); + std::vector stateActionRewards; // Perform the transient edge assignments and create the state action rewards TransientVariableValuation transientVariableValuation; - if (!edge.getAssignments().empty()) { + if (!evaluateRewardExpressionsAtEdges || edge.getAssignments().empty()) { + stateActionRewards.resize(rewardModelInformation.size(), storm::utility::zero()); + } 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 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 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 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);