124 if (existsSat && getInstantiationCheckerSAT()
125 .check(env, valuationToCheckSat)
126 ->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
127 STORM_LOG_INFO(
"Region " << region <<
" is AllSat, discovered with instantiation checker on " << valuationToCheckSat
128 <<
" and help of monotonicity\n");
133 if (existsViolated && !getInstantiationCheckerVIO()
134 .check(env, valuationToCheckViolated)
135 ->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
136 STORM_LOG_INFO(
"Region " << region <<
" is AllViolated, discovered with instantiation checker on " << valuationToCheckViolated
137 <<
" and help of monotonicity\n");
150 ? storm::solver::OptimizationDirection::Minimize
151 : storm::solver::OptimizationDirection::Maximize;
152 auto checkResult = this->
check(env, region, parameterOptimizationDirection, localMonotonicityResult);
153 if (checkResult->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
155 }
else if (sampleVerticesOfRegion) {
156 result = sampleVertices(env, region, result);
158 }
else if (existsViolated) {
161 ? storm::solver::OptimizationDirection::Maximize
162 : storm::solver::OptimizationDirection::Minimize;
163 auto checkResult = this->
check(env, region, parameterOptimizationDirection, localMonotonicityResult);
164 if (!checkResult->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
166 }
else if (sampleVerticesOfRegion) {
167 result = sampleVertices(env, region, result);
170 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"When analyzing a region, an invalid initial result was given: " << initialResult);
175template<
typename SparseModelType,
typename ConstantType>
189 auto vertexIt = vertices.begin();
190 while (vertexIt != vertices.end() && !(hasSatPoint && hasViolatedPoint)) {
191 if (getInstantiationChecker().check(env, *vertexIt)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
194 hasViolatedPoint =
true;
200 if (hasViolatedPoint) {
212template<
typename SparseModelType,
typename ConstantType>
217 localMonotonicityResult) {
218 auto quantitativeResult = computeQuantitativeValues(env, region, dirForParameters, localMonotonicityResult);
219 lastValue = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
220 if (currentCheckTask->getFormula().hasQuantitativeResult()) {
221 return quantitativeResult;
223 return quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(
224 this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(),
225 this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
229template<
typename SparseModelType,
typename ConstantType>
234 localMonotonicityResult) {
235 STORM_LOG_WARN_COND(this->currentCheckTask->getFormula().hasQuantitativeResult(),
"Computing quantitative bounds for a qualitative formula...");
236 return std::make_unique<ExplicitQuantitativeCheckResult<ConstantType>>(std::move(
237 computeQuantitativeValues(env, region, dirForParameters, localMonotonicityResult)->
template asExplicitQuantitativeCheckResult<ConstantType>()));
240template<
typename SparseModelType,
typename ConstantType>
244 STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException,
245 "Getting a bound at the initial state requires a model with a single initial state.");
246 return storm::utility::convertNumber<typename SparseModelType::ValueType>(
247 getBound(env, region, dirForParameters)
248 ->
template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()]);
251template<
typename SparseModelType,
typename ConstantType>
254 return getInstantiationChecker();
257template<
typename SparseModelType,
typename ConstantType>
260 return getInstantiationChecker();
263template<
typename SparseModelType,
typename ConstantType>
271 std::shared_ptr<storm::analysis::Order>
order;
272 std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>>
localMonRes;
273 boost::optional<ConstantType>
bound;
276template<
typename SparseModelType,
typename ConstantType>
277std::pair<ConstantType, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation>
280 typename SparseModelType::ValueType
const& precision,
bool absolutePrecision, boost::optional<ConstantType>
const& initialValue,
281 std::optional<storm::logic::Bound>
const& terminationBound) {
284 STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException,
285 "Getting extremal values at the initial state requires a model with a single initial state.");
286 STORM_LOG_THROW(!this->currentCheckTask->isBoundSet(), storm::exceptions::NotSupportedException,
287 "Computing extremal values with parameter lifting requires no bound on the operator.");
288 bool const useMonotonicity = this->isUseMonotonicitySet();
294 : [](RegionBound<SparseModelType, ConstantType>
const& lhs, RegionBound<SparseModelType, ConstantType>
const& rhs) {
295 return lhs.
bound < rhs.bound;
297 std::priority_queue<RegionBound<SparseModelType, ConstantType>, std::vector<RegionBound<SparseModelType, ConstantType>>,
decltype(cmp)> regionQueue(cmp);
301 auto numberOfPLACallsBounds = 0;
302 boost::optional<ConstantType> initBound;
303 if (useMonotonicity) {
304 if (this->isUseBoundsSet()) {
305 numberOfPLACallsBounds++;
306 numberOfPLACallsBounds++;
307 auto minBound = getBound(env, region, storm::solver::OptimizationDirection::Minimize,
nullptr)
308 ->template asExplicitQuantitativeCheckResult<ConstantType>()
310 auto maxBound = getBound(env, region, storm::solver::OptimizationDirection::Maximize,
nullptr)
311 ->template asExplicitQuantitativeCheckResult<ConstantType>()
314 initBound = minBound[*this->parametricModel->getInitialStates().begin()];
316 initBound = maxBound[*this->parametricModel->getInitialStates().begin()];
318 orderExtender->setMinValuesInit(minBound);
319 orderExtender->setMaxValuesInit(maxBound);
321 auto order = this->extendOrder(
nullptr, region);
322 auto monRes = std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>>(
325 this->extendLocalMonotonicityResult(region, order, monRes);
326 monotonicityWatch.stop();
327 STORM_LOG_INFO(
"\nTotal time for monotonicity checking: " << monotonicityWatch <<
".\n\n");
329 regionQueue.emplace(region, order, monRes, initBound);
331 regionQueue.emplace(region,
nullptr,
nullptr, initBound);
335 boost::optional<ConstantType> value;
338 auto init = getGoodInitialPoint(env, region, dir, regionQueue.top().localMonRes);
339 value = storm::utility::convertNumber<ConstantType>(init.first);
340 valuation = std::move(init.second);
342 value = initialValue;
346 STORM_LOG_INFO(
"\nTotal time for initial points: " << initialWatch <<
".\n\n");
348 STORM_LOG_INFO(
"Initial value: " << value.get() <<
" at " << valuation);
350 STORM_LOG_INFO(
"Initial value: " << value.get() <<
" as provided by the user");
353 if (terminationBound != std::nullopt && !terminationBound.value().isSatisfied(value.get())) {
354 return std::make_pair(storm::utility::convertNumber<ConstantType>(value.get()), valuation);
357 auto numberOfSplits = 0;
358 auto numberOfPLACalls = 0;
359 auto numberOfOrderCopies = 0;
360 auto numberOfMonResCopies = 0;
362 if (!(useMonotonicity && regionQueue.top().localMonRes->getGlobalMonotonicityResult()->isDone() &&
363 regionQueue.top().localMonRes->getGlobalMonotonicityResult()->isAllMonotonicity())) {
365 auto totalArea = storm::utility::convertNumber<ConstantType>(region.
area());
366 auto coveredArea = storm::utility::zero<ConstantType>();
367 while (!regionQueue.empty()) {
369 auto currRegion = regionQueue.top().region;
370 auto order = regionQueue.top().order;
371 auto localMonotonicityResult = regionQueue.top().localMonRes;
372 auto currBound = regionQueue.top().bound;
375 std::vector<storm::storage::ParameterRegion<typename SparseModelType::ValueType>> newRegions;
378 bool investigateBounds = !currBound;
380 if (!investigateBounds && absolutePrecision) {
381 investigateBounds = (
minimize && currBound.get() < value.get() - storm::utility::convertNumber<ConstantType>(precision)) ||
382 (!minimize && currBound.get() > value.get() + storm::utility::convertNumber<ConstantType>(precision));
383 }
else if (!investigateBounds && !absolutePrecision) {
384 investigateBounds = (
minimize && (currBound.get() * (1 + storm::utility::convertNumber<ConstantType>(precision)) < value.get())) ||
385 (!
minimize && (currBound.get() * (1 - storm::utility::convertNumber<ConstantType>(precision)) > value.get()));
388 if (investigateBounds) {
391 getBound(env, currRegion, dir, localMonotonicityResult)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
393 currBound = bounds[*this->parametricModel->getInitialStates().begin()];
396 if (absolutePrecision) {
397 lookAtRegion = (
minimize && currBound.get() < value.get() - storm::utility::convertNumber<ConstantType>(precision)) ||
398 (!minimize && currBound.get() > value.get() + storm::utility::convertNumber<ConstantType>(precision));
400 lookAtRegion = (
minimize && (currBound.get() * (1 + storm::utility::convertNumber<ConstantType>(precision)) < value.get())) ||
401 (!
minimize && (currBound.get() * (1 - storm::utility::convertNumber<ConstantType>(precision)) > value.get()));
404 if (useMonotonicity) {
406 bool changedOrder =
false;
407 if (!order->getDoneBuilding() && orderExtender->isHope(order)) {
408 if (numberOfCopiesOrder[order] != 1) {
409 numberOfCopiesOrder[order]--;
410 order = copyOrder(order);
411 numberOfOrderCopies++;
413 assert(numberOfCopiesOrder[order] == 1);
415 this->extendOrder(order, currRegion);
419 assert(!localMonotonicityResult->isDone());
421 if (numberOfCopiesMonRes[localMonotonicityResult] != 1) {
422 numberOfCopiesMonRes[localMonotonicityResult]--;
423 localMonotonicityResult = localMonotonicityResult->copy();
424 numberOfMonResCopies++;
426 assert(numberOfCopiesMonRes[localMonotonicityResult] == 1);
428 this->extendLocalMonotonicityResult(currRegion, order, localMonotonicityResult);
435 useMonotonicity ? currRegion.getPoint(dir, *(localMonotonicityResult->getGlobalMonotonicityResult())) : currRegion.getCenterPoint();
436 auto currValue = getInstantiationChecker()
438 ->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
439 if (!value || (minimize ? currValue <= value.get() : currValue >= value.get())) {
442 if (terminationBound != std::nullopt && !terminationBound.value().isSatisfied(value.get())) {
443 return std::make_pair(storm::utility::convertNumber<ConstantType>(value.get()), valuation);
448 if (absolutePrecision) {
449 splitRegion = (
minimize && currBound.get() < value.get() - storm::utility::convertNumber<ConstantType>(precision)) ||
450 (!minimize && currBound.get() > value.get() + storm::utility::convertNumber<ConstantType>(precision));
452 splitRegion = (
minimize && (currBound.get() * (1 + storm::utility::convertNumber<ConstantType>(precision)) < value.get())) ||
453 (!
minimize && (currBound.get() * (1 - storm::utility::convertNumber<ConstantType>(precision)) > value.get()));
457 if (useMonotonicity && this->isUseBoundsSet() && !order->getDoneBuilding()) {
459 numberOfPLACallsBounds++;
461 orderExtender->setMinMaxValues(
463 getBound(env, currRegion, storm::solver::OptimizationDirection::Maximize, localMonotonicityResult)
464 ->template asExplicitQuantitativeCheckResult<ConstantType>()
467 orderExtender->setMinMaxValues(
469 getBound(env, currRegion, storm::solver::OptimizationDirection::Maximize, localMonotonicityResult)
470 ->template asExplicitQuantitativeCheckResult<ConstantType>()
477 if (useMonotonicity) {
478 this->splitSmart(currRegion, newRegions, *(localMonotonicityResult->getGlobalMonotonicityResult()),
true);
479 }
else if (this->isRegionSplitEstimateSupported()) {
481 this->splitSmart(currRegion, newRegions, empty,
true);
483 currRegion.split(currRegion.getCenterPoint(), newRegions);
489 if (newRegions.empty()) {
491 coveredArea += storm::utility::convertNumber<ConstantType>(currRegion.area());
492 if (order !=
nullptr) {
493 numberOfCopiesOrder[order]--;
494 numberOfCopiesMonRes[localMonotonicityResult]--;
499 STORM_LOG_INFO(
"Splitting region " << currRegion <<
" into " << newRegions.size());
502 if (useMonotonicity) {
503 for (
auto& r : newRegions) {
504 r.setBoundParent(storm::utility::convertNumber<CoefficientType>(currBound.get()));
505 regionQueue.emplace(r, order, localMonotonicityResult, currBound.get());
507 if (numberOfCopiesOrder.find(order) != numberOfCopiesOrder.end()) {
508 numberOfCopiesOrder[order] += newRegions.size();
509 numberOfCopiesMonRes[localMonotonicityResult] += newRegions.size();
511 numberOfCopiesOrder[order] = newRegions.size();
512 numberOfCopiesMonRes[localMonotonicityResult] = newRegions.size();
515 for (
auto& r : newRegions) {
516 r.setBoundParent(storm::utility::convertNumber<CoefficientType>(currBound.get()));
517 regionQueue.emplace(r,
nullptr,
nullptr, currBound.get());
522 STORM_LOG_INFO(
"Covered " << (coveredArea * storm::utility::convertNumber<ConstantType>(100.0) / totalArea) <<
"% of the region.\n");
523 STORM_LOG_INFO(
"Best value: " << value.get() <<
". Regions queued: " << regionQueue.size() <<
"\n");
528 STORM_LOG_INFO(
"Total number of splits: " << numberOfSplits <<
'\n');
529 STORM_LOG_INFO(
"Total number of pla calls: " << numberOfPLACalls <<
'\n');
530 if (useMonotonicity) {
531 STORM_LOG_INFO(
"Total number of pla calls for bounds for monotonicity checking: " << numberOfPLACallsBounds <<
'\n');
532 STORM_LOG_INFO(
"Total number of copies of the order: " << numberOfOrderCopies <<
'\n');
533 STORM_LOG_INFO(
"Total number of copies of the local monotonicity result: " << numberOfMonResCopies <<
'\n');
535 STORM_LOG_INFO(
"\nTotal time for region refinement: " << loopWatch <<
".\n\n");
536 STORM_LOG_INFO(
"\nTotal time for additional bounds: " << boundsWatch <<
".\n\n");
538 return std::make_pair(storm::utility::convertNumber<ConstantType>(value.get()), valuation);
541template<
typename SparseModelType,
typename ConstantType>
542std::pair<typename SparseModelType::ValueType, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation>
545 typename SparseModelType::ValueType
const& precision,
bool absolutePrecision, std::optional<storm::logic::Bound>
const& terminationBound) {
546 auto res = computeExtremalValue(env, region, dir, precision, absolutePrecision, boost::none, terminationBound);
547 return {storm::utility::convertNumber<typename SparseModelType::ValueType>(res.first), res.second};
550template<
typename SparseModelType,
typename ConstantType>
557 isLowerBound(bound.
comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
559 auto res = computeExtremalValue(env, region, dir, storm::utility::zero<typename SparseModelType::ValueType>(),
false, boost::none, bound).first;
563 : storm::utility::convertNumber<ConstantType>(res) <= valueToCheck;
566template<
typename SparseModelType,
typename ConstantType>
568 return *parametricModel;
571template<
typename SparseModelType,
typename ConstantType>
573 return *currentCheckTask;
576template<
typename SparseModelType,
typename ConstantType>
579 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Parameter lifting is not supported for the given property.");
582template<
typename SparseModelType,
typename ConstantType>
585 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Parameter lifting is not supported for the given property.");
588template<
typename SparseModelType,
typename ConstantType>
594 specifyUntilFormula(env, currentCheckTask->substituteFormula(*untilFormula));
597template<
typename SparseModelType,
typename ConstantType>
600 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Parameter lifting is not supported for the given property.");
603template<
typename SparseModelType,
typename ConstantType>
606 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Parameter lifting is not supported for the given property.");
609template<
typename SparseModelType,
typename ConstantType>
611 std::shared_ptr<storm::analysis::Order> order) {
612 auto res = order->copy();
614 orderExtender->setUnknownStates(order, res);
615 orderExtender->copyMinMax(order, res);
620template<
typename SparseModelType,
typename ConstantType>
621std::pair<typename SparseModelType::ValueType, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation>
624 std::set<VariableType>& possibleMonotoneDecrParameters, std::set<VariableType>& possibleNotMonotoneParameters,
630 for (
auto& var : consideredVariables) {
631 ConstantType previousCenter = -1;
638 int numberOfSamples = 50;
643 ConstantType valueCenter = getInstantiationChecker()
644 .check(env, valuationCenter)
645 ->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
648 valuation = valuationCenter;
651 ConstantType diffCenter = previousCenter - valueCenter;
652 assert(previousCenter == -1 || (diffCenter >= -1 && diffCenter <= 1));
653 if (previousCenter != -1) {
654 assert(previousCenter != -1 && previousCenter != -1);
655 monDecr &= diffCenter > 0 && diffCenter > 0 && diffCenter > 0;
656 monIncr &= diffCenter < 0 && diffCenter < 0 && diffCenter < 0;
658 previousCenter = valueCenter;
659 if (!monDecr && !monIncr) {
662 valuationCenter[var] += stepSize;
665 possibleMonotoneParameters.insert(var);
666 possibleMonotoneIncrParameters.insert(var);
667 }
else if (monDecr) {
668 possibleMonotoneParameters.insert(var);
669 possibleMonotoneDecrParameters.insert(var);
671 possibleNotMonotoneParameters.insert(var);
674 return std::make_pair(storm::utility::convertNumber<typename SparseModelType::ValueType>(value), std::move(valuation));
677template<
typename SparseModelType,
typename ConstantType>
678std::pair<typename SparseModelType::ValueType, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation>
686 std::set<VariableType> monIncr, monDecr, notMon, notMonFirst;
689 if (localMonRes !=
nullptr) {
690 localMonRes->getGlobalMonotonicityResult()->splitBasedOnMonotonicity(region.
getVariables(), monIncr, monDecr, notMonFirst);
692 auto numMon = monIncr.size() + monDecr.size();
693 STORM_LOG_INFO(
"Number of monotone parameters: " << numMon <<
'\n';);
696 checkForPossibleMonotonicity(env, region, monIncr, monDecr, notMon, notMonFirst, dir);
697 STORM_LOG_INFO(
"Number of possible monotone parameters: " << (monIncr.size() + monDecr.size() - numMon) <<
'\n';);
698 STORM_LOG_INFO(
"Number of definitely not monotone parameters: " << notMon.size() <<
'\n';);
701 valuation = region.
getPoint(dir, monIncr, monDecr);
705 value = getInstantiationChecker()
706 .check(env, valuation)
707 ->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
709 return std::make_pair(storm::utility::convertNumber<typename SparseModelType::ValueType>(value), std::move(valuation));