From c07734d80a0d7c0099acc870a71452b23e371e7c Mon Sep 17 00:00:00 2001 From: Jan Erik Karuc Date: Fri, 3 Apr 2020 10:39:27 +0200 Subject: [PATCH 1/8] Handle no change after verification iterations by re-guessing This may lead to some testcases breaking. Needs further investigation Handle only no change by re-guessing, instead of all other cases --- src/storm/solver/helper/OptimisticValueIterationHelper.h | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 1adb29b38..4cfe6c012 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -175,7 +175,7 @@ namespace storm { newUpperBoundAlwaysLowerEqual = false; } } - if (newUpperBoundAlwaysHigherEqual & !newUpperBoundAlwaysLowerEqual) { + if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { // All values moved up or stayed the same (but are not the same) // That means the guess for an upper bound is actually a lower bound iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); @@ -183,7 +183,7 @@ namespace storm { // Set lowerX to the upper bound candidate std::swap(lowerX, upperX); break; - } else if (newUpperBoundAlwaysLowerEqual) { + } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { // All values moved down or stayed the same and we have a maximum difference of twice the requested precision // We can safely use twice the requested precision, as we calculate the center of both vectors bool reachedPrecision; @@ -199,6 +199,9 @@ namespace storm { // From now on, we keep updating both bounds intervalIterationNeeded = true; } + } else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { + // All values stayed the same. For safety we guess above this value again and check, if all values move down + break; } // At this point, the old upper bounds (auxVector) are not needed anymore. From 7982d58ef7e43e6a09459310d5a6bb13a7916ddd Mon Sep 17 00:00:00 2001 From: Jan Erik Karuc Date: Fri, 3 Apr 2020 12:27:13 +0200 Subject: [PATCH 2/8] Combine new upper bound geq cases --- src/storm/solver/helper/OptimisticValueIterationHelper.h | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 4cfe6c012..c298b0ffe 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -175,15 +175,15 @@ namespace storm { newUpperBoundAlwaysLowerEqual = false; } } - if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { - // All values moved up or stayed the same (but are not the same) + if (newUpperBoundAlwaysHigherEqual) { + // All values moved up or stayed the same // That means the guess for an upper bound is actually a lower bound iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound // Set lowerX to the upper bound candidate std::swap(lowerX, upperX); break; - } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { + } else if (newUpperBoundAlwaysLowerEqual) { // All values moved down or stayed the same and we have a maximum difference of twice the requested precision // We can safely use twice the requested precision, as we calculate the center of both vectors bool reachedPrecision; @@ -199,9 +199,6 @@ namespace storm { // From now on, we keep updating both bounds intervalIterationNeeded = true; } - } else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { - // All values stayed the same. For safety we guess above this value again and check, if all values move down - break; } // At this point, the old upper bounds (auxVector) are not needed anymore. From 778a4fc71b96775bf420590f375c3d7f6031d0c7 Mon Sep 17 00:00:00 2001 From: Jan Erik Karuc Date: Thu, 30 Apr 2020 21:12:50 +0200 Subject: [PATCH 3/8] Added temporary function to apply no-change hm results on lower bound --- .../helper/OptimisticValueIterationHelper.h | 224 +++++++++++++++++- 1 file changed, 221 insertions(+), 3 deletions(-) diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index c298b0ffe..c936638c0 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -81,7 +81,216 @@ namespace storm { void guessUpperBoundAbsolute(std::vector const& x, std::vector &target, ValueType const& precision) { storm::utility::vector::applyPointwise(x, target, [&precision] (ValueType const& argument) -> ValueType { return argument + precision; }); } - + + namespace debug { + template + void applyHaddedMonmegeAlwaysEqualResultToLowerBound(std::vector* lowerX, const int n) { + switch(n) { + case 198: + (*lowerX)[0] = 3.5527502373072761e-15; + (*lowerX)[1] = 3.5527502373072769e-15; + (*lowerX)[2] = 3.5527502373072753e-15; + (*lowerX)[3] = 3.5527502373072785e-15; + (*lowerX)[4] = 3.5527502373072753e-15; + (*lowerX)[5] = 3.5527502373072816e-15; + (*lowerX)[6] = 3.5527502373072753e-15; + (*lowerX)[7] = 3.5527502373072879e-15; + (*lowerX)[8] = 3.5527502373072753e-15; + (*lowerX)[9] = 3.5527502373073006e-15; + (*lowerX)[10] = 3.5527502373072753e-15; + (*lowerX)[11] = 3.5527502373073258e-15; + (*lowerX)[12] = 3.5527502373072753e-15; + (*lowerX)[13] = 3.5527502373073763e-15; + (*lowerX)[14] = 3.5527502373072753e-15; + (*lowerX)[15] = 3.5527502373074773e-15; + (*lowerX)[16] = 3.5527502373072753e-15; + (*lowerX)[17] = 3.5527502373076792e-15; + (*lowerX)[18] = 3.552750237072753e-15; + (*lowerX)[19] = 3.5527502373080831e-15; + (*lowerX)[20] = 3.5527502373072753e-15; + (*lowerX)[21] = 3.5527502373088909e-15; + (*lowerX)[22] = 3.5527502373072753e-15; + (*lowerX)[23] = 3.5527502373105065e-15; + (*lowerX)[24] = 3.5527502373072753e-15; + (*lowerX)[25] = 3.5527502373137377e-15; + (*lowerX)[26] = 3.5527502373072753e-15; + (*lowerX)[27] = 3.5527502373202e-15; + (*lowerX)[28] = 3.5527502373072753e-15; + (*lowerX)[29] = 3.5527502373331247e-15; + (*lowerX)[30] = 3.5527502373072753e-15; + (*lowerX)[31] = 3.5527502373589741e-15; + (*lowerX)[32] = 3.5527502373072753e-15; + (*lowerX)[33] = 3.5527502374106729e-15; + (*lowerX)[34] = 3.5527502373072753e-15; + (*lowerX)[35] = 3.5527502375140705e-15; + (*lowerX)[36] = 3.5527502373072753e-15; + (*lowerX)[37] = 3.5527502377208656e-15; + (*lowerX)[38] = 3.5527502373072753e-15; + (*lowerX)[39] = 3.5527502381344559e-15; + (*lowerX)[40] = 3.5527502373072753e-15; + (*lowerX)[41] = 3.5527502389616373e-15; + (*lowerX)[42] = 3.5527502373072753e-15; + (*lowerX)[43] = 3.5527502406159986e-15; + (*lowerX)[44] = 3.5527502373072753e-15; + (*lowerX)[45] = 3.552750243924721e-15; + (*lowerX)[46] = 3.5527502373072753e-15; + (*lowerX)[47] = 3.5527502505421667e-15; + (*lowerX)[48] = 3.5527502373072753e-15; + (*lowerX)[49] = 3.5527502637770581e-15; + (*lowerX)[50] = 3.5527502373072753e-15; + (*lowerX)[51] = 3.55275029024684e-15; + (*lowerX)[52] = 3.5527502373072753e-15; + (*lowerX)[53] = 3.5527503431864048e-15; + (*lowerX)[54] = 3.5527502373072753e-15; + (*lowerX)[55] = 3.5527504490655334e-15; + (*lowerX)[56] = 3.5527502373072753e-15; + (*lowerX)[57] = 3.5527506608237915e-15; + (*lowerX)[58] = 3.5527502373072753e-15; + (*lowerX)[59] = 3.5527510843403078e-15; + (*lowerX)[60] = 3.5527502373072753e-15; + (*lowerX)[61] = 3.5527519313733394e-15; + (*lowerX)[62] = 3.5527502373072753e-15; + (*lowerX)[63] = 3.5527536254394035e-15; + (*lowerX)[64] = 3.5527502373072753e-15; + (*lowerX)[65] = 3.552757013571531e-15; + (*lowerX)[66] = 3.5527502373072753e-15; + (*lowerX)[67] = 3.5527637898357866e-15; + (*lowerX)[68] = 3.5527502373072753e-15; + (*lowerX)[69] = 3.552777342364298e-15; + (*lowerX)[70] = 3.5527502373072753e-15; + (*lowerX)[71] = 3.5528044474213206e-15; + (*lowerX)[72] = 3.5527502373072753e-15; + (*lowerX)[73] = 3.552858657535366e-15; + (*lowerX)[74] = 3.5527502373072753e-15; + (*lowerX)[75] = 3.5529670777634566e-15; + (*lowerX)[76] = 3.5527502373072753e-15; + (*lowerX)[77] = 3.5531839182196379e-15; + (*lowerX)[78] = 3.5527502373072753e-15; + (*lowerX)[79] = 3.5536175991319998e-15; + (*lowerX)[80] = 3.5527502373072753e-15; + (*lowerX)[81] = 3.554484960956725e-15; + (*lowerX)[82] = 3.5527502373072753e-15; + (*lowerX)[83] = 3.5562196846061739e-15; + (*lowerX)[84] = 3.5527502373072753e-15; + (*lowerX)[85] = 3.5596891319050725e-15; + (*lowerX)[86] = 3.5527502373072753e-15; + (*lowerX)[87] = 3.5666280265028689e-15; + (*lowerX)[88] = 3.5527502373072753e-15; + (*lowerX)[89] = 3.5805058156984624e-15; + (*lowerX)[90] = 3.5527502373072753e-15; + (*lowerX)[91] = 3.6082613940896487e-15; + (*lowerX)[92] = 3.5527502373072753e-15; + (*lowerX)[93] = 3.6637725508720213e-15; + (*lowerX)[94] = 3.5527502373072753e-15; + (*lowerX)[95] = 3.7747948644367674e-15; + (*lowerX)[96] = 3.5527502373072753e-15; + (*lowerX)[97] = 3.9968394915662579e-15; + (*lowerX)[98] = 3.5527502373072737e-15; + (*lowerX)[99] = 4.4409287458252396e-15; + (*lowerX)[100] = 3.5527502373072722e-15; + (*lowerX)[101] = 5.3291072543432039e-15; + (*lowerX)[102] = 3.552750237307269e-15; + (*lowerX)[103] = 7.1054642713791325e-15; + (*lowerX)[104] = 3.5527502373072627e-15; + (*lowerX)[105] = 1.0658178305450988e-14; + (*lowerX)[106] = 3.5527502373072501e-15; + (*lowerX)[107] = 1.7763606373594701e-14; + (*lowerX)[108] = 3.5527502373072248e-15; + (*lowerX)[109] = 3.1974462509882126e-14; + (*lowerX)[110] = 3.5527502373071743e-15; + (*lowerX)[111] = 6.0396174782456978e-14; + (*lowerX)[112] = 3.5527502373070734e-15; + (*lowerX)[113] = 1.1723959932760665e-13; + (*lowerX)[114] = 3.5527502373068714e-15; + (*lowerX)[115] = 2.3092644841790603e-13; + (*lowerX)[116] = 3.5527502373064675e-15; + (*lowerX)[117] = 4.5830014659850484e-13; + (*lowerX)[118] = 3.5527502373056597e-15; + (*lowerX)[119] = 9.1304754295970246e-13; + (*lowerX)[120] = 3.5527502373040441e-15; + (*lowerX)[121] = 1.8225423356820975e-12; + (*lowerX)[122] = 3.552750237300813e-15; + (*lowerX)[123] = 3.641531921126888e-12; + (*lowerX)[124] = 3.5527502372943506e-15; + (*lowerX)[125] = 7.2795110920164697e-12; + (*lowerX)[126] = 3.5527502372814259e-15; + (*lowerX)[127] = 1.4555469433795628e-11; + (*lowerX)[128] = 3.5527502372555765e-15; + (*lowerX)[129] = 2.9107386117353949e-11; + (*lowerX)[130] = 3.5527502372038777e-15; + (*lowerX)[131] = 5.8211219484470597e-11; + (*lowerX)[132] = 3.5527502371004786e-15; + (*lowerX)[133] = 1.1641888621870388e-10; + (*lowerX)[134] = 3.5527502368936819e-15; + (*lowerX)[135] = 2.3283421968717047e-10; + (*lowerX)[136] = 3.5527502364800868e-15; + (*lowerX)[137] = 4.6566488662410365e-10; + (*lowerX)[138] = 3.5527502356528983e-15; + (*lowerX)[139] = 9.3132622049797001e-10; + (*lowerX)[140] = 3.5527502339985197e-15; + (*lowerX)[141] = 1.8626488882457027e-09; + (*lowerX)[142] = 3.5527502306897634e-15; + (*lowerX)[143] = 3.7252942237411686e-09; + (*lowerX)[144] = 3.5527502240722506e-15; + (*lowerX)[145] = 7.4505848947320987e-09; + (*lowerX)[146] = 3.5527502108372251e-15; + (*lowerX)[147] = 1.4901166236713957e-08; + (*lowerX)[148] = 3.5527501843671734e-15; + (*lowerX)[149] = 2.9802328920677681e-08; + (*lowerX)[150] = 3.5527501314270691e-15; + (*lowerX)[151] = 5.9604654288605128e-08; + (*lowerX)[152] = 3.5527500255468605e-15; + (*lowerX)[153] = 1.1920930502446e-07; + (*lowerX)[154] = 3.5527498137864448e-15; + (*lowerX)[155] = 2.3841860649616978e-07; + (*lowerX)[156] = 3.5527493902656135e-15; + (*lowerX)[157] = 4.7683720943958926e-07; + (*lowerX)[158] = 3.5527485432239501e-15; + (*lowerX)[159] = 9.5367441532642841e-07; + (*lowerX)[160] = 3.5527468491406226e-15; + (*lowerX)[161] = 1.9073488271001067e-06; + (*lowerX)[162] = 3.5527434609739683e-15; + (*lowerX)[163] = 3.8146976506474625e-06; + (*lowerX)[164] = 3.5527366846406605e-15; + (*lowerX)[165] = 7.6293952977421757e-06; + (*lowerX)[166] = 3.5527231319740448e-15; + (*lowerX)[167] = 1.52587905919316e-05; + (*lowerX)[168] = 3.5526960266408136e-15; + (*lowerX)[169] = 3.0517581180310453e-05; + (*lowerX)[170] = 3.5526418159743506e-15; + (*lowerX)[171] = 6.1035162357068153e-05; + (*lowerX)[172] = 3.5525333946414248e-15; + (*lowerX)[173] = 0.00012207032471058356; + (*lowerX)[174] = 3.5523165519755735e-15; + (*lowerX)[175] = 0.00024414064941761436; + (*lowerX)[176] = 3.5518828666438713e-15; + (*lowerX)[177] = 0.00048828129883167601; + (*lowerX)[178] = 3.551015495980466e-15; + (*lowerX)[179] = 0.0009765625976597993; + (*lowerX)[180] = 3.549280754653656e-15; + (*lowerX)[181] = 0.0019531251953160459; + (*lowerX)[182] = 3.5458112720000354e-15; + (*lowerX)[183] = 0.0039062503906285391; + (*lowerX)[184] = 3.5388723066927948e-15; + (*lowerX)[185] = 0.0078125007812535254; + (*lowerX)[186] = 3.524994376078313e-15; + (*lowerX)[187] = 0.015625001562503498; + (*lowerX)[188] = 3.4972385148493499e-15; + (*lowerX)[189] = 0.031250003125003444; + (*lowerX)[190] = 3.4417267923914238e-15; + (*lowerX)[191] = 0.062500006250003334; + (*lowerX)[192] = 3.3307033474755718e-15; + (*lowerX)[193] = 0.12500001250000312; + (*lowerX)[194] = 3.1086564576438671e-15; + (*lowerX)[195] = 0.25000002500000268; + (*lowerX)[196] = 2.6645626779804573e-15; + (*lowerX)[197] = 0.50000005000000181; + (*lowerX)[198] = 1.7763751186536381e-15; + break; + } + } + + } } @@ -134,6 +343,11 @@ namespace storm { ValueType iterationPrecision = precision; SolverStatus status = SolverStatus::InProgress; + + // DEBUG initialize lower bound to 20 minute result + if(lowerX->size() == 199) { + helper::oviinternal::debug::applyHaddedMonmegeAlwaysEqualResultToLowerBound(lowerX, lowerX->size()); + } while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { @@ -175,7 +389,10 @@ namespace storm { newUpperBoundAlwaysLowerEqual = false; } } - if (newUpperBoundAlwaysHigherEqual) { + if (overallIterations % 10000 == 0 && newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { + std::cout << "[" << overallIterations << "]: All values stayed the same on upper-only / interval verification in OVI.\n"; + } + if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { // All values moved up or stayed the same // That means the guess for an upper bound is actually a lower bound iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); @@ -183,10 +400,11 @@ namespace storm { // Set lowerX to the upper bound candidate std::swap(lowerX, upperX); break; - } else if (newUpperBoundAlwaysLowerEqual) { + } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { // All values moved down or stayed the same and we have a maximum difference of twice the requested precision // We can safely use twice the requested precision, as we calculate the center of both vectors bool reachedPrecision; + std::cout << "\n\nWrongly return in OVI!\n\n"; if (relevantValues) { reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); } else { From f263d9a39fb28aa777846c390773aa1768d956be Mon Sep 17 00:00:00 2001 From: Jan Erik Karuc Date: Sun, 3 May 2020 15:30:05 +0200 Subject: [PATCH 4/8] Remove OVI hm debug elements --- .../helper/OptimisticValueIterationHelper.h | 218 ------------------ 1 file changed, 218 deletions(-) diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index c936638c0..0d905d632 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -82,215 +82,6 @@ namespace storm { storm::utility::vector::applyPointwise(x, target, [&precision] (ValueType const& argument) -> ValueType { return argument + precision; }); } - namespace debug { - template - void applyHaddedMonmegeAlwaysEqualResultToLowerBound(std::vector* lowerX, const int n) { - switch(n) { - case 198: - (*lowerX)[0] = 3.5527502373072761e-15; - (*lowerX)[1] = 3.5527502373072769e-15; - (*lowerX)[2] = 3.5527502373072753e-15; - (*lowerX)[3] = 3.5527502373072785e-15; - (*lowerX)[4] = 3.5527502373072753e-15; - (*lowerX)[5] = 3.5527502373072816e-15; - (*lowerX)[6] = 3.5527502373072753e-15; - (*lowerX)[7] = 3.5527502373072879e-15; - (*lowerX)[8] = 3.5527502373072753e-15; - (*lowerX)[9] = 3.5527502373073006e-15; - (*lowerX)[10] = 3.5527502373072753e-15; - (*lowerX)[11] = 3.5527502373073258e-15; - (*lowerX)[12] = 3.5527502373072753e-15; - (*lowerX)[13] = 3.5527502373073763e-15; - (*lowerX)[14] = 3.5527502373072753e-15; - (*lowerX)[15] = 3.5527502373074773e-15; - (*lowerX)[16] = 3.5527502373072753e-15; - (*lowerX)[17] = 3.5527502373076792e-15; - (*lowerX)[18] = 3.552750237072753e-15; - (*lowerX)[19] = 3.5527502373080831e-15; - (*lowerX)[20] = 3.5527502373072753e-15; - (*lowerX)[21] = 3.5527502373088909e-15; - (*lowerX)[22] = 3.5527502373072753e-15; - (*lowerX)[23] = 3.5527502373105065e-15; - (*lowerX)[24] = 3.5527502373072753e-15; - (*lowerX)[25] = 3.5527502373137377e-15; - (*lowerX)[26] = 3.5527502373072753e-15; - (*lowerX)[27] = 3.5527502373202e-15; - (*lowerX)[28] = 3.5527502373072753e-15; - (*lowerX)[29] = 3.5527502373331247e-15; - (*lowerX)[30] = 3.5527502373072753e-15; - (*lowerX)[31] = 3.5527502373589741e-15; - (*lowerX)[32] = 3.5527502373072753e-15; - (*lowerX)[33] = 3.5527502374106729e-15; - (*lowerX)[34] = 3.5527502373072753e-15; - (*lowerX)[35] = 3.5527502375140705e-15; - (*lowerX)[36] = 3.5527502373072753e-15; - (*lowerX)[37] = 3.5527502377208656e-15; - (*lowerX)[38] = 3.5527502373072753e-15; - (*lowerX)[39] = 3.5527502381344559e-15; - (*lowerX)[40] = 3.5527502373072753e-15; - (*lowerX)[41] = 3.5527502389616373e-15; - (*lowerX)[42] = 3.5527502373072753e-15; - (*lowerX)[43] = 3.5527502406159986e-15; - (*lowerX)[44] = 3.5527502373072753e-15; - (*lowerX)[45] = 3.552750243924721e-15; - (*lowerX)[46] = 3.5527502373072753e-15; - (*lowerX)[47] = 3.5527502505421667e-15; - (*lowerX)[48] = 3.5527502373072753e-15; - (*lowerX)[49] = 3.5527502637770581e-15; - (*lowerX)[50] = 3.5527502373072753e-15; - (*lowerX)[51] = 3.55275029024684e-15; - (*lowerX)[52] = 3.5527502373072753e-15; - (*lowerX)[53] = 3.5527503431864048e-15; - (*lowerX)[54] = 3.5527502373072753e-15; - (*lowerX)[55] = 3.5527504490655334e-15; - (*lowerX)[56] = 3.5527502373072753e-15; - (*lowerX)[57] = 3.5527506608237915e-15; - (*lowerX)[58] = 3.5527502373072753e-15; - (*lowerX)[59] = 3.5527510843403078e-15; - (*lowerX)[60] = 3.5527502373072753e-15; - (*lowerX)[61] = 3.5527519313733394e-15; - (*lowerX)[62] = 3.5527502373072753e-15; - (*lowerX)[63] = 3.5527536254394035e-15; - (*lowerX)[64] = 3.5527502373072753e-15; - (*lowerX)[65] = 3.552757013571531e-15; - (*lowerX)[66] = 3.5527502373072753e-15; - (*lowerX)[67] = 3.5527637898357866e-15; - (*lowerX)[68] = 3.5527502373072753e-15; - (*lowerX)[69] = 3.552777342364298e-15; - (*lowerX)[70] = 3.5527502373072753e-15; - (*lowerX)[71] = 3.5528044474213206e-15; - (*lowerX)[72] = 3.5527502373072753e-15; - (*lowerX)[73] = 3.552858657535366e-15; - (*lowerX)[74] = 3.5527502373072753e-15; - (*lowerX)[75] = 3.5529670777634566e-15; - (*lowerX)[76] = 3.5527502373072753e-15; - (*lowerX)[77] = 3.5531839182196379e-15; - (*lowerX)[78] = 3.5527502373072753e-15; - (*lowerX)[79] = 3.5536175991319998e-15; - (*lowerX)[80] = 3.5527502373072753e-15; - (*lowerX)[81] = 3.554484960956725e-15; - (*lowerX)[82] = 3.5527502373072753e-15; - (*lowerX)[83] = 3.5562196846061739e-15; - (*lowerX)[84] = 3.5527502373072753e-15; - (*lowerX)[85] = 3.5596891319050725e-15; - (*lowerX)[86] = 3.5527502373072753e-15; - (*lowerX)[87] = 3.5666280265028689e-15; - (*lowerX)[88] = 3.5527502373072753e-15; - (*lowerX)[89] = 3.5805058156984624e-15; - (*lowerX)[90] = 3.5527502373072753e-15; - (*lowerX)[91] = 3.6082613940896487e-15; - (*lowerX)[92] = 3.5527502373072753e-15; - (*lowerX)[93] = 3.6637725508720213e-15; - (*lowerX)[94] = 3.5527502373072753e-15; - (*lowerX)[95] = 3.7747948644367674e-15; - (*lowerX)[96] = 3.5527502373072753e-15; - (*lowerX)[97] = 3.9968394915662579e-15; - (*lowerX)[98] = 3.5527502373072737e-15; - (*lowerX)[99] = 4.4409287458252396e-15; - (*lowerX)[100] = 3.5527502373072722e-15; - (*lowerX)[101] = 5.3291072543432039e-15; - (*lowerX)[102] = 3.552750237307269e-15; - (*lowerX)[103] = 7.1054642713791325e-15; - (*lowerX)[104] = 3.5527502373072627e-15; - (*lowerX)[105] = 1.0658178305450988e-14; - (*lowerX)[106] = 3.5527502373072501e-15; - (*lowerX)[107] = 1.7763606373594701e-14; - (*lowerX)[108] = 3.5527502373072248e-15; - (*lowerX)[109] = 3.1974462509882126e-14; - (*lowerX)[110] = 3.5527502373071743e-15; - (*lowerX)[111] = 6.0396174782456978e-14; - (*lowerX)[112] = 3.5527502373070734e-15; - (*lowerX)[113] = 1.1723959932760665e-13; - (*lowerX)[114] = 3.5527502373068714e-15; - (*lowerX)[115] = 2.3092644841790603e-13; - (*lowerX)[116] = 3.5527502373064675e-15; - (*lowerX)[117] = 4.5830014659850484e-13; - (*lowerX)[118] = 3.5527502373056597e-15; - (*lowerX)[119] = 9.1304754295970246e-13; - (*lowerX)[120] = 3.5527502373040441e-15; - (*lowerX)[121] = 1.8225423356820975e-12; - (*lowerX)[122] = 3.552750237300813e-15; - (*lowerX)[123] = 3.641531921126888e-12; - (*lowerX)[124] = 3.5527502372943506e-15; - (*lowerX)[125] = 7.2795110920164697e-12; - (*lowerX)[126] = 3.5527502372814259e-15; - (*lowerX)[127] = 1.4555469433795628e-11; - (*lowerX)[128] = 3.5527502372555765e-15; - (*lowerX)[129] = 2.9107386117353949e-11; - (*lowerX)[130] = 3.5527502372038777e-15; - (*lowerX)[131] = 5.8211219484470597e-11; - (*lowerX)[132] = 3.5527502371004786e-15; - (*lowerX)[133] = 1.1641888621870388e-10; - (*lowerX)[134] = 3.5527502368936819e-15; - (*lowerX)[135] = 2.3283421968717047e-10; - (*lowerX)[136] = 3.5527502364800868e-15; - (*lowerX)[137] = 4.6566488662410365e-10; - (*lowerX)[138] = 3.5527502356528983e-15; - (*lowerX)[139] = 9.3132622049797001e-10; - (*lowerX)[140] = 3.5527502339985197e-15; - (*lowerX)[141] = 1.8626488882457027e-09; - (*lowerX)[142] = 3.5527502306897634e-15; - (*lowerX)[143] = 3.7252942237411686e-09; - (*lowerX)[144] = 3.5527502240722506e-15; - (*lowerX)[145] = 7.4505848947320987e-09; - (*lowerX)[146] = 3.5527502108372251e-15; - (*lowerX)[147] = 1.4901166236713957e-08; - (*lowerX)[148] = 3.5527501843671734e-15; - (*lowerX)[149] = 2.9802328920677681e-08; - (*lowerX)[150] = 3.5527501314270691e-15; - (*lowerX)[151] = 5.9604654288605128e-08; - (*lowerX)[152] = 3.5527500255468605e-15; - (*lowerX)[153] = 1.1920930502446e-07; - (*lowerX)[154] = 3.5527498137864448e-15; - (*lowerX)[155] = 2.3841860649616978e-07; - (*lowerX)[156] = 3.5527493902656135e-15; - (*lowerX)[157] = 4.7683720943958926e-07; - (*lowerX)[158] = 3.5527485432239501e-15; - (*lowerX)[159] = 9.5367441532642841e-07; - (*lowerX)[160] = 3.5527468491406226e-15; - (*lowerX)[161] = 1.9073488271001067e-06; - (*lowerX)[162] = 3.5527434609739683e-15; - (*lowerX)[163] = 3.8146976506474625e-06; - (*lowerX)[164] = 3.5527366846406605e-15; - (*lowerX)[165] = 7.6293952977421757e-06; - (*lowerX)[166] = 3.5527231319740448e-15; - (*lowerX)[167] = 1.52587905919316e-05; - (*lowerX)[168] = 3.5526960266408136e-15; - (*lowerX)[169] = 3.0517581180310453e-05; - (*lowerX)[170] = 3.5526418159743506e-15; - (*lowerX)[171] = 6.1035162357068153e-05; - (*lowerX)[172] = 3.5525333946414248e-15; - (*lowerX)[173] = 0.00012207032471058356; - (*lowerX)[174] = 3.5523165519755735e-15; - (*lowerX)[175] = 0.00024414064941761436; - (*lowerX)[176] = 3.5518828666438713e-15; - (*lowerX)[177] = 0.00048828129883167601; - (*lowerX)[178] = 3.551015495980466e-15; - (*lowerX)[179] = 0.0009765625976597993; - (*lowerX)[180] = 3.549280754653656e-15; - (*lowerX)[181] = 0.0019531251953160459; - (*lowerX)[182] = 3.5458112720000354e-15; - (*lowerX)[183] = 0.0039062503906285391; - (*lowerX)[184] = 3.5388723066927948e-15; - (*lowerX)[185] = 0.0078125007812535254; - (*lowerX)[186] = 3.524994376078313e-15; - (*lowerX)[187] = 0.015625001562503498; - (*lowerX)[188] = 3.4972385148493499e-15; - (*lowerX)[189] = 0.031250003125003444; - (*lowerX)[190] = 3.4417267923914238e-15; - (*lowerX)[191] = 0.062500006250003334; - (*lowerX)[192] = 3.3307033474755718e-15; - (*lowerX)[193] = 0.12500001250000312; - (*lowerX)[194] = 3.1086564576438671e-15; - (*lowerX)[195] = 0.25000002500000268; - (*lowerX)[196] = 2.6645626779804573e-15; - (*lowerX)[197] = 0.50000005000000181; - (*lowerX)[198] = 1.7763751186536381e-15; - break; - } - } - - } } @@ -343,11 +134,6 @@ namespace storm { ValueType iterationPrecision = precision; SolverStatus status = SolverStatus::InProgress; - - // DEBUG initialize lower bound to 20 minute result - if(lowerX->size() == 199) { - helper::oviinternal::debug::applyHaddedMonmegeAlwaysEqualResultToLowerBound(lowerX, lowerX->size()); - } while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { @@ -389,9 +175,6 @@ namespace storm { newUpperBoundAlwaysLowerEqual = false; } } - if (overallIterations % 10000 == 0 && newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { - std::cout << "[" << overallIterations << "]: All values stayed the same on upper-only / interval verification in OVI.\n"; - } if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { // All values moved up or stayed the same // That means the guess for an upper bound is actually a lower bound @@ -404,7 +187,6 @@ namespace storm { // All values moved down or stayed the same and we have a maximum difference of twice the requested precision // We can safely use twice the requested precision, as we calculate the center of both vectors bool reachedPrecision; - std::cout << "\n\nWrongly return in OVI!\n\n"; if (relevantValues) { reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); } else { From 6cfb2be36dd04c28f1e1ca8153c6869c84447364 Mon Sep 17 00:00:00 2001 From: Jan Erik Karuc Date: Thu, 28 May 2020 18:37:09 +0200 Subject: [PATCH 5/8] Preparation for minimum upper and aux benchmarking This temporary option has not yet been implemented in OVI --- src/storm/environment/solver/OviSolverEnvironment.cpp | 5 +++++ src/storm/environment/solver/OviSolverEnvironment.h | 2 ++ src/storm/settings/modules/OviSolverSettings.cpp | 9 ++++++++- src/storm/settings/modules/OviSolverSettings.h | 4 +++- src/storm/solver/helper/OptimisticValueIterationHelper.h | 9 +++++---- 5 files changed, 23 insertions(+), 6 deletions(-) diff --git a/src/storm/environment/solver/OviSolverEnvironment.cpp b/src/storm/environment/solver/OviSolverEnvironment.cpp index a5007aa78..f1e8e1b5b 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.cpp +++ b/src/storm/environment/solver/OviSolverEnvironment.cpp @@ -14,6 +14,7 @@ namespace storm { relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate(); upperBoundGuessingFactor = storm::utility::convertNumber(oviSettings.getUpperBoundGuessingFactor()); upperBoundOnlyIterations = oviSettings.getUpperBoundOnlyIterations(); + useTerminationGuaranteedMinimumMethod = oviSettings.getUseTerminationGuaranteedMinimumMethod(); } OviSolverEnvironment::~OviSolverEnvironment() { @@ -39,5 +40,9 @@ namespace storm { uint64_t OviSolverEnvironment::getUpperBoundOnlyIterations() const { return upperBoundOnlyIterations; } + + bool OviSolverEnvironment::getUseTerminationGuaranteedMinimumMethod() const { + return useTerminationGuaranteedMinimumMethod; + } } diff --git a/src/storm/environment/solver/OviSolverEnvironment.h b/src/storm/environment/solver/OviSolverEnvironment.h index 74a99e518..7b0fa4d8e 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.h +++ b/src/storm/environment/solver/OviSolverEnvironment.h @@ -17,6 +17,7 @@ namespace storm { bool useRelevantValuesForPrecisionUpdate() const; storm::RationalNumber getUpperBoundGuessingFactor() const; uint64_t getUpperBoundOnlyIterations() const; + bool getUseTerminationGuaranteedMinimumMethod() const; private: storm::RationalNumber precisionUpdateFactor; @@ -24,6 +25,7 @@ namespace storm { bool relevantValuesForPrecisionUpdate; storm::RationalNumber upperBoundGuessingFactor; uint64_t upperBoundOnlyIterations; + bool useTerminationGuaranteedMinimumMethod; }; } diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index c617db06f..8f117365c 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -17,7 +17,8 @@ namespace storm { const std::string OviSolverSettings::useRelevantValuesForPrecisionUpdateOptionName = "use-relevant-values"; const std::string OviSolverSettings::upperBoundGuessingFactorOptionName = "upper-bound-factor"; const std::string OviSolverSettings::upperBoundOnlyIterationsOptionName = "check-upper-only-iter"; - + const std::string OviSolverSettings::useTerminationGuaranteedMinimumMethodOptionName = "termination-guarantee"; + OviSolverSettings::OviSolverSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, precisionUpdateFactorOptionName, false, "Sets with which factor the precision of the inner value iteration is updated.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(0.4).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); @@ -29,6 +30,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, upperBoundGuessingFactorOptionName, false, "Sets with which factor the precision is multiplied to guess the upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(1.0).addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, upperBoundOnlyIterationsOptionName, false, "Sets the max. iterations OVI will only iterate over the upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createIntegerArgument("iter", "The iterations.").setDefaultValueInteger(20000).addValidatorInteger(ArgumentValidatorFactory::createIntegerGreaterValidator(0)).build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, useTerminationGuaranteedMinimumMethodOptionName, false, "Sets whether to perform calculations on element-wise minimum of iterated and old upper bound.").setIsAdvanced().build()); } double OviSolverSettings::getPrecisionUpdateFactor() const { @@ -50,6 +53,10 @@ namespace storm { uint64_t OviSolverSettings::getUpperBoundOnlyIterations() const { return this->getOption(upperBoundOnlyIterationsOptionName).getArgumentByName("iter").getValueAsInteger(); } + + bool OviSolverSettings::getUseTerminationGuaranteedMinimumMethod() const { + return this->getOption(useTerminationGuaranteedMinimumMethodOptionName).getHasOptionBeenSet(); + } } } diff --git a/src/storm/settings/modules/OviSolverSettings.h b/src/storm/settings/modules/OviSolverSettings.h index 21884169d..718a646d5 100644 --- a/src/storm/settings/modules/OviSolverSettings.h +++ b/src/storm/settings/modules/OviSolverSettings.h @@ -24,7 +24,8 @@ namespace storm { double getUpperBoundGuessingFactor() const; uint64_t getUpperBoundOnlyIterations() const; - + + bool getUseTerminationGuaranteedMinimumMethod() const; // The name of the module. static const std::string moduleName; @@ -35,6 +36,7 @@ namespace storm { static const std::string useRelevantValuesForPrecisionUpdateOptionName; static const std::string upperBoundGuessingFactorOptionName; static const std::string upperBoundOnlyIterationsOptionName; + static const std::string useTerminationGuaranteedMinimumMethodOptionName; }; } diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 0d905d632..5ebd9c14e 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -163,16 +163,17 @@ namespace storm { // Upper bound iteration singleIterationCallback(upperX, auxVector, overallIterations); - // At this point, auxVector contains the old values for the upper bound whereas upperX contains the new ones. + // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. // Compare the new upper bound candidate with the old one bool newUpperBoundAlwaysHigherEqual = true; bool newUpperBoundAlwaysLowerEqual = true; for (uint64_t i = 0; i < upperX->size(); ++i) { - if ((*auxVector)[i] > (*upperX)[i]) { - newUpperBoundAlwaysHigherEqual = false; - } else if ((*auxVector)[i] != (*upperX)[i]) { + if ((*upperX)[i] < (*auxVector)[i]) { + newUpperBoundAlwaysHigherEqual = false; + } else if ((*upperX)[i] != (*auxVector)[i]) { newUpperBoundAlwaysLowerEqual = false; + //std::swap((*upperX)[i], (*auxVector)[i]); } } if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { From bff888a97e8c6771a070d1cb9978dbedaee06c74 Mon Sep 17 00:00:00 2001 From: Jan Erik Karuc Date: Thu, 28 May 2020 20:58:58 +0200 Subject: [PATCH 6/8] Renaming min upper aux method setting --- src/storm/environment/solver/OviSolverEnvironment.cpp | 8 ++++---- src/storm/environment/solver/OviSolverEnvironment.h | 4 ++-- src/storm/settings/modules/OviSolverSettings.cpp | 2 +- src/storm/settings/modules/OviSolverSettings.h | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/storm/environment/solver/OviSolverEnvironment.cpp b/src/storm/environment/solver/OviSolverEnvironment.cpp index f1e8e1b5b..dba37846e 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.cpp +++ b/src/storm/environment/solver/OviSolverEnvironment.cpp @@ -14,7 +14,7 @@ namespace storm { relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate(); upperBoundGuessingFactor = storm::utility::convertNumber(oviSettings.getUpperBoundGuessingFactor()); upperBoundOnlyIterations = oviSettings.getUpperBoundOnlyIterations(); - useTerminationGuaranteedMinimumMethod = oviSettings.getUseTerminationGuaranteedMinimumMethod(); + terminationGuaranteedMinimumMethod = oviSettings.useTerminationGuaranteedMinimumMethod(); } OviSolverEnvironment::~OviSolverEnvironment() { @@ -34,15 +34,15 @@ namespace storm { } storm::RationalNumber OviSolverEnvironment::getUpperBoundGuessingFactor() const { - return maxVerificationIterationFactor; + return upperBoundGuessingFactor; } uint64_t OviSolverEnvironment::getUpperBoundOnlyIterations() const { return upperBoundOnlyIterations; } - bool OviSolverEnvironment::getUseTerminationGuaranteedMinimumMethod() const { - return useTerminationGuaranteedMinimumMethod; + bool OviSolverEnvironment::useTerminationGuaranteedMinimumMethod() const { + return terminationGuaranteedMinimumMethod; } } diff --git a/src/storm/environment/solver/OviSolverEnvironment.h b/src/storm/environment/solver/OviSolverEnvironment.h index 7b0fa4d8e..f75985924 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.h +++ b/src/storm/environment/solver/OviSolverEnvironment.h @@ -17,7 +17,7 @@ namespace storm { bool useRelevantValuesForPrecisionUpdate() const; storm::RationalNumber getUpperBoundGuessingFactor() const; uint64_t getUpperBoundOnlyIterations() const; - bool getUseTerminationGuaranteedMinimumMethod() const; + bool useTerminationGuaranteedMinimumMethod() const; private: storm::RationalNumber precisionUpdateFactor; @@ -25,7 +25,7 @@ namespace storm { bool relevantValuesForPrecisionUpdate; storm::RationalNumber upperBoundGuessingFactor; uint64_t upperBoundOnlyIterations; - bool useTerminationGuaranteedMinimumMethod; + bool terminationGuaranteedMinimumMethod; }; } diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index 8f117365c..7c34b69dc 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -54,7 +54,7 @@ namespace storm { return this->getOption(upperBoundOnlyIterationsOptionName).getArgumentByName("iter").getValueAsInteger(); } - bool OviSolverSettings::getUseTerminationGuaranteedMinimumMethod() const { + bool OviSolverSettings::useTerminationGuaranteedMinimumMethod() const { return this->getOption(useTerminationGuaranteedMinimumMethodOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/OviSolverSettings.h b/src/storm/settings/modules/OviSolverSettings.h index 718a646d5..2e5934350 100644 --- a/src/storm/settings/modules/OviSolverSettings.h +++ b/src/storm/settings/modules/OviSolverSettings.h @@ -25,7 +25,7 @@ namespace storm { uint64_t getUpperBoundOnlyIterations() const; - bool getUseTerminationGuaranteedMinimumMethod() const; + bool useTerminationGuaranteedMinimumMethod() const; // The name of the module. static const std::string moduleName; From 48a3b5a9270c0688519eb723816236f84c2679f5 Mon Sep 17 00:00:00 2001 From: Jan Erik Karuc Date: Thu, 28 May 2020 20:59:42 +0200 Subject: [PATCH 7/8] Optimizing original OVI & Switch for comparing minswap methods --- .../helper/OptimisticValueIterationHelper.h | 289 +++++++++++++----- 1 file changed, 206 insertions(+), 83 deletions(-) diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 5ebd9c14e..5d9dc8b34 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -135,99 +135,222 @@ namespace storm { SolverStatus status = SolverStatus::InProgress; - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - - // Perform value iteration until convergence - ++valueIterationInvocations; - auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); - lastValueIterationIterations = result.iterations; - overallIterations += result.iterations; - - if (result.status != SolverStatus::Converged) { - status = result.status; - } else { - bool intervalIterationNeeded = false; - currentVerificationIterations = 0; - - if (relative) { - oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); + if(env.solver().ovi().useTerminationGuaranteedMinimumMethod()) { + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + + // Perform value iteration until convergence + ++valueIterationInvocations; + auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); + lastValueIterationIterations = result.iterations; + overallIterations += result.iterations; + + if (result.status != SolverStatus::Converged) { + status = result.status; } else { - oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); - } - - bool cancelGuess = false; - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - ++overallIterations; - ++currentVerificationIterations; - // Perform value iteration stepwise for lower bound and guessed upper bound - - // Upper bound iteration - singleIterationCallback(upperX, auxVector, overallIterations); - // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. - - // Compare the new upper bound candidate with the old one - bool newUpperBoundAlwaysHigherEqual = true; - bool newUpperBoundAlwaysLowerEqual = true; - for (uint64_t i = 0; i < upperX->size(); ++i) { - if ((*upperX)[i] < (*auxVector)[i]) { - newUpperBoundAlwaysHigherEqual = false; - } else if ((*upperX)[i] != (*auxVector)[i]) { - newUpperBoundAlwaysLowerEqual = false; - //std::swap((*upperX)[i], (*auxVector)[i]); - } + bool intervalIterationNeeded = false; + currentVerificationIterations = 0; + + if (relative) { + oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); + } else { + oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); } - if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { - // All values moved up or stayed the same - // That means the guess for an upper bound is actually a lower bound - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); - // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound - // Set lowerX to the upper bound candidate - std::swap(lowerX, upperX); - break; - } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { - // All values moved down or stayed the same and we have a maximum difference of twice the requested precision - // We can safely use twice the requested precision, as we calculate the center of both vectors - bool reachedPrecision; - if (relevantValues) { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); - } else { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); + + bool cancelGuess = false; + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + ++overallIterations; + ++currentVerificationIterations; + // Perform value iteration stepwise for lower bound and guessed upper bound + + // Upper bound iteration + singleIterationCallback(upperX, auxVector, overallIterations); + // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. + + // Compare the new upper bound candidate with the old one + bool newUpperBoundAlwaysHigherEqual = true; + bool newUpperBoundAlwaysLowerEqual = true; + for (uint64_t i = 0; i < upperX->size(); ++i) { + if ((*upperX)[i] < (*auxVector)[i]) { + newUpperBoundAlwaysHigherEqual = false; + } else if ((*upperX)[i] != (*auxVector)[i]) { + newUpperBoundAlwaysLowerEqual = false; + std::swap((*upperX)[i], (*auxVector)[i]); + } } - if (reachedPrecision) { - status = SolverStatus::Converged; + + if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { + // All values moved up or stayed the same + // That means the guess for an upper bound is actually a lower bound + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); + // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound + // Set lowerX to the upper bound candidate + std::swap(lowerX, upperX); break; - } else { - // From now on, we keep updating both bounds - intervalIterationNeeded = true; + } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { + // All values moved down or stayed the same and we have a maximum difference of twice the requested precision + // We can safely use twice the requested precision, as we calculate the center of both vectors + bool reachedPrecision; + if (relevantValues) { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); + } else { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); + } + if (reachedPrecision) { + status = SolverStatus::Converged; + break; + } else { + // From now on, we keep updating both bounds + intervalIterationNeeded = true; + } + } + // At this point, the old upper bounds (auxVector) are not needed anymore. + + // Check whether we tried this guess for too long + ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); + if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { + cancelGuess = true; + // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + } + + // Lower bound iteration (only if needed) + if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { + singleIterationCallback(lowerX, auxVector, overallIterations); + // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. + + // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. + bool valuesCrossed = false; + for (uint64_t i = 0; i < lowerX->size(); ++i) { + if ((*upperX)[i] < (*lowerX)[i]) { + valuesCrossed = true; + break; + } + } + + if (cancelGuess || valuesCrossed) { + // A new guess is needed. + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + break; + } } } - // At this point, the old upper bounds (auxVector) are not needed anymore. - - // Check whether we tried this guess for too long - ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); - if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { - cancelGuess = true; - // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + } + } + } + else { + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + + // Perform value iteration until convergence + ++valueIterationInvocations; + auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); + lastValueIterationIterations = result.iterations; + overallIterations += result.iterations; + + if (result.status != SolverStatus::Converged) { + status = result.status; + } else { + bool intervalIterationNeeded = false; + currentVerificationIterations = 0; + + if (relative) { + oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); + } else { + oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); } - - // Lower bound iteration (only if needed) - if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { - singleIterationCallback(lowerX, auxVector, overallIterations); - // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. - - // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. - bool valuesCrossed = false; - for (uint64_t i = 0; i < lowerX->size(); ++i) { - if ((*upperX)[i] < (*lowerX)[i]) { - valuesCrossed = true; - break; + + bool cancelGuess = false; + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + ++overallIterations; + ++currentVerificationIterations; + // Perform value iteration stepwise for lower bound and guessed upper bound + + // Upper bound iteration + singleIterationCallback(upperX, auxVector, overallIterations); + + // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. + + // Compare the new upper bound candidate with the old one + bool newUpperBoundAlwaysHigherEqual = true; + bool newUpperBoundAlwaysLowerEqual = true; + bool cancelOuterScan = false; + for (uint64_t i = 0; i < upperX->size() &! cancelOuterScan; ++i) { + if ((*upperX)[i] < (*auxVector)[i]) { + newUpperBoundAlwaysHigherEqual = false; + ++i; + while (i < upperX->size()) { + if ((*upperX)[i] > (*auxVector)[i]) { + newUpperBoundAlwaysLowerEqual = false; + cancelOuterScan = true; + break; + } + ++i; + } + } else if ((*upperX)[i] != (*auxVector)[i]) { + newUpperBoundAlwaysLowerEqual = false; + ++i; + while (i < upperX->size()) { + if ((*upperX)[i] > (*auxVector)[i]) { + newUpperBoundAlwaysLowerEqual = false; + cancelOuterScan = true; + break; + } + ++i; + } } } - - if (cancelGuess || valuesCrossed) { - // A new guess is needed. - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + + if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { + // All values moved up or stayed the same + // That means the guess for an upper bound is actually a lower bound + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); + // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound + // Set lowerX to the upper bound candidate + std::swap(lowerX, upperX); break; + } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { + // All values moved down or stayed the same and we have a maximum difference of twice the requested precision + // We can safely use twice the requested precision, as we calculate the center of both vectors + bool reachedPrecision; + if (relevantValues) { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); + } else { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); + } + if (reachedPrecision) { + status = SolverStatus::Converged; + break; + } else { + // From now on, we keep updating both bounds + intervalIterationNeeded = true; + } + } + // At this point, the old upper bounds (auxVector) are not needed anymore. + + // Check whether we tried this guess for too long + ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); + if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { + cancelGuess = true; + // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + } + + // Lower bound iteration (only if needed) + if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { + singleIterationCallback(lowerX, auxVector, overallIterations); + // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. + + // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. + bool valuesCrossed = false; + for (uint64_t i = 0; i < lowerX->size(); ++i) { + if ((*upperX)[i] < (*lowerX)[i]) { + valuesCrossed = true; + break; + } + } + + if (cancelGuess || valuesCrossed) { + // A new guess is needed. + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + break; + } } } } From 6c70b42549cd5d4e8f3b083f286730072a103cbb Mon Sep 17 00:00:00 2001 From: Jan Erik Karuc Date: Sun, 26 Jul 2020 13:14:18 +0200 Subject: [PATCH 8/8] OVI: Defaulting to M1/M2, changed CLI option for termination guarantee Adapted CLI option description --- .../solver/OviSolverEnvironment.cpp | 6 +- .../environment/solver/OviSolverEnvironment.h | 4 +- .../settings/modules/OviSolverSettings.cpp | 8 +- .../settings/modules/OviSolverSettings.h | 4 +- .../helper/OptimisticValueIterationHelper.h | 262 ++++++------------ 5 files changed, 97 insertions(+), 187 deletions(-) diff --git a/src/storm/environment/solver/OviSolverEnvironment.cpp b/src/storm/environment/solver/OviSolverEnvironment.cpp index dba37846e..fe6a21a12 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.cpp +++ b/src/storm/environment/solver/OviSolverEnvironment.cpp @@ -14,7 +14,7 @@ namespace storm { relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate(); upperBoundGuessingFactor = storm::utility::convertNumber(oviSettings.getUpperBoundGuessingFactor()); upperBoundOnlyIterations = oviSettings.getUpperBoundOnlyIterations(); - terminationGuaranteedMinimumMethod = oviSettings.useTerminationGuaranteedMinimumMethod(); + noTerminationGuaranteeMinimumMethod = oviSettings.useNoTerminationGuaranteeMinimumMethod(); } OviSolverEnvironment::~OviSolverEnvironment() { @@ -41,8 +41,8 @@ namespace storm { return upperBoundOnlyIterations; } - bool OviSolverEnvironment::useTerminationGuaranteedMinimumMethod() const { - return terminationGuaranteedMinimumMethod; + bool OviSolverEnvironment::useNoTerminationGuaranteeMinimumMethod() const { + return noTerminationGuaranteeMinimumMethod; } } diff --git a/src/storm/environment/solver/OviSolverEnvironment.h b/src/storm/environment/solver/OviSolverEnvironment.h index f75985924..0875bad9a 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.h +++ b/src/storm/environment/solver/OviSolverEnvironment.h @@ -17,7 +17,7 @@ namespace storm { bool useRelevantValuesForPrecisionUpdate() const; storm::RationalNumber getUpperBoundGuessingFactor() const; uint64_t getUpperBoundOnlyIterations() const; - bool useTerminationGuaranteedMinimumMethod() const; + bool useNoTerminationGuaranteeMinimumMethod() const; private: storm::RationalNumber precisionUpdateFactor; @@ -25,7 +25,7 @@ namespace storm { bool relevantValuesForPrecisionUpdate; storm::RationalNumber upperBoundGuessingFactor; uint64_t upperBoundOnlyIterations; - bool terminationGuaranteedMinimumMethod; + bool noTerminationGuaranteeMinimumMethod; }; } diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index 7c34b69dc..46cc82f36 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -17,7 +17,7 @@ namespace storm { const std::string OviSolverSettings::useRelevantValuesForPrecisionUpdateOptionName = "use-relevant-values"; const std::string OviSolverSettings::upperBoundGuessingFactorOptionName = "upper-bound-factor"; const std::string OviSolverSettings::upperBoundOnlyIterationsOptionName = "check-upper-only-iter"; - const std::string OviSolverSettings::useTerminationGuaranteedMinimumMethodOptionName = "termination-guarantee"; + const std::string OviSolverSettings::useNoTerminationGuaranteeMinimumMethodOptionName = "no-termination-guarantee"; OviSolverSettings::OviSolverSettings() : ModuleSettings(moduleName) { @@ -31,7 +31,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, upperBoundOnlyIterationsOptionName, false, "Sets the max. iterations OVI will only iterate over the upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createIntegerArgument("iter", "The iterations.").setDefaultValueInteger(20000).addValidatorInteger(ArgumentValidatorFactory::createIntegerGreaterValidator(0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, useTerminationGuaranteedMinimumMethodOptionName, false, "Sets whether to perform calculations on element-wise minimum of iterated and old upper bound.").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, useNoTerminationGuaranteeMinimumMethodOptionName, false, "Sets whether to perform element-wise minimum of iterated and old upper bound. If this option is set, that will be skipped, slightly increasing performance but giving no termination guarantee.").setShortName("ntg").setIsAdvanced().build()); } double OviSolverSettings::getPrecisionUpdateFactor() const { @@ -54,8 +54,8 @@ namespace storm { return this->getOption(upperBoundOnlyIterationsOptionName).getArgumentByName("iter").getValueAsInteger(); } - bool OviSolverSettings::useTerminationGuaranteedMinimumMethod() const { - return this->getOption(useTerminationGuaranteedMinimumMethodOptionName).getHasOptionBeenSet(); + bool OviSolverSettings::useNoTerminationGuaranteeMinimumMethod() const { + return this->getOption(useNoTerminationGuaranteeMinimumMethodOptionName).getHasOptionBeenSet(); } } diff --git a/src/storm/settings/modules/OviSolverSettings.h b/src/storm/settings/modules/OviSolverSettings.h index 2e5934350..70c1c4f0f 100644 --- a/src/storm/settings/modules/OviSolverSettings.h +++ b/src/storm/settings/modules/OviSolverSettings.h @@ -25,7 +25,7 @@ namespace storm { uint64_t getUpperBoundOnlyIterations() const; - bool useTerminationGuaranteedMinimumMethod() const; + bool useNoTerminationGuaranteeMinimumMethod() const; // The name of the module. static const std::string moduleName; @@ -36,7 +36,7 @@ namespace storm { static const std::string useRelevantValuesForPrecisionUpdateOptionName; static const std::string upperBoundGuessingFactorOptionName; static const std::string upperBoundOnlyIterationsOptionName; - static const std::string useTerminationGuaranteedMinimumMethodOptionName; + static const std::string useNoTerminationGuaranteeMinimumMethodOptionName; }; } diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 5d9dc8b34..8bb6a3cca 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -121,6 +121,8 @@ namespace storm { ValueType two = storm::utility::convertNumber(2.0); // Relative errors bool relative = env.solver().minMax().getRelativeTerminationCriterion(); + // Use no termination guaranteed upper bound iteration method + bool noTerminationGuarantee = env.solver().ovi().useNoTerminationGuaranteeMinimumMethod(); // Goal precision ValueType precision = storm::utility::convertNumber(env.solver().minMax().getPrecision()); // Desired max difference between upperX and lowerX @@ -135,142 +137,40 @@ namespace storm { SolverStatus status = SolverStatus::InProgress; - if(env.solver().ovi().useTerminationGuaranteedMinimumMethod()) { - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - // Perform value iteration until convergence - ++valueIterationInvocations; - auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); - lastValueIterationIterations = result.iterations; - overallIterations += result.iterations; + // Perform value iteration until convergence + ++valueIterationInvocations; + auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); + lastValueIterationIterations = result.iterations; + overallIterations += result.iterations; - if (result.status != SolverStatus::Converged) { - status = result.status; - } else { - bool intervalIterationNeeded = false; - currentVerificationIterations = 0; - - if (relative) { - oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); - } else { - oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); - } - - bool cancelGuess = false; - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - ++overallIterations; - ++currentVerificationIterations; - // Perform value iteration stepwise for lower bound and guessed upper bound - - // Upper bound iteration - singleIterationCallback(upperX, auxVector, overallIterations); - // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. - - // Compare the new upper bound candidate with the old one - bool newUpperBoundAlwaysHigherEqual = true; - bool newUpperBoundAlwaysLowerEqual = true; - for (uint64_t i = 0; i < upperX->size(); ++i) { - if ((*upperX)[i] < (*auxVector)[i]) { - newUpperBoundAlwaysHigherEqual = false; - } else if ((*upperX)[i] != (*auxVector)[i]) { - newUpperBoundAlwaysLowerEqual = false; - std::swap((*upperX)[i], (*auxVector)[i]); - } - } - - if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { - // All values moved up or stayed the same - // That means the guess for an upper bound is actually a lower bound - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); - // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound - // Set lowerX to the upper bound candidate - std::swap(lowerX, upperX); - break; - } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { - // All values moved down or stayed the same and we have a maximum difference of twice the requested precision - // We can safely use twice the requested precision, as we calculate the center of both vectors - bool reachedPrecision; - if (relevantValues) { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); - } else { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); - } - if (reachedPrecision) { - status = SolverStatus::Converged; - break; - } else { - // From now on, we keep updating both bounds - intervalIterationNeeded = true; - } - } - // At this point, the old upper bounds (auxVector) are not needed anymore. - - // Check whether we tried this guess for too long - ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); - if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { - cancelGuess = true; - // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) - } - - // Lower bound iteration (only if needed) - if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { - singleIterationCallback(lowerX, auxVector, overallIterations); - // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. - - // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. - bool valuesCrossed = false; - for (uint64_t i = 0; i < lowerX->size(); ++i) { - if ((*upperX)[i] < (*lowerX)[i]) { - valuesCrossed = true; - break; - } - } - - if (cancelGuess || valuesCrossed) { - // A new guess is needed. - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); - break; - } - } - } - } - } - } - else { - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - - // Perform value iteration until convergence - ++valueIterationInvocations; - auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); - lastValueIterationIterations = result.iterations; - overallIterations += result.iterations; + if (result.status != SolverStatus::Converged) { + status = result.status; + } else { + bool intervalIterationNeeded = false; + currentVerificationIterations = 0; - if (result.status != SolverStatus::Converged) { - status = result.status; + if (relative) { + oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); } else { - bool intervalIterationNeeded = false; - currentVerificationIterations = 0; - - if (relative) { - oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); - } else { - oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); - } - - bool cancelGuess = false; - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - ++overallIterations; - ++currentVerificationIterations; - // Perform value iteration stepwise for lower bound and guessed upper bound + oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); + } - // Upper bound iteration - singleIterationCallback(upperX, auxVector, overallIterations); + bool cancelGuess = false; + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + ++overallIterations; + ++currentVerificationIterations; + // Perform value iteration stepwise for lower bound and guessed upper bound - // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. + // Upper bound iteration + singleIterationCallback(upperX, auxVector, overallIterations); + // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. - // Compare the new upper bound candidate with the old one - bool newUpperBoundAlwaysHigherEqual = true; - bool newUpperBoundAlwaysLowerEqual = true; + // Compare the new upper bound candidate with the old one + bool newUpperBoundAlwaysHigherEqual = true; + bool newUpperBoundAlwaysLowerEqual = true; + if(noTerminationGuarantee) { bool cancelOuterScan = false; for (uint64_t i = 0; i < upperX->size() &! cancelOuterScan; ++i) { if ((*upperX)[i] < (*auxVector)[i]) { @@ -288,8 +188,8 @@ namespace storm { newUpperBoundAlwaysLowerEqual = false; ++i; while (i < upperX->size()) { - if ((*upperX)[i] > (*auxVector)[i]) { - newUpperBoundAlwaysLowerEqual = false; + if ((*upperX)[i] < (*auxVector)[i]) { + newUpperBoundAlwaysHigherEqual = false; cancelOuterScan = true; break; } @@ -297,61 +197,71 @@ namespace storm { } } } - - if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { - // All values moved up or stayed the same - // That means the guess for an upper bound is actually a lower bound - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); - // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound - // Set lowerX to the upper bound candidate - std::swap(lowerX, upperX); - break; - } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { - // All values moved down or stayed the same and we have a maximum difference of twice the requested precision - // We can safely use twice the requested precision, as we calculate the center of both vectors - bool reachedPrecision; - if (relevantValues) { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); - } else { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); - } - if (reachedPrecision) { - status = SolverStatus::Converged; - break; - } else { - // From now on, we keep updating both bounds - intervalIterationNeeded = true; + } + else { + for (uint64_t i = 0; i < upperX->size(); ++i) { + if ((*upperX)[i] < (*auxVector)[i]) { + newUpperBoundAlwaysHigherEqual = false; + } else if ((*upperX)[i] != (*auxVector)[i]) { + newUpperBoundAlwaysLowerEqual = false; + std::swap((*upperX)[i], (*auxVector)[i]); } } - // At this point, the old upper bounds (auxVector) are not needed anymore. + } - // Check whether we tried this guess for too long - ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); - if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { - cancelGuess = true; - // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { + // All values moved up or stayed the same + // That means the guess for an upper bound is actually a lower bound + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); + // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound + // Set lowerX to the upper bound candidate + std::swap(lowerX, upperX); + break; + } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { + // All values moved down or stayed the same and we have a maximum difference of twice the requested precision + // We can safely use twice the requested precision, as we calculate the center of both vectors + bool reachedPrecision; + if (relevantValues) { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); + } else { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); + } + if (reachedPrecision) { + status = SolverStatus::Converged; + break; + } else { + // From now on, we keep updating both bounds + intervalIterationNeeded = true; } + } + // At this point, the old upper bounds (auxVector) are not needed anymore. - // Lower bound iteration (only if needed) - if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { - singleIterationCallback(lowerX, auxVector, overallIterations); - // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. + // Check whether we tried this guess for too long + ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); + if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { + cancelGuess = true; + // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + } - // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. - bool valuesCrossed = false; - for (uint64_t i = 0; i < lowerX->size(); ++i) { - if ((*upperX)[i] < (*lowerX)[i]) { - valuesCrossed = true; - break; - } - } + // Lower bound iteration (only if needed) + if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { + singleIterationCallback(lowerX, auxVector, overallIterations); + // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. - if (cancelGuess || valuesCrossed) { - // A new guess is needed. - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. + bool valuesCrossed = false; + for (uint64_t i = 0; i < lowerX->size(); ++i) { + if ((*upperX)[i] < (*lowerX)[i]) { + valuesCrossed = true; break; } } + + if (cancelGuess || valuesCrossed) { + // A new guess is needed. + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + break; + } } } }