Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

@@ -6,6 +6,8 @@
 #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
+#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/solver/StandardMinMaxLinearEquationSolver.h"
@@ -17,6 +19,8 @@
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/UncheckedRequirementException.h"
+
 
 namespace storm {
     namespace modelchecker {
@@ -27,7 +31,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)) {
+        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false) {
             // Intentionally left empty
         }
         
@@ -109,6 +113,8 @@ namespace storm {
             // We know some bounds for the results so set them
             lowerResultBound = storm::utility::zero<ConstantType>();
             upperResultBound = storm::utility::one<ConstantType>();
+            // No requirements for bounded formulas
+            solverFactory->setRequirementsChecked(true);
         }
 
         template <typename SparseModelType, typename ConstantType>
@@ -139,6 +145,12 @@ namespace storm {
             // We know some bounds for the results so set them
             lowerResultBound = storm::utility::zero<ConstantType>();
             upperResultBound = storm::utility::one<ConstantType>();
+            
+            auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::UntilProbabilities);
+            req.clearBounds();
+            req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
+            STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
+            solverFactory->setRequirementsChecked(true);
         }
 
         template <typename SparseModelType, typename ConstantType>
@@ -172,6 +184,17 @@ namespace storm {
             
             // We only know a lower bound for the result
             lowerResultBound = storm::utility::zero<ConstantType>();
+        
+            auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards);
+            req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
+            req.clearLowerBounds();
+            if (req.requiresUpperBounds()) {
+                solvingRequiresUpperRewardBounds = true;
+                req.clearUpperBounds();
+            }
+            STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
+            solverFactory->setRequirementsChecked(true);
+
 
         }
 
@@ -200,6 +223,9 @@ namespace storm {
             
             // We only know a lower bound for the result
             lowerResultBound = storm::utility::zero<ConstantType>();
+            
+            // No requirements for bounded reward formula
+            solverFactory->setRequirementsChecked(true);
         }
         
         template <typename SparseModelType, typename ConstantType>
@@ -228,7 +254,23 @@ namespace storm {
             }
             auto solver = solverFactory->create(parameterLifter->getMatrix());
             if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
-            if (upperResultBound) solver->setUpperBound(upperResultBound.get());
+            if (upperResultBound) {
+                solver->setUpperBound(upperResultBound.get());
+            } else if (solvingRequiresUpperRewardBounds) {
+                // For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17).
+                std::vector<ConstantType> oneStepProbs;
+                oneStepProbs.reserve(parameterLifter->getMatrix().getRowCount());
+                for (uint64_t row = 0; row < parameterLifter->getMatrix().getRowCount(); ++row) {
+                    oneStepProbs.push_back(storm::utility::one<ConstantType>() - parameterLifter->getMatrix().getRowSum(row));
+                }
+                if (dirForParameters == storm::OptimizationDirection::Minimize) {
+                    storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<ConstantType> dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+                    solver->setUpperBounds(dsmpi.computeUpperBounds());
+                } else {
+                    storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ConstantType> baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+                    solver->setUpperBound(baier.computeUpperBound());
+                }
+            }
             if (!stepBound) solver->setTrackScheduler(true);
             if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setInitialScheduler(std::move(minSchedChoices.get()));
             if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setInitialScheduler(std::move(maxSchedChoices.get()));
@@ -247,7 +289,7 @@ namespace storm {
             }
             
             // Invoke the solver
-            if(stepBound) {
+            if (stepBound) {
                 assert(*stepBound > 0);
                 x = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
                 solver->repeatedMultiply(dirForParameters, x, &parameterLifter->getVector(), *stepBound);

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h

@@ -12,7 +12,6 @@
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 #include "storm/logic/FragmentSpecification.h"
 
-
 namespace storm {
     namespace modelchecker {
             
@@ -49,12 +48,13 @@ namespace storm {
             storm::storage::BitVector maybeStates;
             std::vector<ConstantType> resultsForNonMaybeStates;
             boost::optional<uint_fast64_t> stepBound;
-                
+            
             std::unique_ptr<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
-                
+            
             std::unique_ptr<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>> parameterLifter;
             std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>> solverFactory;
-                
+            bool solvingRequiresUpperRewardBounds;
+            
             // Results from the most recent solver call.
             boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
             std::vector<ConstantType> x;

src/storm/settings/modules/EigenEquationSolverSettings.cpp

@@ -113,6 +113,7 @@ namespace storm {
                     case EigenEquationSolverSettings::LinearEquationMethod::DGMRES: out << "dgmres"; break;
                     case EigenEquationSolverSettings::LinearEquationMethod::SparseLU: out << "sparselu"; break;
                 }
+                return out;
             }
             
         } // namespace modules

src/storm/settings/modules/NativeEquationSolverSettings.cpp

@@ -120,6 +120,7 @@ namespace storm {
                     case NativeEquationSolverSettings::LinearEquationMethod::WalkerChae: out << "walkerchae"; break;
                     case NativeEquationSolverSettings::LinearEquationMethod::Power: out << "power"; break;
                 }
+                return out;
             }
             
         } // namespace modules

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -255,6 +255,11 @@ namespace storm {
             // Start by copying the requirements of the linear equation solver.
             MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements());
             
+            // In case we perform value iteration and need to retrieve a scheduler, end components are forbidden
+            if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && this->isTrackSchedulerSet()) {
+                requirements.requireNoEndComponents();
+            }
+            
             // Guide requirements by whether or not we force soundness.
             if (this->getSettings().getForceSoundness()) {
                 // Only add requirements for value iteration here as the policy iteration requirements are indifferent
@@ -375,7 +380,7 @@ namespace storm {
             // If requested, we store the scheduler for retrieval.
             if (this->isTrackSchedulerSet()) {
                 this->schedulerChoices = std::vector<uint_fast64_t>(this->A->getRowGroupCount());
-                this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *currentX, &this->schedulerChoices.get());
+                this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *auxiliaryRowGroupVector.get(), &this->schedulerChoices.get());
             }
 
             if (!this->isCachingEnabled()) {

src/storm/solver/LpMinMaxLinearEquationSolver.cpp

@@ -108,6 +108,21 @@ namespace storm {
             StandardMinMaxLinearEquationSolver<ValueType>::clearCache();
         }
         
+        
+        template<typename ValueType>
+        MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+            
+            MinMaxLinearEquationSolverRequirements requirements;
+            
+            // In case we need to retrieve a scheduler, end components are forbidden
+            if (this->isTrackSchedulerSet()) {
+                requirements.requireNoEndComponents();
+            }
+            
+            return  requirements;
+        }
+
+        
         template<typename ValueType>
         LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>()) {
             // Intentionally left empty

src/storm/solver/LpMinMaxLinearEquationSolver.h

@@ -18,6 +18,8 @@ namespace storm {
 
             virtual void clearCache() const override;
 
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
+            
         private:
             std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;
         };