made everything compile again and all tests passing

Former-commit-id: 65c66fb58f

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -985,7 +985,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;
@@ -1015,7 +1015,7 @@ namespace storm {
                 
                 // Delegate the actual computation work to the function of equal name.
                 auto startTime = std::chrono::high_resolution_clock::now();
-                boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(probabilityOperator.getSubformula(), labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet());
+                boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(probabilityOperator.getSubformula(), labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet());
                 auto endTime = std::chrono::high_resolution_clock::now();
                 std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
 

src/logic/Bound.h

@@ -14,7 +14,8 @@ namespace storm {
             ComparisonType comparisonType;
             ValueType threshold;
 
-            friend std::ostream& operator<<(std::ostream& out, Bound<ValueType> const& bound);
+            template<typename ValueTypePrime>
+            friend std::ostream& operator<<(std::ostream& out, Bound<ValueTypePrime> const& bound);
         };
 
         template<typename ValueType>

src/parser/FormulaParser.cpp

@@ -97,7 +97,7 @@ namespace storm {
             
             qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> start;
             
-            qi::rule<Iterator, std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
+            qi::rule<Iterator, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>>(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> probabilityOperator;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardOperator;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expectedTimeOperator;
@@ -149,10 +149,11 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula> createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula);
             std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const;
-            std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula> createExpectedTimeOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
+            std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const;
+            std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createExpectedTimeOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
             std::shared_ptr<storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
             std::shared_ptr<storm::logic::Formula> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
             
@@ -305,7 +306,7 @@ namespace storm {
             pathFormula = conditionalFormula;
             pathFormula.name("path formula");
             
-            operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct<std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>>(qi::_a, qi::_b, qi::_c)];
+            operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
             operatorInformation.name("operator information");
             
             longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
@@ -469,20 +470,28 @@ namespace storm {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+        std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const {
+            if (comparisonType && threshold) {
+                return std::make_pair(optimizationDirection, storm::logic::Bound<double>(comparisonType.get(), threshold.get()));
+            } else {
+                return std::make_pair(optimizationDirection, boost::none);
+            }
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(rewardModelName, operatorInformation.first, operatorInformation.second, subformula));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createExpectedTimeOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ExpectedTimeOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
         }
         
         std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {

src/solver/AbstractEquationSolver.h

@@ -29,7 +29,7 @@ namespace storm {
             /*!
              * Retrieves whether a custom termination condition has been set.
              */
-            bool hasCustomTerminationCondition() {
+            bool hasCustomTerminationCondition() const {
                 return static_cast<bool>(this->terminationCondition);
             }
             

src/solver/GmmxxLinearEquationSolver.cpp

@@ -171,7 +171,7 @@ namespace storm {
             uint_fast64_t iterationCount = 0;
             bool converged = false;
             
-            while (!converged && iterationCount < maximalNumberOfIterations) {
+            while (!converged && iterationCount < maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
                 // Compute D^-1 * (b - LU * x) and store result in nextX.
                 gmm::mult(*gmmLU, *currentX, tmpX);
                 gmm::add(b, gmm::scaled(tmpX, -storm::utility::one<ValueType>()), tmpX);

src/solver/GmmxxMinMaxLinearEquationSolver.cpp

@@ -5,6 +5,7 @@
 #include "src/settings/SettingsManager.h"
 #include "src/adapters/GmmxxAdapter.h"
 #include "src/solver/GmmxxLinearEquationSolver.h"
+#include "src/storage/TotalScheduler.h"
 #include "src/utility/vector.h"
 
 #include "src/settings/modules/GeneralSettings.h"
@@ -53,7 +54,7 @@ namespace storm {
 
 				// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
 				// of iterations.
-				while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) {
+				while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
 					// Compute x' = A*x + b.
 					gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult);
 					gmm::add(b, *multiplyResult);
@@ -92,7 +93,7 @@ namespace storm {
 			} else {
 				// We will use Policy Iteration to solve the given system.
 				// We first guess an initial choice resolution which will be refined after each iteration.
-				this->policy = std::vector<storm::storage::sparse::state_type>(this->A.getRowGroupIndices().size() - 1);
+				std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupIndices().size() - 1);
 
 				// Create our own multiplyResult for solving the deterministic sub-instances.
 				std::vector<ValueType> deterministicMultiplyResult(rowGroupIndices.size() - 1);
@@ -119,13 +120,13 @@ namespace storm {
 
 				// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
 				// of iterations.
-				while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) {
+				while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
 					// Take the sub-matrix according to the current choices
-					storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(this->policy, true);
+					storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
 					submatrix.convertToEquationSystem();
 					
 					GmmxxLinearEquationSolver<ValueType> gmmLinearEquationSolver(submatrix, storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, this->precision, this->maximalNumberOfIterations, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::Ilu, this->relative, 50);
-					storm::utility::vector::selectVectorValues<ValueType>(subB, this->policy, rowGroupIndices, b);
+					storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, rowGroupIndices, b);
 
 					// Copy X since we will overwrite it
 					std::copy(currentX->begin(), currentX->end(), newX->begin());
@@ -139,8 +140,7 @@ namespace storm {
 
 					// Reduce the vector x by applying min/max over all nondeterministic choices.
 					// Here, we capture which choice was taken in each state, thereby refining our initial guess.
-					storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices, &(this->policy));
-					
+					storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices, &(scheduler));
 
 					// Determine whether the method converged.
 					converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, static_cast<ValueType>(this->precision), this->relative);
@@ -156,6 +156,11 @@ namespace storm {
 				} else {
 					LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations.");
 				}
+                
+                // If requested, we store the scheduler for retrieval.
+                if (this->isTrackSchedulerSet()) {
+                    this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(scheduler));
+                }
 
 				// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
 				// is currently stored in currentX, but x is the output vector.

src/solver/MinMaxLinearEquationSolver.cpp

@@ -8,9 +8,8 @@
 
 namespace storm {
     namespace solver {
-        AbstractMinMaxLinearEquationSolver::AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) :
-        precision(precision), relative(relativeError), maximalNumberOfIterations(maximalIterations), trackPolicy(trackPolicy)
-        {
+        template<typename ValueType>
+        AbstractMinMaxLinearEquationSolver<ValueType>::AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech) : precision(precision), relative(relativeError), maximalNumberOfIterations(maximalIterations), trackScheduler(trackScheduler) {
             
             if(prefTech == MinMaxTechniqueSelection::FROMSETTINGS) {
                 useValueIteration = (storm::settings::generalSettings().getMinMaxEquationSolvingTechnique() == storm::solver::MinMaxTechnique::ValueIteration);
@@ -19,13 +18,34 @@ namespace storm {
             }
         }
         
-        void AbstractMinMaxLinearEquationSolver::setPolicyTracking(bool setToTrue) {
-            trackPolicy = setToTrue;
+        template<typename ValueType>
+        void AbstractMinMaxLinearEquationSolver<ValueType>::setTrackScheduler(bool trackScheduler) {
+            this->trackScheduler = trackScheduler;
         }
         
-        std::vector<storm::storage::sparse::state_type> AbstractMinMaxLinearEquationSolver::getPolicy() const {
-            STORM_LOG_THROW(!useValueIteration, storm::exceptions::NotImplementedException, "Getting policies after value iteration is not yet supported!");
-            return policy;
+        template<typename ValueType>
+        bool AbstractMinMaxLinearEquationSolver<ValueType>::isTrackSchedulerSet() const {
+            return this->trackScheduler;
         }
+        
+        template<typename ValueType>
+        storm::storage::Scheduler const& AbstractMinMaxLinearEquationSolver<ValueType>::getScheduler() const {
+            STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated.");
+            return *scheduler.get();
+        }
+        
+        template<typename ValueType>
+        void AbstractMinMaxLinearEquationSolver<ValueType>::setOptimizationDirection(OptimizationDirection d) {
+            direction = convert(d);
+        }
+        
+        template<typename ValueType>
+        void AbstractMinMaxLinearEquationSolver<ValueType>::resetOptimizationDirection() {
+            direction = OptimizationDirectionSetting::Unset;
+        }
+        
+        template class AbstractMinMaxLinearEquationSolver<float>;
+        template class AbstractMinMaxLinearEquationSolver<double>;
+
     }
 }

src/solver/MinMaxLinearEquationSolver.h

@@ -5,6 +5,8 @@
 #include <cstdint>
 #include <memory>
 
+#include <boost/optional.hpp>
+
 #include "src/solver/AbstractEquationSolver.h"
 #include "src/solver/SolverSelectionOptions.h"
 #include "src/storage/sparse/StateType.h"
@@ -26,20 +28,13 @@ namespace storm {
         template<typename ValueType>
         class AbstractMinMaxLinearEquationSolver : public AbstractEquationSolver<ValueType> {
         public:
-            void setSchedulerTracking(bool trackScheduler = true);
+            void setTrackScheduler(bool trackScheduler = true);
+            bool isTrackSchedulerSet() const;
             
-            std::vector<storm::storage::sparse::state_type> getScheduler() const {
-                STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated.");
-                return scheduler.get();
-            }
+            storm::storage::Scheduler const& getScheduler() const;
             
-            void setOptimizationDirection(OptimizationDirection d) {
-                direction = convert(d);
-            }
-            
-            void resetOptimizationDirection() {
-                direction = OptimizationDirectionSetting::Unset;
-            }
+            void setOptimizationDirection(OptimizationDirection d);
+            void resetOptimizationDirection();
                         
         protected:
             AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech);
@@ -63,7 +58,7 @@ namespace storm {
             bool trackScheduler;
             
             // The scheduler (if it could be successfully generated).
-            boost::optional<std::unique_ptr<storm::storage::Scheduler>> scheduler;
+            mutable boost::optional<std::unique_ptr<storm::storage::Scheduler>> scheduler;
         };
         
         /*!

src/solver/NativeLinearEquationSolver.cpp

@@ -51,7 +51,7 @@ namespace storm {
                     A.performSuccessiveOverRelaxationStep(omega, x, b);
                     
                     // Now check if the process already converged within our precision.
-                    converged = storm::utility::vector::equalModuloPrecision<ValueType>(x, *tmpX, static_cast<ValueType>(precision), relative);
+                    converged = storm::utility::vector::equalModuloPrecision<ValueType>(x, *tmpX, static_cast<ValueType>(precision), relative) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x));
                     
                     // If we did not yet converge, we need to copy the contents of x to *tmpX.
                     if (!converged) {
@@ -87,7 +87,7 @@ namespace storm {
                 uint_fast64_t iterationCount = 0;
                 bool converged = false;
                 
-                while (!converged && iterationCount < maximalNumberOfIterations) {
+                while (!converged && iterationCount < maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
                     // Compute D^-1 * (b - LU * x) and store result in nextX.
                     jacobiDecomposition.first.multiplyWithVector(*currentX, tmpX);
                     storm::utility::vector::subtractVectors(b, tmpX, tmpX);

src/solver/NativeMinMaxLinearEquationSolver.cpp

@@ -2,7 +2,7 @@
 
 #include <utility>
 
-
+#include "src/storage/TotalScheduler.h"
 
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/NativeEquationSolverSettings.h"
@@ -53,7 +53,7 @@ namespace storm {
 
 				// Proceed with the iterations as long as the method did not converge or reach the
 				// user-specified maximum number of iterations.
-				while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) {
+				while (!converged && iterations < this->maximalNumberOfIterations && (!this->hasCustomTerminationCondition() || this->getTerminationCondition().terminateNow(*currentX))) {
 					// Compute x' = A*x + b.
 					this->A.multiplyWithVector(*currentX, *multiplyResult);
 					storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult);
@@ -93,7 +93,7 @@ namespace storm {
 			} else {
 				// We will use Policy Iteration to solve the given system.
 				// We first guess an initial choice resolution which will be refined after each iteration.
-				this->policy = std::vector<storm::storage::sparse::state_type>(this->A.getRowGroupIndices().size() - 1);
+				std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupIndices().size() - 1);
 
 				// Create our own multiplyResult for solving the deterministic sub-instances.
 				std::vector<ValueType> deterministicMultiplyResult(this->A.getRowGroupIndices().size() - 1);
@@ -121,13 +121,13 @@ namespace storm {
 
 				// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
 				// of iterations.
-				while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) {
+				while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
 					// Take the sub-matrix according to the current choices
-					storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(this->policy, true);
+					storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
 					submatrix.convertToEquationSystem();
 
 					NativeLinearEquationSolver<ValueType> nativeLinearEquationSolver(submatrix);
-					storm::utility::vector::selectVectorValues<ValueType>(subB, this->policy, this->A.getRowGroupIndices(), b);
+					storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A.getRowGroupIndices(), b);
 
 					// Copy X since we will overwrite it
 					std::copy(currentX->begin(), currentX->end(), newX->begin());
@@ -141,7 +141,7 @@ namespace storm {
 
 					// Reduce the vector x by applying min/max over all nondeterministic choices.
 					// Here, we capture which choice was taken in each state, thereby refining our initial guess.
-					storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(this->policy));
+					storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(scheduler));
 					
 
 					// Determine whether the method converged.
@@ -158,8 +158,12 @@ namespace storm {
 				} else {
 					LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations.");
 				}
-                
 
+                // If requested, we store the scheduler for retrieval.
+                if (this->isTrackSchedulerSet()) {
+                    this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(scheduler));
+                }
+                
 				// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
 				// is currently stored in currentX, but x is the output vector.
 				if (currentX == copyX) {

src/solver/SolveGoal.cpp

@@ -17,7 +17,7 @@ namespace storm {
         std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> configureMinMaxLinearEquationSolver(BoundedGoal<ValueType> const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& factory, storm::storage::SparseMatrix<ValueType> const& matrix) {
             std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> p = factory.create(matrix);
             p->setOptimizationDirection(goal.direction());
-            p->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumPassesThresholdValue<double>>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize()));
+            p->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumExceedsThreshold<double>>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize()));
             return p;
         }
         
@@ -34,8 +34,7 @@ namespace storm {
         template<typename ValueType>
         std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> configureLinearEquationSolver(BoundedGoal<ValueType> const& goal, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& factory, storm::storage::SparseMatrix<ValueType> const& matrix) {
             std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = factory.create(matrix);
-            solver->setOptimizationDirection(goal.direction());
-            solver->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumPassesThresholdValue<double>>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize()));
+            solver->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumExceedsThreshold<double>>(goal.relevantValues(), goal.thresholdValue(), goal.boundIsStrict(), goal.minimize()));
             return solver;
         }
         

src/solver/SolveGoal.h

@@ -77,12 +77,16 @@ namespace storm {
                 return (bound.comparisonType == storm::logic::ComparisonType::Greater || bound.comparisonType == storm::logic::ComparisonType::GreaterEqual);
             }
             
+            bool boundIsStrict() const {
+                return (bound.comparisonType == storm::logic::ComparisonType::Greater || bound.comparisonType == storm::logic::ComparisonType::Less);
+            }
+            
             ValueType const& thresholdValue() const {
                 return bound.threshold;
             }
             
             storm::storage::BitVector const& relevantValues() const {
-                return relevantValues;
+                return relevantValueVector;
             }
             
         private:

src/solver/TerminationCondition.cpp

@@ -29,9 +29,9 @@ namespace storm {
         }
         
         template<typename ValueType>
-        bool TerminateIfFilteredExtremumExceedsThreshold<ValueType>::terminateNow(const std::vector<ValueType>& currentValues) const {
-            STORM_LOG_ASSERT(currentValues.size() == filter.size(), "Vectors sizes mismatch.");
-            ValueType currentValue = useMinimum ? storm::utility::vector::min_if(currentValues, filter) : storm::utility::vector::max_if(currentValues, filter);
+        bool TerminateIfFilteredExtremumExceedsThreshold<ValueType>::terminateNow(std::vector<ValueType> const& currentValues) const {
+            STORM_LOG_ASSERT(currentValues.size() == this->filter.size(), "Vectors sizes mismatch.");
+            ValueType currentValue = useMinimum ? storm::utility::vector::min_if(currentValues, this->filter) : storm::utility::vector::max_if(currentValues, this->filter);
             return this->strict ? currentValue > this->threshold : currentValue >= this->threshold;
         }
         

src/solver/TerminationCondition.h

@@ -38,8 +38,6 @@ namespace storm {
             bool terminateNow(std::vector<ValueType> const& currentValue) const;
             
         protected:
-            ValueType threshold;
-            storm::storage::BitVector filter;
             bool useMinimum;
         };
     }

src/storage/TotalScheduler.cpp

@@ -11,6 +11,10 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        TotalScheduler::TotalScheduler(std::vector<uint_fast64_t>&& choices) : choices(std::move(choices)) {
+            // Intentionally left empty.
+        }
+        
         void TotalScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) {
             if (state > choices.size()) {
                 throw storm::exceptions::InvalidArgumentException() << "Invalid call to TotalScheduler::setChoice: scheduler cannot not define a choice for state " << state << ".";

src/storage/TotalScheduler.h

@@ -25,7 +25,14 @@ namespace storm {
              * @param choices A vector whose i-th entry defines the choice of state i.
              */
             TotalScheduler(std::vector<uint_fast64_t> const& choices);
-            
+
+            /*!
+             * Creates a total scheduler that defines the choices for states according to the given vector.
+             *
+             * @param choices A vector whose i-th entry defines the choice of state i.
+             */
+            TotalScheduler(std::vector<uint_fast64_t>&& choices);
+
             void setChoice(uint_fast64_t state, uint_fast64_t choice) override;
             
             bool isChoiceDefined(uint_fast64_t state) const override;

src/utility/solver.cpp

@@ -105,8 +105,7 @@ namespace storm {
             }
             
             template<typename ValueType>
-            std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackPolicy) const {
-                
+            std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackScheduler) const {
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> p1;
                 
                 switch (solverType) {
@@ -127,7 +126,7 @@ namespace storm {
                         break;
                     }
                 }
-                p1->setPolicyTracking(trackPolicy);
+                p1->setTrackScheduler(trackScheduler);
                 return p1;
                 
             }

src/utility/solver.h

@@ -113,7 +113,7 @@ 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 trackPolicy = false) const;
+                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);
                 

test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp

@@ -39,7 +39,8 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio
         
     double bound = 0.8;
     storm::solver::GmmxxMinMaxLinearEquationSolver<double> solver(A);
-    solver.setEarlyTerminationCriterion(std::make_unique<storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue<double>>(storm::storage::BitVector(1, true), bound, true));
+    
+    solver.setTerminationCondition(std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<double>>(storm::storage::BitVector(A.getRowGroupCount(), true), bound, false, true));
     ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Minimize, x, b));
     ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision());
     
@@ -47,11 +48,10 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio
     ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision());
     
     bound = 0.6;
-    solver.setEarlyTerminationCriterion(std::make_unique<storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue<double>>(storm::storage::BitVector(1, true), bound, true));
+    solver.setTerminationCondition(std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<double>>(storm::storage::BitVector(A.getRowGroupCount(), true), bound, false, true));
     
     ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Maximize, x, b));
     ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision());
