corrected some output and adapted requirements of symbolic minmax solver

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

@@ -28,10 +28,11 @@ namespace storm {
             std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 // We need to identify the states which have to be taken out of the matrix, i.e. all states that have
                 // probability 0 and 1 of satisfying the until-formula.
+                STORM_LOG_TRACE("Found " << phiStates.getNonZeroCount() << " phi states and " << psiStates.getNonZeroCount() << " psi states.");
                 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates);
                 storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates();
                 
-                STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 1, " << statesWithProbability01.second.getNonZeroCount() << " with probability 0 (" << maybeStates.getNonZeroCount() << " states remaining).");
+                STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 0, " << statesWithProbability01.second.getNonZeroCount() << " with probability 1 (" << maybeStates.getNonZeroCount() << " states remaining).");
                 
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {

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

@@ -22,10 +22,11 @@ namespace storm {
             storm::dd::Add<DdType, ValueType> SymbolicDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) {
                 // We need to identify the states which have to be taken out of the matrix, i.e. all states that have
                 // probability 0 and 1 of satisfying the until-formula.
+                STORM_LOG_TRACE("Found " << phiStates.getNonZeroCount() << " phi states and " << psiStates.getNonZeroCount() << " psi states.");
                 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates);
                 storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates();
                 
-                STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 1, " << statesWithProbability01.second.getNonZeroCount() << " with probability 0 (" << maybeStates.getNonZeroCount() << " states remaining).");
+                STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 0, " << statesWithProbability01.second.getNonZeroCount() << " with probability 1 (" << maybeStates.getNonZeroCount() << " states remaining).");
                 
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {

src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

@@ -28,7 +28,13 @@ namespace storm {
             if (comparisonType == storm::logic::ComparisonType::Less) {
                 states &= values.less(bound);
             } else if (comparisonType == storm::logic::ComparisonType::LessEqual) {
+                std::cout << "states zero: " << (values.equals(values.getDdManager().template getAddZero<ValueType>()) && reachableStates).getNonZeroCount() << std::endl;
+                std::cout << "states one: " << (values.equals(values.getDdManager().template getAddOne<ValueType>()) && reachableStates).getNonZeroCount() << std::endl;
+                std::cout << "states before: " << states.getNonZeroCount() << std::endl;
+                values.exportToDot("vals.dot");
+                std::cout << "total: " <<((values.equals(values.getDdManager().template getAddOne<ValueType>()) && states) || (values.lessOrEqual(bound) && states)).getNonZeroCount() << std::endl;
                 states &= values.lessOrEqual(bound);
+                std::cout << "states after: " << states.getNonZeroCount() << std::endl;
             } else if (comparisonType == storm::logic::ComparisonType::Greater) {
                 states &= values.greater(bound);
             } else if (comparisonType == storm::logic::ComparisonType::GreaterEqual) {

src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -406,19 +406,32 @@ namespace storm {
         template<storm::dd::DdType DdType, typename ValueType>
         MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             MinMaxLinearEquationSolverRequirements requirements;
-            
-            if (equationSystemType == EquationSystemType::UntilProbabilities) {
-                if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
+
+            if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
+                if (equationSystemType == EquationSystemType::UntilProbabilities) {
                     if (!direction || direction.get() == OptimizationDirection::Maximize) {
                         requirements.requireValidInitialScheduler();
                     }
                 }
-            } else if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                    requirements.requireValidInitialScheduler();
+                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
+                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
+                        requirements.requireValidInitialScheduler();
+                    }
+                }
+            } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) {
+                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
+                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
+                        requirements.requireValidInitialScheduler();
+                    }
+                }
+            } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch) {
+                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
+                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
+                        requirements.requireNoEndComponents();
+                    }
                 }
             }
-            
+
             return requirements;
         }