more work towards proper scheduler generation

Former-commit-id: ee6237ef49

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -1763,7 +1763,7 @@ namespace storm {
                 STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation.");
                 
                 bool strictBound = comparisonType == storm::logic::ComparisonType::Less;
-                double bound = probabilityOperator.getBound();
+                double threshold = probabilityOperator.getThreshold();
                 
                 storm::storage::BitVector phiStates;
                 storm::storage::BitVector psiStates;
@@ -1793,7 +1793,7 @@ namespace storm {
                 
                 // Delegate the actual computation work to the function of equal name.
                 auto startTime = std::chrono::high_resolution_clock::now();
-                auto labelSet = getMinimalCommandSet(probabilityOperator.getSubformula(), program, constantDefinitionString, labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet());
+                auto labelSet = getMinimalCommandSet(probabilityOperator.getSubformula(), program, constantDefinitionString, labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet());
                 auto endTime = std::chrono::high_resolution_clock::now();
                 std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
                 

src/modelchecker/CheckTask.h

@@ -30,7 +30,7 @@ namespace storm {
              */
             CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula) {
                 this->onlyInitialStatesRelevant = onlyInitialStatesRelevant;
-                this->produceSchedulers = true;
+                this->produceSchedulers = false;
                 this->qualitative = false;
                 
                 if (formula.isOperatorFormula()) {
@@ -165,6 +165,13 @@ namespace storm {
                 return qualitative;
             }
             
+            /*!
+             * Sets whether to produce schedulers (if supported).
+             */
+            void setProduceSchedulers(bool produceSchedulers) {
+                this->produceSchedulers = produceSchedulers;
+            }
+            
             /*!
              * Retrieves whether scheduler(s) are to be produced (if supported).
              */

src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h

@@ -3,14 +3,13 @@
 
 #include <vector>
 #include <memory>
-#include "src/storage/PartialScheduler.h"
+#include "src/storage/Scheduler.h"
 
 namespace storm {
     namespace storage {
         class BitVector;
     }
     
-    
     namespace modelchecker {
         namespace helper {
             template<typename ValueType>
@@ -19,7 +18,7 @@ namespace storm {
                 MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType const&) = delete;
                 MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType&&) = default;
                 
-                MDPSparseModelCheckingHelperReturnType(std::vector<ValueType>&& values, std::unique_ptr<storm::storage::PartialScheduler> && scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) {
+                MDPSparseModelCheckingHelperReturnType(std::vector<ValueType>&& values, std::unique_ptr<storm::storage::Scheduler>&& scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) {
                     // Intentionally left empty.
                 }
                 
@@ -31,7 +30,7 @@ namespace storm {
                 std::vector<ValueType> values;
                 
                 // A scheduler, if it was computed.
-                std::unique_ptr<storm::storage::PartialScheduler> scheduler;
+                std::unique_ptr<storm::storage::Scheduler> scheduler;
             };
         }
         

src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -1,4 +1,4 @@
-#include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
+ #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
 
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
@@ -12,6 +12,7 @@
 
 #include "src/storage/expressions/Variable.h"
 #include "src/storage/expressions/Expression.h"
+#include "src/storage/TotalScheduler.h"
 
 #include "src/solver/MinMaxLinearEquationSolver.h"
 #include "src/solver/LpSolver.h"
@@ -56,7 +57,6 @@ namespace storm {
                 
                 return result;
             }
-            
 
             template<typename ValueType>
             std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
@@ -73,7 +73,8 @@ namespace storm {
        
             
             template<typename ValueType>
-            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+                STORM_LOG_THROW(!(qualitative && produceScheduler), storm::exceptions::InvalidSettingsException, "Cannot produce scheduler when performing qualitative model checking only.");
                      
                 // 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.
@@ -96,7 +97,12 @@ namespace storm {
                 // Set values of resulting vector that are known exactly.
                 storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>());
                 storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>());
-                
+
+                // If requested, we will produce a scheduler.
+                std::unique_ptr<storm::storage::TotalScheduler> scheduler;
+                if (produceScheduler) {
+                    scheduler = std::make_unique<storm::storage::TotalScheduler>(transitionMatrix.getRowGroupCount());
+                }
                 
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {
@@ -119,20 +125,44 @@ namespace storm {
                         
                         // Solve the corresponding system of equations.
                         std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix);
+                        solver->setTrackScheduler(produceScheduler);
                         solver->solveEquationSystem(x, b);
                         
                         // Set values of resulting vector according to result.
                         storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
+                        
+                        if (produceScheduler) {
+                            storm::storage::Scheduler const& subscheduler = solver->getScheduler();
+                            uint_fast64_t currentSubState = 0;
+                            for (auto maybeState : maybeStates) {
+                                scheduler->setChoice(maybeState, subscheduler.getChoice(currentSubState));
+                                ++currentSubState;
+                            }
+                        }
+                    }
+                }
+                
+                // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for
+                // the states with probability 0 or 1 (depending on whether we maximize or minimize).
+                if (produceScheduler) {
+                    storm::storage::PartialScheduler relevantQualitativeScheduler;
+                    if (goal.minimize()) {
+                        relevantQualitativeScheduler = storm::utility::graph::computeSchedulerProb0E(statesWithProbability0, transitionMatrix);
+                    } else {
+                        relevantQualitativeScheduler = storm::utility::graph::computeSchedulerProb1E(statesWithProbability1, transitionMatrix, backwardTransitions, phiStates, psiStates);
+                    }
+                    for (auto const& stateChoicePair : relevantQualitativeScheduler) {
+                        scheduler->setChoice(stateChoicePair.first, stateChoicePair.second);
                     }
                 }
                 
-                return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(result));
+                return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(scheduler));
             }
 
             template<typename ValueType>
-            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
                 storm::solver::SolveGoal goal(dir);
-                return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, producePolicy, minMaxLinearEquationSolverFactory));
+                return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory));
             }
            
             template<typename ValueType>