-    
 }
 
 TEST(GmmxxMinMaxLinearEquationSolver, MatrixVectorMultiplication) {

test/functional/utility/VectorTest.cpp

@@ -18,8 +18,8 @@ TEST(VectorTest, max_if) {
     storm::storage::BitVector f1(5, {2,4});
     storm::storage::BitVector f2(5, {3,4});
     
-    ASSERT_EQ(34.0, storm::utility::vector::max_if(a,f1,0.0));
-    ASSERT_EQ(16.0, storm::utility::vector::max_if(a,f2,0.0));
+    ASSERT_EQ(34.0, storm::utility::vector::max_if(a, f1));
+    ASSERT_EQ(16.0, storm::utility::vector::max_if(a, f2));
 }
 
 
@@ -28,6 +28,6 @@ TEST(VectorTest, min_if) {
     storm::storage::BitVector f1(5, {2,4});
     storm::storage::BitVector f2(5, {3,4});
     
-    ASSERT_EQ(16.0, storm::utility::vector::min_if(a,f1,100.0));
-    ASSERT_EQ(8.0, storm::utility::vector::min_if(a,f2,100.0));
+    ASSERT_EQ(16.0, storm::utility::vector::min_if(a, f1));
+    ASSERT_EQ(8.0, storm::utility::vector::min_if(a, f2));
 }