Browse Source

storm-conv: Fixed wrong jani export of step-bounded until properties in discrete time models.

tempestpy_adaptions
TimQu 6 years ago
parent
commit
fa2bcbd71b
  1. 4
      src/storm/storage/jani/JSONExporter.cpp

4
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;
}

Loading…
Cancel
Save