src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h

@@ -36,9 +36,9 @@ namespace storm {
 
                 static std::vector<ValueType> computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
 
-                static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
+                static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
                 
-                static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
+                static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
                 
                 static std::vector<ValueType> computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false);
                 

src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -79,6 +79,22 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        bool ExplicitQuantitativeCheckResult<ValueType>::hasScheduler() const {
+            return static_cast<bool>(scheduler);
+        }
+        
+        template<typename ValueType>
+        void ExplicitQuantitativeCheckResult<ValueType>::setScheduler(std::unique_ptr<storm::storage::Scheduler>&& scheduler) {
+            this->scheduler = std::move(scheduler);
+        }
+        
+        template<typename ValueType>
+        storm::storage::Scheduler const& ExplicitQuantitativeCheckResult<ValueType>::getScheduler() const {
+            STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler.");
+            return *scheduler.get();
+        }
+        
         template<typename ValueType>
         std::ostream& ExplicitQuantitativeCheckResult<ValueType>::writeToStream(std::ostream& out) const {
             out << "[";

src/modelchecker/results/ExplicitQuantitativeCheckResult.h

@@ -4,9 +4,11 @@
 #include <vector>
 #include <map>
 #include <boost/variant.hpp>
+#include <boost/optional.hpp>
 
 #include "src/modelchecker/results/QuantitativeCheckResult.h"
 #include "src/storage/sparse/StateType.h"
+#include "src/storage/Scheduler.h"
 #include "src/utility/OsDetection.h"
 
 namespace storm {
@@ -51,9 +53,16 @@ namespace storm {
 
             virtual void oneMinus() override;
             
+            bool hasScheduler() const;
+            void setScheduler(std::unique_ptr<storm::storage::Scheduler>&& scheduler);
+            storm::storage::Scheduler const& getScheduler() const;
+            
         private:
             // The values of the quantitative check result.
             boost::variant<vector_type, map_type> values;
+            
+            // An optional scheduler that accompanies the values.
+            boost::optional<std::shared_ptr<storm::storage::Scheduler>> scheduler;
         };
     }
 }

src/parser/PrismParser.cpp

@@ -142,7 +142,7 @@ namespace storm {
             assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()];
             assignmentDefinitionList.name("assignment list");
             
