From e81d979d569b606622291c4d6a85bd93c832e719 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 5 Sep 2017 18:18:05 +0200 Subject: [PATCH] hybrid MDP helper respecting solver requirements --- .../prctl/helper/HybridMdpPrctlHelper.cpp | 36 +++++++++++-------- .../prctl/helper/SparseMdpPrctlHelper.cpp | 2 +- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 24 ++++++------- .../GmmxxMdpPrctlModelCheckerTest.cpp | 8 ++--- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 8 ++--- .../NativeMdpPrctlModelCheckerTest.cpp | 8 ++--- 6 files changed, 46 insertions(+), 40 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 67b2dbf1f..5447d7fbd 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -285,22 +285,27 @@ namespace storm { template void eliminateTargetStatesFromExplicitRepresentation(std::pair, std::vector>& explicitRepresentation, std::vector& scheduler, storm::storage::BitVector const& properMaybeStates) { - // Treat the matrix first. - explicitRepresentation.first = explicitRepresentation.first.getSubmatrix(true, properMaybeStates, properMaybeStates); - - // Now eliminate the superfluous entries from the rhs vector and the scheduler. + // Eliminate the superfluous entries from the rhs vector and the scheduler. uint64_t position = 0; for (auto state : properMaybeStates) { - explicitRepresentation.second[position] = explicitRepresentation.second[state]; + for (uint64_t row = explicitRepresentation.first.getRowGroupIndices()[state]; row < explicitRepresentation.first.getRowGroupIndices()[state + 1]; ++row) { + explicitRepresentation.second[position] = explicitRepresentation.second[row]; + position++; + } + } + explicitRepresentation.second.resize(position); + explicitRepresentation.second.shrink_to_fit(); + + position = 0; + for (auto state : properMaybeStates) { scheduler[position] = scheduler[state]; position++; } - - uint64_t numberOfProperMaybeStates = properMaybeStates.getNumberOfSetBits(); - explicitRepresentation.second.resize(numberOfProperMaybeStates); - explicitRepresentation.second.shrink_to_fit(); - scheduler.resize(numberOfProperMaybeStates); + scheduler.resize(properMaybeStates.getNumberOfSetBits()); scheduler.shrink_to_fit(); + + // Treat the matrix. + explicitRepresentation.first = explicitRepresentation.first.getSubmatrix(true, properMaybeStates, properMaybeStates); } template @@ -312,6 +317,8 @@ namespace storm { expandedResult[state] = x[position]; position++; } + + return expandedResult; } template @@ -324,7 +331,6 @@ namespace storm { storm::dd::Bdd infinityStates; storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); if (dir == OptimizationDirection::Minimize) { - STORM_LOG_WARN("Results of reward computation may be too low, because of zero-reward loops."); infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); } else { infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); @@ -345,7 +351,7 @@ namespace storm { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { // Check for requirements of the solver this early so we can adapt the maybe states accordingly. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards, dir); bool requireInitialScheduler = false; if (!requirements.empty()) { if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { @@ -403,6 +409,9 @@ namespace storm { // of the scheduler, we have to get rid of them now. eliminateTargetStatesFromExplicitRepresentation(explicitRepresentation, initialScheduler.get(), properMaybeStates.get()); } + + // Create the solution vector. + std::vector x(explicitRepresentation.first.getRowGroupCount(), storm::utility::zero()); // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); @@ -412,9 +421,6 @@ namespace storm { solver->setInitialScheduler(std::move(initialScheduler.get())); } - // Create the solution vector. - std::vector x(explicitRepresentation.first.getRowGroupCount(), storm::utility::zero()); - solver->setRequirementsChecked(); solver->solveEquations(dir, x, explicitRepresentation.second); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 605f108bf..fb70009a3 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -202,7 +202,7 @@ namespace storm { SparseMdpHintType result; // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(type); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(type, dir); if (!(hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()) && !requirements.empty()) { if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { STORM_LOG_DEBUG("Computing valid scheduler hint, because the solver requires it."); diff --git a/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index adf69343c..203730667 100644 --- a/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -107,8 +107,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -205,8 +205,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -285,8 +285,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); @@ -294,8 +294,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2856896106114934, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2856896106114934, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2856904354441401, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2856904354441401, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); } TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { @@ -365,8 +365,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); @@ -374,7 +374,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.2856896106114934, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2856896106114934, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2856904354441401, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2856904354441401, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); } diff --git a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 3d590ef74..e771b3e0a 100644 --- a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -79,7 +79,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333333333333375, quantitativeResult7[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -101,7 +101,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333333333333375, quantitativeResult9[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -123,7 +123,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(14.666666666666675, quantitativeResult11[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -181,7 +181,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2857129064503061, quantitativeResult5[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); diff --git a/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index 09e480133..1bba57ace 100644 --- a/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -103,8 +103,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -200,8 +200,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); diff --git a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 7cec42eae..a64e66f04 100644 --- a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -76,7 +76,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333317041397095, quantitativeResult7[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -98,7 +98,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333317041397095, quantitativeResult9[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -120,7 +120,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(14.666663408279419, quantitativeResult11[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -178,7 +178,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2856907116062786, quantitativeResult5[0], storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");