Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseParameterLiftingModelChecker.cpp
Go to the documentation of this file.
2
4#include <boost/container/flat_set.hpp>
5#include <queue>
6
16
19
20namespace storm {
21namespace modelchecker {
22
23template<typename SparseModelType, typename ConstantType>
27
28template<typename SparseModelType, typename ConstantType>
31 currentFormula = checkTask.getFormula().asSharedPointer();
32 currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(
33 checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
35 if (currentCheckTask->getFormula().isProbabilityOperatorFormula()) {
36 auto const& probOpFormula = currentCheckTask->getFormula().asProbabilityOperatorFormula();
37 if (probOpFormula.getSubformula().isBoundedUntilFormula()) {
38 specifyBoundedUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asBoundedUntilFormula()));
39 } else if (probOpFormula.getSubformula().isUntilFormula()) {
40 specifyUntilFormula(env, currentCheckTask->substituteFormula(probOpFormula.getSubformula().asUntilFormula()));
41 } else if (probOpFormula.getSubformula().isEventuallyFormula()) {
42 specifyReachabilityProbabilityFormula(env, currentCheckTask->substituteFormula(probOpFormula.getSubformula().asEventuallyFormula()));
43 } else {
44 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
45 }
46 } else if (currentCheckTask->getFormula().isRewardOperatorFormula()) {
47 auto const& rewOpFormula = currentCheckTask->getFormula().asRewardOperatorFormula();
48 if (rewOpFormula.getSubformula().isEventuallyFormula()) {
49 specifyReachabilityRewardFormula(env, currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asEventuallyFormula()));
50 } else if (rewOpFormula.getSubformula().isCumulativeRewardFormula()) {
51 specifyCumulativeRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula()));
52 }
53 }
54}
56template<typename SparseModelType, typename ConstantType>
59 RegionResult const& initialResult, bool sampleVerticesOfRegion,
61 localMonotonicityResult) {
66 STORM_LOG_THROW(this->currentCheckTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException,
67 "Analyzing regions with parameter lifting requires a property where only the value in the initial states is relevant.");
68 STORM_LOG_THROW(this->currentCheckTask->isBoundSet(), storm::exceptions::NotSupportedException,
69 "Analyzing regions with parameter lifting requires a bounded property.");
70 STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException,
71 "Analyzing regions with parameter lifting requires a model with a single initial state.");
72
73 RegionResult result = initialResult;
74
75 // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
77 result = getInstantiationChecker()
78 .check(env, region.getCenterPoint())
79 ->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]
82 }
84 bool existsSat = (hypothesis == RegionResultHypothesis::AllSat || result == RegionResult::ExistsSat || result == RegionResult::CenterSat);
85 bool existsViolated =
88 // Here we check on global monotonicity
89 if (localMonotonicityResult != nullptr && localMonotonicityResult->isDone()) {
90 // Try to check it with a global monotonicity result
91 auto monRes = localMonotonicityResult->getGlobalMonotonicityResult();
92 bool lowerBound = isLowerBound(this->currentCheckTask->getBound().comparisonType);
93
94 if (monRes->isDone() && monRes->isAllMonotonicity()) {
95 // Build valuations
96 auto monMap = monRes->getMonotonicityResult();
97 Valuation valuationToCheckSat;
98 Valuation valuationToCheckViolated;
99 for (auto var : region.getVariables()) {
100 auto monVar = monMap[var];
101 if (monVar == Monotonicity::Constant) {
102 valuationToCheckSat.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
103 valuationToCheckViolated.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
104 } else if (monVar == Monotonicity::Decr) {
105 if (lowerBound) {
106 valuationToCheckSat.insert(std::pair<VariableType, CoefficientType>(var, region.getUpperBoundary(var)));
107 valuationToCheckViolated.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
108 } else {
109 valuationToCheckSat.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
110 valuationToCheckViolated.insert(std::pair<VariableType, CoefficientType>(var, region.getUpperBoundary(var)));
111 }
112 } else if (monVar == Monotonicity::Incr) {
113 if (lowerBound) {
114 valuationToCheckSat.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
115 valuationToCheckViolated.insert(std::pair<VariableType, CoefficientType>(var, region.getUpperBoundary(var)));
116 } else {
117 valuationToCheckSat.insert(std::pair<VariableType, CoefficientType>(var, region.getUpperBoundary(var)));
118 valuationToCheckViolated.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
119 }
120 }
121 }
123 // Check for result
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");
131 }
132
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");
140 }
141
143 }
144 }
145
146 // Try to prove AllSat or AllViolated, depending on the hypothesis or the current result
147 if (existsSat) {
148 // show AllSat:
149 storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType)
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()]) {
154 result = RegionResult::AllSat;
155 } else if (sampleVerticesOfRegion) {
156 result = sampleVertices(env, region, result);
157 }
158 } else if (existsViolated) {
159 // show AllViolated:
160 storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType)
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);
168 }
169 } else {
170 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
171 }
172 return result;
173}
174
175template<typename SparseModelType, typename ConstantType>
178 RegionResult result = initialResult;
179
180 if (result == RegionResult::AllSat || result == RegionResult::AllViolated) {
181 return result;
182 }
183
184 bool hasSatPoint = result == RegionResult::ExistsSat || result == RegionResult::CenterSat;
185 bool hasViolatedPoint = result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated;
186
187 // Check if there is a point in the region for which the property is satisfied
188 auto vertices = region.getVerticesOfRegion(region.getVariables());
189 auto vertexIt = vertices.begin();
190 while (vertexIt != vertices.end() && !(hasSatPoint && hasViolatedPoint)) {
191 if (getInstantiationChecker().check(env, *vertexIt)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
192 hasSatPoint = true;
193 } else {
194 hasViolatedPoint = true;
195 }
196 ++vertexIt;
197 }
198
199 if (hasSatPoint) {
200 if (hasViolatedPoint) {
202 } else if (result != RegionResult::CenterSat) {
204 }
205 } else if (hasViolatedPoint && result != RegionResult::CenterViolated) {
207 }
208
209 return result;
210}
211
212template<typename SparseModelType, typename ConstantType>
215 storm::solver::OptimizationDirection const& dirForParameters,
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;
222 } else {
223 return quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(
224 this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(),
225 this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
226 }
227}
228
229template<typename SparseModelType, typename ConstantType>
230std::unique_ptr<QuantitativeCheckResult<ConstantType>> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBound(
232 storm::solver::OptimizationDirection const& dirForParameters,
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>()));
238}
239
240template<typename SparseModelType, typename ConstantType>
243 storm::solver::OptimizationDirection const& dirForParameters) {
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()]);
249}
250
251template<typename SparseModelType, typename ConstantType>
256
257template<typename SparseModelType, typename ConstantType>
262
263template<typename SparseModelType, typename ConstantType>
266
268 std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> l, boost::optional<ConstantType> const& b)
269 : region(r), order(o), localMonRes(l), bound(b) {}
271 std::shared_ptr<storm::analysis::Order> order;
272 std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> localMonRes;
273 boost::optional<ConstantType> bound;
274};
275
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();
289 bool const minimize = storm::solver::minimize(dir);
290
291 // Comparator for the region queue
293 RegionBound<SparseModelType, ConstantType> const& rhs) { return lhs.bound > rhs.bound; }
294 : [](RegionBound<SparseModelType, ConstantType> const& lhs, RegionBound<SparseModelType, ConstantType> const& rhs) {
295 return lhs.bound < rhs.bound;
296 };
297 std::priority_queue<RegionBound<SparseModelType, ConstantType>, std::vector<RegionBound<SparseModelType, ConstantType>>, decltype(cmp)> regionQueue(cmp);
298 storm::utility::Stopwatch initialWatch(true);
299
300 storm::utility::Stopwatch boundsWatch(false);
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>()
309 .getValueVector();
310 auto maxBound = getBound(env, region, storm::solver::OptimizationDirection::Maximize, nullptr)
311 ->template asExplicitQuantitativeCheckResult<ConstantType>()
312 .getValueVector();
313 if (minimize) {
314 initBound = minBound[*this->parametricModel->getInitialStates().begin()];
315 } else {
316 initBound = maxBound[*this->parametricModel->getInitialStates().begin()];
317 }
318 orderExtender->setMinValuesInit(minBound);
319 orderExtender->setMaxValuesInit(maxBound);
320 }
321 auto order = this->extendOrder(nullptr, region);
322 auto monRes = std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>>(
323 new storm::analysis::LocalMonotonicityResult<VariableType>(order->getNumberOfStates()));
324 storm::utility::Stopwatch monotonicityWatch(true);
325 this->extendLocalMonotonicityResult(region, order, monRes);
326 monotonicityWatch.stop();
327 STORM_LOG_INFO("\nTotal time for monotonicity checking: " << monotonicityWatch << ".\n\n");
328
329 regionQueue.emplace(region, order, monRes, initBound);
330 } else {
331 regionQueue.emplace(region, nullptr, nullptr, initBound);
332 }
333
334 // The results
335 boost::optional<ConstantType> value;
336 Valuation valuation;
337 if (!initialValue) {
338 auto init = getGoodInitialPoint(env, region, dir, regionQueue.top().localMonRes);
339 value = storm::utility::convertNumber<ConstantType>(init.first);
340 valuation = std::move(init.second);
341 } else {
342 value = initialValue;
343 }
344
345 initialWatch.stop();
346 STORM_LOG_INFO("\nTotal time for initial points: " << initialWatch << ".\n\n");
347 if (!initialValue) {
348 STORM_LOG_INFO("Initial value: " << value.get() << " at " << valuation);
349 } else {
350 STORM_LOG_INFO("Initial value: " << value.get() << " as provided by the user");
351 }
352
353 if (terminationBound != std::nullopt && !terminationBound.value().isSatisfied(value.get())) {
354 return std::make_pair(storm::utility::convertNumber<ConstantType>(value.get()), valuation);
355 }
356
357 auto numberOfSplits = 0;
358 auto numberOfPLACalls = 0;
359 auto numberOfOrderCopies = 0;
360 auto numberOfMonResCopies = 0;
361 storm::utility::Stopwatch loopWatch(true);
362 if (!(useMonotonicity && regionQueue.top().localMonRes->getGlobalMonotonicityResult()->isDone() &&
363 regionQueue.top().localMonRes->getGlobalMonotonicityResult()->isAllMonotonicity())) {
364 // Doing the extremal computation, only when we don't use monotonicity or there are possibly not monotone variables.
365 auto totalArea = storm::utility::convertNumber<ConstantType>(region.area());
366 auto coveredArea = storm::utility::zero<ConstantType>();
367 while (!regionQueue.empty()) {
368 assert(value);
369 auto currRegion = regionQueue.top().region;
370 auto order = regionQueue.top().order;
371 auto localMonotonicityResult = regionQueue.top().localMonRes;
372 auto currBound = regionQueue.top().bound;
373 STORM_LOG_INFO("Currently looking at region: " << currRegion);
374
375 std::vector<storm::storage::ParameterRegion<typename SparseModelType::ValueType>> newRegions;
376
377 // Check whether this region needs further investigation based on the bound of the parent region
378 bool investigateBounds = !currBound;
379
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()));
386 }
387
388 if (investigateBounds) {
389 numberOfPLACalls++;
390 auto bounds =
391 getBound(env, currRegion, dir, localMonotonicityResult)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
392 // TODO this looks dangerous
393 currBound = bounds[*this->parametricModel->getInitialStates().begin()];
394 // Check whether this region needs further investigation based on the bound of this region
395 bool lookAtRegion;
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));
399 } else {
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()));
402 }
403 if (lookAtRegion) {
404 if (useMonotonicity) {
405 // Continue extending order/monotonicity result
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++;
412 } else {
413 assert(numberOfCopiesOrder[order] == 1);
414 }
415 this->extendOrder(order, currRegion);
416 changedOrder = true;
417 }
418 if (changedOrder) {
419 assert(!localMonotonicityResult->isDone());
420
421 if (numberOfCopiesMonRes[localMonotonicityResult] != 1) {
422 numberOfCopiesMonRes[localMonotonicityResult]--;
423 localMonotonicityResult = localMonotonicityResult->copy();
424 numberOfMonResCopies++;
425 } else {
426 assert(numberOfCopiesMonRes[localMonotonicityResult] == 1);
427 }
428 this->extendLocalMonotonicityResult(currRegion, order, localMonotonicityResult);
429 STORM_LOG_INFO("Order and monotonicity result got extended");
430 }
431 }
432
433 // Check whether this region contains a new 'good' value and set this value
434 auto point =
435 useMonotonicity ? currRegion.getPoint(dir, *(localMonotonicityResult->getGlobalMonotonicityResult())) : currRegion.getCenterPoint();
436 auto currValue = getInstantiationChecker()
437 .check(env, point)
438 ->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
439 if (!value || (minimize ? currValue <= value.get() : currValue >= value.get())) {
440 value = currValue;
441 valuation = point;
442 if (terminationBound != std::nullopt && !terminationBound.value().isSatisfied(value.get())) {
443 return std::make_pair(storm::utility::convertNumber<ConstantType>(value.get()), valuation);
444 }
445 }
446
447 bool splitRegion;
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));
451 } else {
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()));
454 }
455 if (splitRegion) {
456 // We will split the region in this case, but first we set the bounds to extend the order for the new regions.
457 if (useMonotonicity && this->isUseBoundsSet() && !order->getDoneBuilding()) {
458 boundsWatch.start();
459 numberOfPLACallsBounds++;
460 if (minimize) {
461 orderExtender->setMinMaxValues(
462 order, bounds,
463 getBound(env, currRegion, storm::solver::OptimizationDirection::Maximize, localMonotonicityResult)
464 ->template asExplicitQuantitativeCheckResult<ConstantType>()
465 .getValueVector());
466 } else {
467 orderExtender->setMinMaxValues(
468 order,
469 getBound(env, currRegion, storm::solver::OptimizationDirection::Maximize, localMonotonicityResult)
470 ->template asExplicitQuantitativeCheckResult<ConstantType>()
471 .getValueVector(),
472 bounds);
473 }
474 boundsWatch.stop();
475 }
476 // Now split the region
477 if (useMonotonicity) {
478 this->splitSmart(currRegion, newRegions, *(localMonotonicityResult->getGlobalMonotonicityResult()), true);
479 } else if (this->isRegionSplitEstimateSupported()) {
481 this->splitSmart(currRegion, newRegions, empty, true);
482 } else {
483 currRegion.split(currRegion.getCenterPoint(), newRegions);
484 }
485 }
486 }
487 }
488
489 if (newRegions.empty()) {
490 // When the newRegions is empty we are done with the current region
491 coveredArea += storm::utility::convertNumber<ConstantType>(currRegion.area());
492 if (order != nullptr) {
493 numberOfCopiesOrder[order]--;
494 numberOfCopiesMonRes[localMonotonicityResult]--;
495 }
496 regionQueue.pop();
497 } else {
498 regionQueue.pop();
499 STORM_LOG_INFO("Splitting region " << currRegion << " into " << newRegions.size());
500 numberOfSplits++;
501 // Add the new regions to the queue
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());
506 }
507 if (numberOfCopiesOrder.find(order) != numberOfCopiesOrder.end()) {
508 numberOfCopiesOrder[order] += newRegions.size();
509 numberOfCopiesMonRes[localMonotonicityResult] += newRegions.size();
510 } else {
511 numberOfCopiesOrder[order] = newRegions.size();
512 numberOfCopiesMonRes[localMonotonicityResult] = newRegions.size();
513 }
514 } else {
515 for (auto& r : newRegions) {
516 r.setBoundParent(storm::utility::convertNumber<CoefficientType>(currBound.get()));
517 regionQueue.emplace(r, nullptr, nullptr, currBound.get());
518 }
519 }
520 }
521
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");
524 }
525 loopWatch.stop();
526 }
527
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');
534 }
535 STORM_LOG_INFO("\nTotal time for region refinement: " << loopWatch << ".\n\n");
536 STORM_LOG_INFO("\nTotal time for additional bounds: " << boundsWatch << ".\n\n");
537
538 return std::make_pair(storm::utility::convertNumber<ConstantType>(value.get()), valuation);
539}
540
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};
548}
549
550template<typename SparseModelType, typename ConstantType>
553 // Use the bound from the formula.
554 ConstantType valueToCheck = storm::utility::convertNumber<ConstantType>(bound.threshold.evaluateAsDouble());
555 // We will try to violate the bound.
557 isLowerBound(bound.comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
558 // We pass the bound as an invariant; as soon as it is obtained, we can stop the search.
559 auto res = computeExtremalValue(env, region, dir, storm::utility::zero<typename SparseModelType::ValueType>(), false, boost::none, bound).first;
560 STORM_LOG_DEBUG("Reported extremal value " << res);
561 // TODO use termination bound instead of initial value?
562 return storm::solver::minimize(dir) ? storm::utility::convertNumber<ConstantType>(res) >= valueToCheck
563 : storm::utility::convertNumber<ConstantType>(res) <= valueToCheck;
564}
565
566template<typename SparseModelType, typename ConstantType>
568 return *parametricModel;
569}
570
571template<typename SparseModelType, typename ConstantType>
575
576template<typename SparseModelType, typename ConstantType>
579 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
580}
581
582template<typename SparseModelType, typename ConstantType>
585 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
586}
587
588template<typename SparseModelType, typename ConstantType>
591 // transform to until formula
592 auto untilFormula =
593 std::make_shared<storm::logic::UntilFormula const>(storm::logic::Formula::getTrueFormula(), checkTask.getFormula().getSubformula().asSharedPointer());
594 specifyUntilFormula(env, currentCheckTask->substituteFormula(*untilFormula));
595}
596
597template<typename SparseModelType, typename ConstantType>
600 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
601}
602
603template<typename SparseModelType, typename ConstantType>
606 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
607}
608
609template<typename SparseModelType, typename ConstantType>
611 std::shared_ptr<storm::analysis::Order> order) {
612 auto res = order->copy();
613 if (orderExtender) {
614 orderExtender->setUnknownStates(order, res);
615 orderExtender->copyMinMax(order, res);
616 }
617 return res;
618}
619
620template<typename SparseModelType, typename ConstantType>
621std::pair<typename SparseModelType::ValueType, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation>
623 Environment const& env, const storage::ParameterRegion<typename SparseModelType::ValueType>& region, std::set<VariableType>& possibleMonotoneIncrParameters,
624 std::set<VariableType>& possibleMonotoneDecrParameters, std::set<VariableType>& possibleNotMonotoneParameters,
625 std::set<VariableType> const& consideredVariables, storm::solver::OptimizationDirection const& dir) {
628 ConstantType value = storm::solver::minimize(dir) ? 1 : 0;
629 Valuation valuation;
630 for (auto& var : consideredVariables) {
631 ConstantType previousCenter = -1;
632 bool monDecr = true;
633 bool monIncr = true;
634 auto valuationCenter = region.getCenterPoint();
635
636 valuationCenter[var] = region.getLowerBoundary(var);
637 // TODO: make cmdline argument or 1/precision
638 int numberOfSamples = 50;
639 auto stepSize = (region.getUpperBoundary(var) - region.getLowerBoundary(var)) / (numberOfSamples - 1);
640
641 while (valuationCenter[var] <= region.getUpperBoundary(var)) {
642 // Create valuation
643 ConstantType valueCenter = getInstantiationChecker()
644 .check(env, valuationCenter)
645 ->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
646 if (storm::solver::minimize(dir) ? valueCenter <= value : valueCenter >= value) {
647 value = valueCenter;
648 valuation = valuationCenter;
649 }
650 // Calculate difference with result for previous valuation
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; // then previous value is larger than the current value from the initial states
656 monIncr &= diffCenter < 0 && diffCenter < 0 && diffCenter < 0;
657 }
658 previousCenter = valueCenter;
659 if (!monDecr && !monIncr) {
660 break;
661 }
662 valuationCenter[var] += stepSize;
663 }
664 if (monIncr) {
665 possibleMonotoneParameters.insert(var);
666 possibleMonotoneIncrParameters.insert(var);
667 } else if (monDecr) {
668 possibleMonotoneParameters.insert(var);
669 possibleMonotoneDecrParameters.insert(var);
670 } else {
671 possibleNotMonotoneParameters.insert(var);
672 }
673 }
674 return std::make_pair(storm::utility::convertNumber<typename SparseModelType::ValueType>(value), std::move(valuation));
675}
676
677template<typename SparseModelType, typename ConstantType>
678std::pair<typename SparseModelType::ValueType, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation>
681 std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> localMonRes) {
684 ConstantType value = storm::solver::minimize(dir) ? 1 : 0;
685 Valuation valuation;
686 std::set<VariableType> monIncr, monDecr, notMon, notMonFirst;
687 STORM_LOG_INFO("Number of parameters: " << region.getVariables().size() << '\n';);
688
689 if (localMonRes != nullptr) {
690 localMonRes->getGlobalMonotonicityResult()->splitBasedOnMonotonicity(region.getVariables(), monIncr, monDecr, notMonFirst);
691
692 auto numMon = monIncr.size() + monDecr.size();
693 STORM_LOG_INFO("Number of monotone parameters: " << numMon << '\n';);
694
695 if (numMon < region.getVariables().size()) {
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';);
699 }
700
701 valuation = region.getPoint(dir, monIncr, monDecr);
702 } else {
703 valuation = region.getCenterPoint();
704 }
705 value = getInstantiationChecker()
706 .check(env, valuation)
707 ->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
708
709 return std::make_pair(storm::utility::convertNumber<typename SparseModelType::ValueType>(value), std::move(valuation));
710}
711
716} // namespace modelchecker
717} // namespace storm
Monotonicity
The results of monotonicity checking for a single Parameter Region.
double evaluateAsDouble(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
static std::shared_ptr< Formula const > getTrueFormula()
Definition Formula.cpp:205
CheckTask< NewFormulaType, ValueType > substituteFormula(NewFormulaType const &newFormula) const
Copies the check task from the source while replacing the formula with the new one.
Definition CheckTask.h:52
FormulaType const & getFormula() const
Retrieves the formula from this task.
Definition CheckTask.h:140
storm::storage::ParameterRegion< SparseModelType::ValueType >::CoefficientType CoefficientType
storm::storage::ParameterRegion< ParametricType >::VariableType VariableType
Class to efficiently check a formula on a parametric model with different parameter instantiations.
Class to approximatively check a formula on a parametric model for all parameter valuations within a ...
virtual RegionResult analyzeRegion(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, RegionResultHypothesis const &hypothesis=RegionResultHypothesis::Unknown, RegionResult const &initialResult=RegionResult::Unknown, bool sampleVerticesOfRegion=false, std::shared_ptr< storm::analysis::LocalMonotonicityResult< typename RegionModelChecker< typename SparseModelType::ValueType >::VariableType > > localMonotonicityResult=nullptr) override
Analyzes the given region by means of parameter lifting.
virtual bool verifyRegion(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, storm::logic::Bound const &bound) override
Checks whether the bound is satisfied on the complete region.
std::pair< typename SparseModelType::ValueType, typename storm::storage::ParameterRegion< typename SparseModelType::ValueType >::Valuation > getGoodInitialPoint(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, storm::solver::OptimizationDirection const &dir, std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > > localMonRes)
virtual storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType > & getInstantiationCheckerSAT()
virtual void specifyUntilFormula(Environment const &env, CheckTask< storm::logic::UntilFormula, ConstantType > const &checkTask)
virtual std::pair< typename SparseModelType::ValueType, typename storm::storage::ParameterRegion< typename SparseModelType::ValueType >::Valuation > computeExtremalValue(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, storm::solver::OptimizationDirection const &dirForParameters, typename SparseModelType::ValueType const &precision, bool absolutePrecision, std::optional< storm::logic::Bound > const &terminationBound=std::nullopt) override
Finds the extremal value within the given region and with the given precision.
virtual void specifyReachabilityRewardFormula(Environment const &env, CheckTask< storm::logic::EventuallyFormula, ConstantType > const &checkTask)
virtual storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType > & getInstantiationCheckerVIO()
virtual void specifyCumulativeRewardFormula(const CheckTask< storm::logic::CumulativeRewardFormula, ConstantType > &checkTask)
std::unique_ptr< CheckResult > check(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, storm::solver::OptimizationDirection const &dirForParameters, std::shared_ptr< storm::analysis::LocalMonotonicityResult< typename RegionModelChecker< typename SparseModelType::ValueType >::VariableType > > localMonotonicityResult=nullptr)
Checks the specified formula on the given region by applying parameter lifting (Parameter choices are...
void specifyFormula(Environment const &env, CheckTask< storm::logic::Formula, typename SparseModelType::ValueType > const &checkTask)
std::pair< typename SparseModelType::ValueType, typename storm::storage::ParameterRegion< typename SparseModelType::ValueType >::Valuation > checkForPossibleMonotonicity(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, std::set< VariableType > &possibleMonotoneIncrParameters, std::set< VariableType > &possibleMonotoneDecrParameters, std::set< VariableType > &possibleNotMonotoneParameters, std::set< VariableType > const &consideredVariables, storm::solver::OptimizationDirection const &dir)
RegionResult sampleVertices(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, RegionResult const &initialResult=RegionResult::Unknown)
Analyzes the 2^#parameters corner points of the given region.
virtual void specifyReachabilityProbabilityFormula(Environment const &env, CheckTask< storm::logic::EventuallyFormula, ConstantType > const &checkTask)
CheckTask< storm::logic::Formula, ConstantType > const & getCurrentCheckTask() const
std::unique_ptr< QuantitativeCheckResult< ConstantType > > getBound(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, storm::solver::OptimizationDirection const &dirForParameters, std::shared_ptr< storm::analysis::LocalMonotonicityResult< typename RegionModelChecker< typename SparseModelType::ValueType >::VariableType > > localMonotonicityResult=nullptr)
virtual SparseModelType::ValueType getBoundAtInitState(Environment const &env, storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &region, storm::solver::OptimizationDirection const &dirForParameters) override
virtual void specifyBoundedUntilFormula(const CheckTask< storm::logic::BoundedUntilFormula, ConstantType > &checkTask)
storm::utility::parametric::CoefficientType< ParametricType >::type CoefficientType
std::set< VariableType > const & getVariables() const
Valuation getCenterPoint() const
Returns the center point of this region.
CoefficientType area() const
Returns the area of this region.
storm::utility::parametric::Valuation< ParametricType > Valuation
storm::utility::parametric::VariableType< ParametricType >::type VariableType
Valuation getPoint(storm::solver::OptimizationDirection dir, storm::analysis::MonotonicityResult< VariableType > &monRes) const
CoefficientType const & getLowerBoundary(VariableType const &variable) const
CoefficientType const & getUpperBoundary(VariableType const &variable) const
std::vector< Valuation > getVerticesOfRegion(std::set< VariableType > const &consideredVariables) const
Returns a vector of all possible combinations of lower and upper bounds of the given variables.
A class that provides convenience operations to display run times.
Definition Stopwatch.h:14
#define STORM_LOG_INFO(message)
Definition logging.h:29
#define STORM_LOG_DEBUG(message)
Definition logging.h:23
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
bool isLowerBound(ComparisonType t)
helper::MDPSparseModelCheckingHelperReturnType< ValueType > check(Environment const &, SparseModelType const &model, CheckTask< storm::logic::MultiObjectiveFormula, ValueType > const &checkTask, CheckFormulaCallback const &formulaChecker)
check a lexicographic LTL-formula
RegionResult
The results for a single Parameter Region.
@ CenterSat
the formula is satisfied for the parameter Valuation that corresponds to the center point of the regi...
@ AllSat
the formula is satisfied for all parameters in the given region
@ AllViolated
the formula is violated for all parameters in the given region
@ Unknown
the result is unknown
@ ExistsBoth
the formula is satisfied for some parameters but also violated for others
@ CenterViolated
the formula is violated for the parameter Valuation that corresponds to the center point of the regio...
@ ExistsSat
the formula is satisfied for at least one parameter evaluation that lies in the given region
@ ExistsViolated
the formula is violated for at least one parameter evaluation that lies in the given region
RegionResultHypothesis
hypothesis for the result for a single Parameter Region
bool constexpr minimize(OptimizationDirection d)
std::map< typename VariableType< FunctionType >::type, typename CoefficientType< FunctionType >::type > Valuation
Definition parametric.h:41
LabParser.cpp.
Definition cli.cpp:18
ComparisonType comparisonType
Definition Bound.h:18
storm::expressions::Expression threshold
Definition Bound.h:19
std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > > localMonRes
storm::storage::ParameterRegion< typenameSparseModelType::ValueType >::VariableType VariableType
storm::storage::ParameterRegion< typename SparseModelType::ValueType > region
RegionBound(storm::storage::ParameterRegion< typename SparseModelType::ValueType > const &r, std::shared_ptr< storm::analysis::Order > o, std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > > l, boost::optional< ConstantType > const &b)
std::shared_ptr< storm::analysis::Order > order