-            updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
+            updateDefinition = (((expressionParser >> qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
             updateDefinition.name("update");
             
             updateListDefinition %= +updateDefinition(qi::_r1) % "+";

src/solver/GmmxxMinMaxLinearEquationSolver.cpp

@@ -16,12 +16,8 @@ namespace storm {
         
         template<typename ValueType>
         GmmxxMinMaxLinearEquationSolver<ValueType>::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, MinMaxTechniqueSelection preferredTechnique, bool trackPolicy) : 
-        MinMaxLinearEquationSolver<ValueType>(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), \
-                                                storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative,\
-                                                storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique),
-            gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A)), rowGroupIndices(A.getRowGroupIndices()) {
-           
-			
+        MinMaxLinearEquationSolver<ValueType>(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A)), rowGroupIndices(A.getRowGroupIndices()) {
+                // Intentionally left empty.
         }
         
         template<typename ValueType>
@@ -29,11 +25,12 @@ namespace storm {
             // Intentionally left empty.
         }
 
-        
         template<typename ValueType>
         void GmmxxMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
 			if (this->useValueIteration) {
-				// Set up the environment for the power method. If scratch memory was not provided, we need to create it.
+                STORM_LOG_THROW(!this->isTrackSchedulerSet(), storm::exceptions::InvalidSettingsException, "Unable to produce a scheduler when using value iteration. Use policy iteration instead.");
+
+                // Set up the environment for the power method. If scratch memory was not provided, we need to create it.
 				bool multiplyResultMemoryProvided = true;
 				if (multiplyResult == nullptr) {
 					multiplyResult = new std::vector<ValueType>(b.size());

src/solver/MinMaxLinearEquationSolver.cpp

@@ -23,6 +23,11 @@ namespace storm {
             this->trackScheduler = trackScheduler;
         }
         
+        template<typename ValueType>
+        bool AbstractMinMaxLinearEquationSolver<ValueType>::hasScheduler() const {
+            return static_cast<bool>(scheduler);
+        }
+        
         template<typename ValueType>
         bool AbstractMinMaxLinearEquationSolver<ValueType>::isTrackSchedulerSet() const {
             return this->trackScheduler;

src/solver/MinMaxLinearEquationSolver.h

@@ -30,6 +30,7 @@ namespace storm {
         public:
             void setTrackScheduler(bool trackScheduler = true);
             bool isTrackSchedulerSet() const;
+            bool hasScheduler() const;
             
             storm::storage::Scheduler const& getScheduler() const;
             
@@ -69,7 +70,7 @@ namespace storm {
         template<class ValueType>
         class MinMaxLinearEquationSolver : public AbstractMinMaxLinearEquationSolver<ValueType> {
         protected:
-            MinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : AbstractMinMaxLinearEquationSolver<ValueType>(precision, relativeError, maxNrIterations, trackPolicy, prefTech), A(matrix) {
+            MinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech) : AbstractMinMaxLinearEquationSolver<ValueType>(precision, relativeError, maxNrIterations, trackScheduler, prefTech), A(matrix) {
                 // Intentionally left empty.
             }
         

src/storage/PartialScheduler.cpp

@@ -22,6 +22,14 @@ namespace storm {
             return stateChoicePair->second;
         }
         
+        PartialScheduler::map_type::const_iterator PartialScheduler::begin() const {
+            return stateToChoiceMapping.begin();
+        }
+        
+        PartialScheduler::map_type::const_iterator PartialScheduler::end() const {
+            return stateToChoiceMapping.end();
+        }
+        
         std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler) {
             out << "partial scheduler (defined on " << scheduler.stateToChoiceMapping.size() << " states) [ ";
             uint_fast64_t remainingEntries = scheduler.stateToChoiceMapping.size();

src/storage/PartialScheduler.h

@@ -19,6 +19,9 @@ namespace storm {
             
             uint_fast64_t getChoice(uint_fast64_t state) const override;
             
+            map_type::const_iterator begin() const;
+            map_type::const_iterator end() const;
+            
             friend std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler);
 
         private:

src/utility/graph.cpp

@@ -280,7 +280,7 @@ namespace storm {
                             }
                         }
                         if (allSuccessorsInStates) {
-                            result.setChoice(state, choice);
+                            result.setChoice(state, choice - nondeterministicChoiceIndices[state]);
                             break;
                         }
                     }
@@ -304,7 +304,7 @@ namespace storm {
                             }
                         }
                         if (oneSuccessorInStates) {
-                            result.setChoice(state, choice);
+                            result.setChoice(state, choice - nondeterministicChoiceIndices[state]);
                             break;
                         }
                     }
@@ -356,7 +356,7 @@ namespace storm {
                                 // If all successors for a given nondeterministic choice are in the prob1E state set, we
                                 // perform a backward search from that state.
                                 if (allSuccessorsInProb1EStates && hasSuccessorInCurrentStates) {
-                                    result.setChoice(predecessorEntryIt->getColumn(), row);
+                                    result.setChoice(predecessorEntryIt->getColumn(), row - nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]);
                                     currentStates.set(predecessorEntryIt->getColumn(), true);
                                     stack.push_back(predecessorEntryIt->getColumn());
                                     break;

src/utility/solver.cpp

@@ -91,17 +91,19 @@ namespace storm {
             }
             
             template<typename ValueType>
-            void MinMaxLinearEquationSolverFactory<ValueType>::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) {
+            MinMaxLinearEquationSolverFactory<ValueType>& MinMaxLinearEquationSolverFactory<ValueType>::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) {
                 if(solverTypeSel == storm::solver::EquationSolverTypeSelection::FROMSETTINGS) {
                     this->solverType = storm::settings::generalSettings().getEquationSolver();
                 } else {
                     this->solverType = storm::solver::convert(solverTypeSel);
                 }
-                
+                return *this;
             }
+            
             template<typename ValueType>
-            void MinMaxLinearEquationSolverFactory<ValueType>::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) {
+            MinMaxLinearEquationSolverFactory<ValueType>& MinMaxLinearEquationSolverFactory<ValueType>::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) {
                 this->prefTech = preferredTech;
+                return *this;
             }
             
             template<typename ValueType>
@@ -128,7 +130,6 @@ namespace storm {
                 }
                 p1->setTrackScheduler(trackScheduler);
                 return p1;
-                
             }
 
             template<typename ValueType>

