150TYPED_TEST(GradientDescentInstantiationSearcherTest, Crowds) {
151 std::string programFile = STORM_TEST_RESOURCES_DIR
"/pdtmc/crowds3_5.pm";
152 std::string formulaAsString =
"P<=0.00000001 [F \"observe0Greater1\"]";
153 std::string constantsAsString =
"";
158 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
160 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
164 ASSERT_TRUE(simplifier.simplify(*formulas[0]));
165 model = simplifier.getSimplifiedModel();
169 std::shared_ptr<storm::logic::Formula> formulaWithoutBounds = formulas[0]->clone();
170 std::shared_ptr<storm::logic::Formula const> formulaNoBound = formulaWithoutBounds->asSharedPointer();
171 std::shared_ptr<FeasibilitySynthesisTask> t = std::make_shared<FeasibilitySynthesisTask>(formulaNoBound);
172 t->setBound(formulas[0]->asOperatorFormula().getBound());
173 std::shared_ptr<FeasibilitySynthesisTask const> feasibilityTask = std::make_shared<FeasibilitySynthesisTask const>(std::move(*t));
182 adamChecker.
setup(this->env(), feasibilityTask);
186 carl::Variable badCVar;
187 carl::Variable pfVar;
189 if (parameter.name() ==
"badC") {
191 }
else if (parameter.name() ==
"PF") {
195 std::shared_ptr<storm::RawPolynomialCache> cache = std::make_shared<storm::RawPolynomialCache>();
199 const double badCValues[] = {0.5,
239 0.07072017341852188};
240 const double pfValues[] = {0.5,
280 0.10981585085391998};
282 for (uint_fast64_t i = 0; i < 41; i++) {
283 ASSERT_NEAR(storm::utility::convertNumber<double>(walk[i].position[badCVar]), badCValues[i], 1e-4);
284 ASSERT_NEAR(storm::utility::convertNumber<double>(walk[i].position[pfVar]), pfValues[i], 1e-4);
287 ASSERT_NEAR(storm::utility::convertNumber<double>(doubleInstantiation.second), 0, 1e-6);
293 radamChecker.
setup(this->env(), feasibilityTask);
297 const double badCValuesRadam[] = {0.5,
339 const double pfValuesRadam[] = {0.5,
381 for (uint_fast64_t i = 0; i < 41; i++) {
382 ASSERT_NEAR(storm::utility::convertNumber<double>(radamWalk[i].position[badCVar]), badCValuesRadam[i], 1e-5);
383 ASSERT_NEAR(storm::utility::convertNumber<double>(radamWalk[i].position[pfVar]), pfValuesRadam[i], 1e-5);
390 momentumChecker.
setup(this->env(), feasibilityTask);
394 const double badCValuesMomentum[] = {
395 0.5 + 1e-6, 0.4990617036819458, 0.4972723126411438, 0.4947088360786438, 0.4914357662200928, 0.4875074326992035, 0.48296919465065,
396 0.4778585731983185, 0.47220611572265625, 0.4660361409187317, 0.45936742424964905, 0.45221376419067383, 0.44458451867103577, 0.43648505210876465,
397 0.42791709303855896, 0.41887906193733215, 0.4093664884567261, 0.3993722200393677, 0.3888867497444153, 0.37789851427078247, 0.3663942813873291,
398 0.3543594181537628, 0.34177839756011963, 0.32863524556159973, 0.3149142265319824, 0.30060049891471863, 0.28568127751350403, 0.27014678716659546,
399 0.253991961479187, 0.23721818625926971, 0.2198355346918106, 0.201865553855896, 0.18334446847438812, 0.16432702541351318, 0.1448907107114792,
400 0.12514044344425201, 0.10521329939365387, 0.08528289198875427, 0.06556269526481628, 0.04630732536315918, 0.027810536324977875};
401 const double pfValuesMomentum[] = {
402 0.5 + 1e-6, 0.49985647201538086, 0.49958109855651855, 0.4991863965988159, 0.49868202209472656, 0.49807605147361755, 0.49737516045570374,
403 0.49658480286598206, 0.4957093894481659, 0.49475228786468506, 0.4937160611152649, 0.49260255694389343, 0.4914129376411438, 0.49014779925346375,
404 0.4888072907924652, 0.4873911142349243, 0.4858987331390381, 0.4843292832374573, 0.4826817214488983, 0.4809550344944, 0.47914814949035645,
405 0.47726020216941833, 0.47529059648513794, 0.4732392132282257, 0.4711065888404846, 0.4688941240310669, 0.4666043817996979, 0.46424129605293274,
406 0.46181055903434753, 0.45931991934776306, 0.4567795991897583, 0.4542025327682495, 0.4516047239303589, 0.4490053057670593, 0.44642651081085205,
407 0.4438934028148651, 0.44143298268318176, 0.43907299637794495, 0.43684011697769165, 0.43475744128227234, 0.43284183740615845};
409 for (uint_fast64_t i = 0; i < 41; i++) {
410 ASSERT_NEAR(storm::utility::convertNumber<double>(momentumWalk[i].position[badCVar]), badCValuesMomentum[i], 1e-5);
411 ASSERT_NEAR(storm::utility::convertNumber<double>(momentumWalk[i].position[pfVar]), pfValuesMomentum[i], 1e-5);
418 nesterovChecker.
setup(this->env(), feasibilityTask);
422 const double badCValuesNesterov[] = {
423 0.5 + 1e-6, 0.49821633100509644, 0.49565380811691284, 0.4923747181892395, 0.48843076825141907, 0.4838651120662689, 0.4787132740020752,
424 0.473004013299942, 0.4667600393295288, 0.45999863743782043, 0.452732115983963, 0.44496846199035645, 0.43671154975891113, 0.4279615581035614,
425 0.4187155067920685, 0.4089673161506653, 0.3987082839012146, 0.387927383184433, 0.376611590385437, 0.36474621295928955, 0.35231542587280273,
426 0.33930283784866333, 0.3256921172142029, 0.3114677667617798, 0.2966162860393524, 0.2811274528503418, 0.2649959325790405, 0.24822339415550232,
427 0.23082087934017181, 0.21281197667121887, 0.19423632323741913, 0.1751537024974823, 0.15564869344234467, 0.1358354091644287, 0.11586219072341919,
428 0.09591540694236755, 0.07622162997722626, 0.05704677850008011, 0.03869114816188812, 0.021478772163391113, 0.005740571767091751};
429 const double pfValuesNesterov[] = {
430 0.5 + 1e-6, 0.49972638487815857, 0.4993318021297455, 0.4988263249397278, 0.4982176721096039, 0.4975121319293976, 0.4967147409915924,
431 0.4958295524120331, 0.4948597252368927, 0.4938075542449951, 0.49267470836639404, 0.49146217107772827, 0.49017035961151123, 0.48879921436309814,
432 0.48734840750694275, 0.48581716418266296, 0.48420456051826477, 0.4825096130371094, 0.48073118925094604, 0.4788684844970703, 0.47692081332206726,
433 0.4748881161212921, 0.4727708697319031, 0.47057047486305237, 0.4682896137237549, 0.4659323990345001, 0.4635048806667328, 0.4610152840614319,
434 0.4584745764732361, 0.45589667558670044, 0.45329880714416504, 0.45070162415504456, 0.4481291174888611, 0.44560813903808594, 0.44316741824150085,
435 0.440836101770401, 0.43864157795906067, 0.4366067945957184, 0.4347473978996277, 0.433069109916687, 0.43156614899635315};
437 for (uint_fast64_t i = 0; i < 41; i++) {
438 ASSERT_NEAR(storm::utility::convertNumber<double>(nesterovWalk[i].position[badCVar]), badCValuesNesterov[i], 1e-5);
439 ASSERT_NEAR(storm::utility::convertNumber<double>(nesterovWalk[i].position[pfVar]), pfValuesNesterov[i], 1e-5);