Jani: export the correct accumulation parameters for expected reward properties

src/storm-parsers/parser/JaniParser.cpp

@@ -243,8 +243,7 @@ namespace storm {
                             }
                         }
                     }
-                    STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "Storm does not allow to accumulate over both time and steps");
-                    
+                    // TODO: handle accumulation parameters!
                     
                     if (propertyStructure.count("step-instant") > 0) {
                         STORM_LOG_THROW(propertyStructure.count("time-instant") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a time-instant in " + context);
@@ -303,7 +302,8 @@ namespace storm {
                                     STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "One may only accumulate either 'steps' or 'time', got " << accEntry.dump() << " in "  << context);
                                 }
                             }
-                            STORM_LOG_THROW((rewInstAccTime && !rewInstAccSteps) || (!rewInstAccTime && rewInstAccSteps), storm::exceptions::NotSupportedException, "Storm only allows to accumulate either over time or over steps in " + context);
+                            STORM_LOG_THROW(rewInstAccSteps || rewInstAccTime, storm::exceptions::NotSupportedException, "Storm only allows to accumulate either over time or over steps in " + context);
+                            // TODO: handle accumulation parameters
                             storm::expressions::Expression rewInstantExpr = parseExpression(rewInst.at("instant"), "reward instant in " + context, globalVars, constants);
                             bounds.emplace_back(false, rewInstantExpr);
                         }

src/storm/storage/jani/JSONExporter.cpp

@@ -209,10 +209,8 @@ namespace storm {
                 } else if(tbr.isRewardBound()) {
                     modernjson::json rewbound;
                     rewbound["exp"] = tbr.getRewardName();
-                    std::vector<std::string> accvec;
-                    if (model.isDiscreteTimeModel()) {
-                        accvec.push_back("steps");
-                    } else {
+                    std::vector<std::string> accvec = {"steps"};
+                    if (!model.isDiscreteTimeModel()) {
                         accvec.push_back("time");
                     }
                     rewbound["accumulate"] = modernjson::json(accvec);
@@ -403,10 +401,9 @@ namespace storm {
         
         boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const {
             modernjson::json opDecl;
-            std::vector<std::string> accvec;
+            std::vector<std::string> accvec = {"steps"};
             std::string instantName;
             if (model.isDiscreteTimeModel()) {
-                accvec.push_back("steps");
                 instantName = "step-instant";
             } else {
                 accvec.push_back("time");