correct treatment of non-trivial reward expressions

src/storm-parsers/parser/JaniParser.cpp

@@ -205,7 +205,11 @@ namespace storm {
                 STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array");
                 for(auto const& propertyEntry : parsedStructure.at("properties")) {
                     try {
+                        nonTrivialRewardModelExpressions.clear();
                         auto prop = this->parseProperty(propertyEntry, scope.refine("property[" + std::to_string(properties.size()) + "]"));
+                        for (auto const& nonTrivRewExpr : nonTrivialRewardModelExpressions) {
+                            model.addNonTrivialRewardExpression(nonTrivRewExpr.first, nonTrivRewExpr.second);
+                        }
                         // Eliminate reward accumulations as much as possible
                         rewAccEliminator.eliminateRewardAccumulations(prop);
                         properties.push_back(prop);
@@ -321,7 +325,10 @@ namespace storm {
                         STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a reward-instant in " + scope.description);
 
                         storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), scope.refine("Step instant"));
-                        if(rewardAccumulation.isEmpty()) {
+                        if (!rewExpr.isVariable()) {
+                            nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
+                        }
+                        if (rewardAccumulation.isEmpty()) {
                              return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(stepInstantExpr, storm::logic::TimeBoundType::Steps), rewardName, opInfo);
                         } else {
                             return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps), rewardAccumulation), rewardName, opInfo);
@@ -329,7 +336,10 @@ namespace storm {
                     } else if (propertyStructure.count("time-instant") > 0) {
                         STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a time-instant and a reward-instant in " + scope.description);
                         storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), scope.refine("time instant"));
-                        if(rewardAccumulation.isEmpty()) {
+                        if (!rewExpr.isVariable()) {
+                            nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
+                        }
+                        if (rewardAccumulation.isEmpty()) {
                             return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(timeInstantExpr, storm::logic::TimeBoundType::Time), rewardName, opInfo);
                         } else {
                             return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time), rewardAccumulation), rewardName, opInfo);
@@ -349,6 +359,9 @@ namespace storm {
                             storm::expressions::Expression rewInstantExpr = parseExpression(rewInst.at("instant"), scope.refine("reward instant"));
                             bounds.emplace_back(false, rewInstantExpr);
                         }
+                        if (!rewExpr.isVariable()) {
+                            nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
+                        }
                         return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(bounds, boundReferences, rewardAccumulation), rewardName, opInfo);
                     } else {
                         time = !rewExpr.containsVariables() && storm::utility::isOne(rewExpr.evaluateAsRational());
@@ -363,11 +376,11 @@ namespace storm {
                             assert(subformula->isTotalRewardFormula() || subformula->isTimePathFormula());
                             return std::make_shared<storm::logic::TimeOperatorFormula>(subformula, opInfo);
                         } else {
-                            return std::make_shared<storm::logic::RewardOperatorFormula>(subformula, rewardName, opInfo);
+                            if (!rewExpr.isVariable()) {
+                                nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
                             }
+                            return std::make_shared<storm::logic::RewardOperatorFormula>(subformula, rewardName, opInfo);
                         }
-                    if (!time && !rewExpr.isVariable()) {
-                        nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
                     }
                 } else if (opString == "Smin" || opString == "Smax") {
                     STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported");
@@ -1403,6 +1416,7 @@ namespace storm {
                     STORM_LOG_THROW(edgeEntry.at("rate").count("exp") == 1, storm::exceptions::InvalidJaniException, "Rate in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a defing expression.");
                     rateExpr = parseExpression(edgeEntry.at("rate").at("exp"), scope.refine("rate expression in edge from '" + sourceLoc));
                     STORM_LOG_THROW(rateExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Rate '" << rateExpr << "' has not a numerical type");
+                    STORM_LOG_THROW(rateExpr.containsVariables() || rateExpr.evaluateAsRational() > storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidJaniException, "Only positive rates are allowed but rate '" << rateExpr << " was found.");
                 }
                 // guard
                 STORM_LOG_THROW(edgeEntry.count("guard") <= 1, storm::exceptions::InvalidJaniException, "Guard can be given at most once in edge from '" << sourceLoc << "' in automaton '" << name << "'");

src/storm/logic/RewardAccumulationEliminationVisitor.cpp

@@ -3,6 +3,7 @@
 
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/jani/traverser/AssignmentsFinder.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 #include "storm/utility/macros.h"
 
 #include "storm/exceptions/UnexpectedException.h"
@@ -126,20 +127,33 @@ namespace storm {
         }
         
         bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const {
-            STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with for unique reward model.");
-            storm::jani::AssignmentsFinder::ResultType assignmentKinds;
-            STORM_LOG_THROW(model.hasGlobalVariable(rewardModelName.get()), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with name " << rewardModelName.get() << ".");
-            storm::jani::Variable const& transientVar = model.getGlobalVariable(rewardModelName.get());
-            if (transientVar.getInitExpression().containsVariables() || !storm::utility::isZero(transientVar.getInitExpression().evaluateAsRational())) {
-                assignmentKinds.hasLocationAssignment = true;
-                assignmentKinds.hasEdgeAssignment = true;
-                assignmentKinds.hasEdgeDestinationAssignment = true;
-            }
-            assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar);
-            if ((assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment) && !accumulation.isStepsSet()) {
+            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<storm::expressions::Variable, storm::expressions::Expression> 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;
+            }
+            
+            
+            if (hasActionOrTransitionRewards && !accumulation.isStepsSet()) {
                 return false;
             }
-            if (assignmentKinds.hasLocationAssignment) {
+            if (hasStateRewards) {
                 if (model.isDiscreteTimeModel()) {
                     if (!accumulation.isExitSet()) {
                         return false;

src/storm/storage/jani/JSONExporter.cpp

@@ -183,7 +183,7 @@ namespace storm {
                 time = time || (!model.isDeterministicModel() && assignmentKinds.hasLocationAssignment);
                 exit = exit || assignmentKinds.hasLocationAssignment;
             }
-            storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution);
+            rewardExpression = storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution);
             if (rewardExpression.containsVariables() || !storm::utility::isZero(rewardExpression.evaluateAsRational())) {
                 steps = true;
                 time = true;