diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 0d415d388..f6d6251dd 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/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); } diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 42bc15d62..deb831ed1 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/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 accvec; - if (model.isDiscreteTimeModel()) { - accvec.push_back("steps"); - } else { + std::vector 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 accvec; + std::vector accvec = {"steps"}; std::string instantName; if (model.isDiscreteTimeModel()) { - accvec.push_back("steps"); instantName = "step-instant"; } else { accvec.push_back("time");