From 0a6122258c18f772ef763a3388efc3550d3e40ce Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 8 Oct 2018 10:06:29 +0200 Subject: [PATCH] Used the new reward information traverser wherever one needs to find out the reward kinds of a given rewardmodel --- .../generator/JaniNextStateGenerator.cpp | 42 ++++--------------- .../RewardAccumulationEliminationVisitor.cpp | 28 ++----------- .../RewardModelNameSubstitutionVisitor.cpp | 1 - src/storm/storage/jani/JSONExporter.cpp | 33 +++------------ 4 files changed, 16 insertions(+), 88 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index eeae4b4ad..0eaf8c480 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -15,7 +15,7 @@ #include "storm/storage/jani/CompositionInformationVisitor.h" #include "storm/storage/jani/traverser/AssignmentLevelFinder.h" #include "storm/storage/jani/traverser/ArrayExpressionFinder.h" -#include "storm/storage/jani/traverser/AssignmentsFinder.h" +#include "storm/storage/jani/traverser/RewardModelInformation.h" #include "storm/storage/sparse/JaniChoiceOrigins.h" @@ -949,41 +949,13 @@ namespace storm { template void JaniNextStateGenerator::buildRewardModelInformation() { - // Prepare all reward model information structs and get a mapping from variables to rewardModels that use this variable - std::map> variableToRewardIndices; - for (uint64_t i = 0; i < rewardExpressions.size(); ++i) { - rewardModelInformation.emplace_back(rewardExpressions[i].first, false, false, false); - auto varsInExpression = rewardExpressions[i].second.getVariables(); - for (auto const& v : varsInExpression) { - auto mapIt = variableToRewardIndices.emplace(v, std::vector()).first; - mapIt->second.push_back(i); - } - } - - storm::jani::AssignmentsFinder finder; - for (auto const& varRewIndices : variableToRewardIndices) { - auto assignmentsFinderResult = finder.find(this->model, varRewIndices.first); - if (assignmentsFinderResult.hasLocationAssignment) { - for (auto const& rewModelIndex : varRewIndices.second) { - rewardModelInformation[rewModelIndex].setHasStateRewards(); - } - } - if (assignmentsFinderResult.hasEdgeAssignment || (this->options.isScaleAndLiftTransitionRewardsSet() && assignmentsFinderResult.hasEdgeDestinationAssignment)) { - for (auto const& rewModelIndex : varRewIndices.second) { - rewardModelInformation[rewModelIndex].setHasStateActionRewards(); - hasStateActionRewards = true; - } - } - STORM_LOG_THROW(this->options.isScaleAndLiftTransitionRewardsSet() || !assignmentsFinderResult.hasEdgeDestinationAssignment, storm::exceptions::NotSupportedException, "Transition rewards are not supported and a reduction to action-based rewards was not possible."); - } - - // If the reward expression does not evaluate to zero, we set all reward types to true - for (uint64_t i = 0; i < rewardExpressions.size(); ++i) { - auto const& rewExpr = rewardExpressions[i].second; - if (rewExpr.containsVariables() || !storm::utility::isZero(this->evaluator->asRational(rewExpr))) { - rewardModelInformation[i].setHasStateRewards(); - rewardModelInformation[i].setHasStateActionRewards(); + for (auto const& rewardModel : rewardExpressions) { + 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.hasActionRewards() || (this->options.isScaleAndLiftTransitionRewardsSet() && info.hasTransitionRewards())) { hasStateActionRewards = true; + rewardModelInformation.back().setHasStateActionRewards(); } } } diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 11b99dabe..374e49f94 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -2,7 +2,7 @@ #include "storm/logic/Formulas.h" #include "storm/storage/jani/Model.h" -#include "storm/storage/jani/traverser/AssignmentsFinder.h" +#include "storm/storage/jani/traverser/RewardModelInformation.h" #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/utility/macros.h" @@ -128,32 +128,12 @@ namespace storm { bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional rewardModelName) const { STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable for unique reward model."); - storm::expressions::Expression rewardExpression = model.getRewardModelExpression(rewardModelName.get()); - bool hasStateRewards = false; - bool hasActionOrTransitionRewards = false; - auto variablesInRewardExpression = rewardExpression.getVariables(); - std::map initialSubstitution; - for (auto const& v : variablesInRewardExpression) { - STORM_LOG_ASSERT(model.hasGlobalVariable(v.getName()), "Unable to find global variable " << v.getName() << " occurring in a reward expression."); - auto const& janiVar = model.getGlobalVariable(v.getName()); - if (janiVar.hasInitExpression()) { - initialSubstitution.emplace(v, janiVar.getInitExpression()); - } - auto assignmentKinds = storm::jani::AssignmentsFinder().find(model, v); - hasActionOrTransitionRewards = hasActionOrTransitionRewards || assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment; - hasStateRewards = hasStateRewards || assignmentKinds.hasLocationAssignment; - } - rewardExpression = storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution); - if (rewardExpression.containsVariables() || !storm::utility::isZero(rewardExpression.evaluateAsRational())) { - hasStateRewards = true; - hasActionOrTransitionRewards = true; - } - + storm::jani::RewardModelInformation info(model, rewardModelName.get()); - if (hasActionOrTransitionRewards && !accumulation.isStepsSet()) { + if ((info.hasActionRewards() || info.hasTransitionRewards()) && !accumulation.isStepsSet()) { return false; } - if (hasStateRewards) { + if (info.hasStateRewards()) { if (model.isDiscreteTimeModel()) { if (!accumulation.isExitSet()) { return false; diff --git a/src/storm/logic/RewardModelNameSubstitutionVisitor.cpp b/src/storm/logic/RewardModelNameSubstitutionVisitor.cpp index 314e6c74d..11f5506a8 100644 --- a/src/storm/logic/RewardModelNameSubstitutionVisitor.cpp +++ b/src/storm/logic/RewardModelNameSubstitutionVisitor.cpp @@ -2,7 +2,6 @@ #include "storm/logic/Formulas.h" #include "storm/storage/jani/Model.h" -#include "storm/storage/jani/traverser/AssignmentsFinder.h" #include "storm/utility/macros.h" #include "storm/exceptions/UnexpectedException.h" diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index ca9bb2989..d5e43af93 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -30,7 +30,7 @@ #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/Property.h" -#include "storm/storage/jani/traverser/AssignmentsFinder.h" +#include "storm/storage/jani/traverser/RewardModelInformation.h" #include "storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.h" #include "storm/storage/jani/FunctionEliminator.h" #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" @@ -164,35 +164,12 @@ namespace storm { } modernjson::json FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const { - bool steps = false; - bool time = false; - bool exit = false; + storm::jani::RewardModelInformation info(model, rewardModelName); - auto rewardExpression = storm::jani::eliminateFunctionCallsInExpression(model.getRewardModelExpression(rewardModelName), model); + bool steps = rewardAccumulation.isStepsSet() && (info.hasActionRewards() || info.hasTransitionRewards()); + bool time = rewardAccumulation.isTimeSet() && !model.isDeterministicModel() && info.hasStateRewards(); + bool exit = rewardAccumulation.isExitSet() && info.hasStateRewards(); - auto variablesInRewardExpression = rewardExpression.getVariables(); - std::map initialSubstitution; - for (auto const& v : variablesInRewardExpression) { - STORM_LOG_ASSERT(model.hasGlobalVariable(v.getName()), "Unable to find global variable " << v.getName() << " occurring in a reward expression."); - auto const& janiVar = model.getGlobalVariable(v.getName()); - if (janiVar.hasInitExpression()) { - initialSubstitution.emplace(v, janiVar.getInitExpression()); - } - auto assignmentKinds = storm::jani::AssignmentsFinder().find(model, v); - steps = steps || assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment; - time = time || (!model.isDeterministicModel() && assignmentKinds.hasLocationAssignment); - exit = exit || assignmentKinds.hasLocationAssignment; - } - rewardExpression = storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution); - if (rewardExpression.containsVariables() || !storm::utility::isZero(rewardExpression.evaluateAsRational())) { - steps = true; - time = true; - exit = true; - } - - steps = steps && rewardAccumulation.isStepsSet(); - time = time && rewardAccumulation.isTimeSet(); - exit = exit && rewardAccumulation.isExitSet(); return constructRewardAccumulation(storm::logic::RewardAccumulation(steps, time, exit)); }