From 778a4fc71b96775bf420590f375c3d7f6031d0c7 Mon Sep 17 00:00:00 2001 From: Jan Erik Karuc Date: Thu, 30 Apr 2020 21:12:50 +0200 Subject: [PATCH] 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 {