|
@ -19,15 +19,19 @@ namespace storm { |
|
|
RewardModelInformation::RewardModelInformation(Model const& model, storm::expressions::Expression const& rewardModelExpression) : stateRewards(false), actionRewards(false), transitionRewards(false) { |
|
|
RewardModelInformation::RewardModelInformation(Model const& model, storm::expressions::Expression const& rewardModelExpression) : stateRewards(false), actionRewards(false), transitionRewards(false) { |
|
|
auto variablesInRewardExpression = rewardModelExpression.getVariables(); |
|
|
auto variablesInRewardExpression = rewardModelExpression.getVariables(); |
|
|
std::map<storm::expressions::Variable, storm::expressions::Expression> initialSubstitution; |
|
|
std::map<storm::expressions::Variable, storm::expressions::Expression> initialSubstitution; |
|
|
|
|
|
bool containsNonTransientVariable = false; |
|
|
for (auto const& v : variablesInRewardExpression) { |
|
|
for (auto const& v : variablesInRewardExpression) { |
|
|
STORM_LOG_ASSERT(model.hasGlobalVariable(v.getName()), "Unable to find global variable " << v.getName() << " occurring in a reward expression."); |
|
|
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()); |
|
|
auto const& janiVar = model.getGlobalVariable(v.getName()); |
|
|
if (janiVar.hasInitExpression()) { |
|
|
if (janiVar.hasInitExpression()) { |
|
|
initialSubstitution.emplace(v, janiVar.getInitExpression()); |
|
|
initialSubstitution.emplace(v, janiVar.getInitExpression()); |
|
|
} |
|
|
} |
|
|
|
|
|
if (!janiVar.isTransient()) { |
|
|
|
|
|
containsNonTransientVariable = true; |
|
|
|
|
|
} |
|
|
} |
|
|
} |
|
|
auto initExpr = storm::jani::substituteJaniExpression(rewardModelExpression, initialSubstitution); |
|
|
auto initExpr = storm::jani::substituteJaniExpression(rewardModelExpression, initialSubstitution); |
|
|
if (initExpr.containsVariables() || !storm::utility::isZero(initExpr.evaluateAsRational())) { |
|
|
|
|
|
|
|
|
if (containsNonTransientVariable || initExpr.containsVariables() || !storm::utility::isZero(initExpr.evaluateAsRational())) { |
|
|
stateRewards = true; |
|
|
stateRewards = true; |
|
|
actionRewards = true; |
|
|
actionRewards = true; |
|
|
transitionRewards = true; |
|
|
transitionRewards = true; |
|
|