From 9771658dcc3f4c488d6bd88e7ec453df511b1f4c Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 16 Nov 2017 15:17:23 +0100 Subject: [PATCH] only do end component elimination in MDP model checking if there are end components --- .../prctl/helper/HybridMdpPrctlHelper.cpp | 25 ++++++++++++++++--- .../prctl/helper/SparseMdpPrctlHelper.cpp | 17 ++++++++++--- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 20 +++++++++++++++ 3 files changed, 55 insertions(+), 7 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 6b3ea5b6a..3b671028f 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -96,8 +96,16 @@ namespace storm { storm::storage::MaximalEndComponentDecomposition endComponentDecomposition; if (doDecomposition) { - // Then compute the states that are in MECs with zero reward. - endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition(transitionMatrix, transitionMatrix.transpose(), solverRequirementsData.properMaybeStates); + auto backwardTransitions = transitionMatrix.transpose(true); + // Get the set of states that (under some scheduler) can stay in the set of maybestates forever + storm::storage::BitVector candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, solverRequirementsData.properMaybeStates, ~solverRequirementsData.properMaybeStates); + + doDecomposition = !candidateStates.empty(); + + if (doDecomposition) { + // If there are candidates, compute the states that are in MECs with zero reward. + endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition(transitionMatrix, backwardTransitions, candidateStates); + } } // Only do more work if there are actually end-components. @@ -430,8 +438,17 @@ namespace storm { storm::storage::MaximalEndComponentDecomposition endComponentDecomposition; if (doDecomposition) { - // Then compute the states that are in MECs with zero reward. - endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition(transitionMatrix, transitionMatrix.transpose(), candidateStates, zeroRewardChoices); + auto backwardTransitions = transitionMatrix.transpose(true); + + // Only keep the candidate states that (under some scheduler) can stay in the set of candidates forever + candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, ~candidateStates); + + doDecomposition = !candidateStates.empty(); + + if (doDecomposition) { + // If there are candidates, compute the states that are in MECs with zero reward. + endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition(transitionMatrix, backwardTransitions, candidateStates, zeroRewardChoices); + } } // Only do more work if there are actually end-components. diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index e638a6b15..ef8f5a1bb 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -660,11 +660,19 @@ namespace storm { template boost::optional> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix& submatrix, std::vector& b) { - // Start by computing the states that are in MECs. - storm::storage::MaximalEndComponentDecomposition endComponentDecomposition(transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates); + // Get the set of states that (under some scheduler) can stay in the set of maybestates forever + storm::storage::BitVector candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.maybeStates); + + bool doDecomposition = !candidateStates.empty(); + + storm::storage::MaximalEndComponentDecomposition endComponentDecomposition; + if (doDecomposition) { + // Compute the states that are in MECs. + endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition(transitionMatrix, backwardTransitions, candidateStates); + } // Only do more work if there are actually end-components. - if (!endComponentDecomposition.empty()) { + if (doDecomposition && !endComponentDecomposition.empty()) { STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " EC(s)."); SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr); @@ -994,6 +1002,9 @@ namespace storm { } } + // Only keep the candidate states that (under some scheduler) can stay in the set of candidates forever + candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, ~candidateStates); + bool doDecomposition = !candidateStates.empty(); storm::storage::MaximalEndComponentDecomposition endComponentDecomposition; diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index c8e754764..523ba2711 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -67,6 +67,10 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); + if (storm::solver::minimize(dir)) { + solver->setHasUniqueSolution(true); + } + // Check requirements of solver. storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(env, dir); boost::optional> initialScheduler; @@ -77,6 +81,12 @@ namespace storm { requirements.clearValidInitialScheduler(); } requirements.clearBounds(); + if (requirements.requiresNoEndComponents()) { + // Check whether there are end components + if (storm::utility::graph::performProb0E(model, transitionMatrix.notZero(), maybeStates, !maybeStates && model.getReachableStates()).isZero()) { + requirements.clearNoEndComponents(); + } + } STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Could not establish requirements of solver."); } if (initialScheduler) { @@ -224,6 +234,10 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); + if (storm::solver::maximize(dir)) { + solver->setHasUniqueSolution(true); + } + // Check requirements of solver. storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(env, dir); boost::optional> initialScheduler; @@ -234,6 +248,12 @@ namespace storm { requirements.clearValidInitialScheduler(); } requirements.clearLowerBounds(); + if (requirements.requiresNoEndComponents()) { + // Check whether there are end components + if (storm::utility::graph::performProb0E(model, transitionMatrixBdd, maybeStates, !maybeStates && model.getReachableStates()).isZero()) { + requirements.clearNoEndComponents(); + } + } STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Could not establish requirements of solver."); } if (initialScheduler) {