src/utility/solver.h

@@ -114,8 +114,8 @@ namespace storm {
                  * Creates a new min/max linear equation solver instance with the given matrix.
                  */
                 virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackScheduler = false) const;
-                void setSolverType(storm::solver::EquationSolverTypeSelection solverType);
-                void setPreferredTechnique(storm::solver::MinMaxTechniqueSelection);
+                MinMaxLinearEquationSolverFactory<ValueType>& setSolverType(storm::solver::EquationSolverTypeSelection solverType);
+                MinMaxLinearEquationSolverFactory<ValueType>& setPreferredTechnique(storm::solver::MinMaxTechniqueSelection);
                 
             protected:
                 /// The type of solver which should be created.

test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@@ -14,6 +14,8 @@
 
 #include "src/settings/modules/NativeEquationSolverSettings.h"
 #include "src/parser/AutoParser.h"
+#include "src/parser/PrismParser.h"
+#include "src/builder/ExplicitPrismModelBuilder.h"
 
 TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
     std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
@@ -188,3 +190,37 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
 
     EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
 }
+
+TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/scheduler_generation.nm");
+    
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+    EXPECT_EQ(4ul, model->getNumberOfStates());
+    EXPECT_EQ(11ul, model->getNumberOfTransitions());
+    
+    ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>();
+
+    EXPECT_EQ(7ul, mdp->getNumberOfChoices());
+    
+    auto solverFactory = std::make_unique<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(storm::solver::EquationSolverTypeSelection::Gmmxx);
+    solverFactory->setPreferredTechnique(storm::solver::MinMaxTechniqueSelection::PolicyIteration);
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::move(solverFactory));
+    
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]");
+    
+    storm::modelchecker::CheckTask<storm::logic::Formula> checkTask(*formula);
+    checkTask.setProduceSchedulers(true);
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(checkTask);
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]");
+    checkTask.replaceFormula(*formula);
+
+    result = checker.check(checkTask);
+    
+}

test/functional/modelchecker/scheduler_generation.nm

@@ -0,0 +1,16 @@
+mdp
+
+module one
+
+  s : [0 .. 5] init 0;
+
+  [] s=0 -> 0.5: (s'=1) + 0.5: (s'=3);
+  [] s=1 -> 0.4 : (s'=4) + 0.6: (s'=3);
+  [] s=1 -> 1: (s'=4);
+  [] s=1 -> 0.8: (s'=3) + 0.2: (s'=4);
+  [] s=0 | s = 2 -> 0.9: (s'=s) + 0.1 : (s'=3);
+  [] 3 <= s & s <= 4 -> 1: true;
+
+endmodule
+
+label "target" = s=3;