diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index 54ca1622f..336c1d299 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -21,8 +21,8 @@ namespace storm { // Intentionally left empty } - std::shared_ptr replaceBoundsByGreaterEqZero(std::shared_ptr const& boundedUntilOperator, std::set dimensionsToReplace) { - auto const& origBoundedUntil = boundedUntilOperator->getSubformula().asBoundedUntilFormula(); + std::shared_ptr replaceBoundsByGreaterEqZero(storm::logic::ProbabilityOperatorFormula const& boundedUntilOperator, std::set const& dimensionsToReplace) { + auto const& origBoundedUntil = boundedUntilOperator.getSubformula().asBoundedUntilFormula(); STORM_LOG_ASSERT(*(--dimensionsToReplace.end()) < origBoundedUntil.getDimension(), "Tried to replace the bound of a dimension that is higher than the number of dimensions of the formula."); std::vector> leftSubformulas, rightSubformulas; std::vector> lowerBounds, upperBounds; @@ -39,7 +39,7 @@ namespace storm { lowerBounds.push_back(boost::none); } if (origBoundedUntil.hasUpperBound()) { - upperBounds.emplace_back(origBoundedUntil.isUpperBoundStrict(dim), origBoundedUntil.getUpperBound(dim)); + lowerBounds.push_back(storm::logic::TimeBound(origBoundedUntil.isUpperBoundStrict(dim), origBoundedUntil.getUpperBound(dim))); } else { upperBounds.push_back(boost::none); } @@ -51,12 +51,12 @@ namespace storm { STORM_LOG_THROW(origBoundedUntil.hasUpperBound(dim), storm::exceptions::InvalidOperationException, "The given bounded until formula has no cost-bound for one dimension."); zero = origBoundedUntil.getUpperBound(dim).getManager().rational(0.0); } - lowerBounds.emplace_back(false, zero); + lowerBounds.push_back(storm::logic::TimeBound(false, zero)); upperBounds.push_back(boost::none); } } auto newBoundedUntil = std::make_shared(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences); - return std::make_shared(newBoundedUntil, boundedUntilOperator->getOperatorInformation()); + return std::make_shared(newBoundedUntil, boundedUntilOperator.getOperatorInformation()); } @@ -78,6 +78,7 @@ namespace storm { template bool QuantileHelper::computeUnboundedValue(Environment const& env) { + auto unboundedFormula = replaceBoundsByGreaterEqZero(quantileFormula.getSubformula().asProbabilityOperatorFormula(), std::set()); return false; }