only do end component elimination in MDP model checking if there are end components

src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp

@@ -96,8 +96,16 @@ namespace storm {
                 
                 storm::storage::MaximalEndComponentDecomposition<ValueType> endComponentDecomposition;
                 if (doDecomposition) {
-                    // Then compute the states that are in MECs with zero reward.
-                    endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(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<ValueType>(transitionMatrix, backwardTransitions, candidateStates);
+                    }
                 }
                 
                 // Only do more work if there are actually end-components.
@@ -430,8 +438,17 @@ namespace storm {
                 
                 storm::storage::MaximalEndComponentDecomposition<ValueType> endComponentDecomposition;
                 if (doDecomposition) {
-                    // Then compute the states that are in MECs with zero reward.
-                    endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(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<ValueType>(transitionMatrix, backwardTransitions, candidateStates, zeroRewardChoices);
+                    }
                 }
 
                 // Only do more work if there are actually end-components.

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -660,11 +660,19 @@ namespace storm {
             template<typename ValueType>
             boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b) {
                 
-                // Start by computing the states that are in MECs.
-                storm::storage::MaximalEndComponentDecomposition<ValueType> 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<ValueType> endComponentDecomposition;
+                if (doDecomposition) {
+                    // Compute the states that are in MECs.
+                    endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(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<ValueType> result = SparseMdpEndComponentInformation<ValueType>::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<ValueType> endComponentDecomposition;

src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp

@@ -67,6 +67,10 @@ namespace storm {
                 // Now solve the resulting equation system.
                 std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> 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<storm::dd::Bdd<DdType>> 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<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> 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<storm::dd::Bdd<DdType>> 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) {