From e3c0a49ed3f91a3e9f488a1d44b6fa87e864a5f8 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 8 Oct 2018 12:01:22 +0200 Subject: [PATCH] New RewardModelInformation now compiles... --- .../storage/jani/traverser/RewardModelInformation.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/storm/storage/jani/traverser/RewardModelInformation.cpp b/src/storm/storage/jani/traverser/RewardModelInformation.cpp index a89139f4f..908802742 100644 --- a/src/storm/storage/jani/traverser/RewardModelInformation.cpp +++ b/src/storm/storage/jani/traverser/RewardModelInformation.cpp @@ -3,6 +3,7 @@ #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/Variable.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" namespace storm { namespace jani { @@ -15,8 +16,8 @@ namespace storm { // Intentionally left empty } - RewardModelInformation::RewardModelInformation(Model const& model, storm::expressions::Expression const& rewardModelExpression) : stateRewards(false), actionRewards(false), transitionRewards(false), destinationDependendRewards(false) { - auto variablesInRewardExpression = rewardExpression.getVariables(); + RewardModelInformation::RewardModelInformation(Model const& model, storm::expressions::Expression const& rewardModelExpression) : stateRewards(false), actionRewards(false), transitionRewards(false) { + auto variablesInRewardExpression = rewardModelExpression.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."); @@ -25,7 +26,7 @@ namespace storm { initialSubstitution.emplace(v, janiVar.getInitExpression()); } } - auto initExpr = storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution); + auto initExpr = storm::jani::substituteJaniExpression(rewardModelExpression, initialSubstitution); if (initExpr.containsVariables() || !storm::utility::isZero(initExpr.evaluateAsRational())) { stateRewards = true; actionRewards = true; @@ -91,7 +92,7 @@ namespace storm { } bool RewardModelInformation::hasTransitionRewards () const { - return transitionReward; + return transitionRewards; }