diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 2ab4ee3e1..1aa2522fb 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -253,7 +253,7 @@ namespace storm { modernjson::json propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive); auto tbr = f.getTimeBoundReference(i); - if (tbr.isStepBound()) { + if (tbr.isStepBound() || (model.isDiscreteTimeModel() && tbr.isTimeBound())) { STORM_LOG_THROW(!hasStepBounds, storm::exceptions::NotSupportedException, "Jani export of until formulas with multiple step bounds is not supported."); hasStepBounds = true; opDecl["step-bounds"] = propertyInterval; @@ -268,7 +268,7 @@ namespace storm { rewbound["bounds"] = propertyInterval; rewardBounds.push_back(std::move(rewbound)); } else { - STORM_LOG_THROW(!hasTimeBounds, storm::exceptions::NotSupportedException, "Jani export of until formulas with multiple step bounds is not supported."); + STORM_LOG_THROW(!hasTimeBounds, storm::exceptions::NotSupportedException, "Jani export of until formulas with multiple time bounds is not supported."); hasTimeBounds = true; opDecl["time-bounds"] = propertyInterval; }