fixed tests, removed old files

Former-commit-id: 90381faa73

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -2,6 +2,8 @@
 
 #include "src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h"
 
+#include "src/modelchecker/multiobjective/pcaa.h"
+
 #include "src/models/sparse/StandardRewardModel.h"
 
 #include "src/utility/macros.h"
@@ -34,7 +36,15 @@ namespace storm {
             storm::logic::Formula const& formula = checkTask.getFormula();
             storm::logic::FragmentSpecification fragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setReachabilityRewardFormulasAllowed(true);
             fragment.setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true);
-            return formula.isInFragment(fragment);
+            if(formula.isInFragment(fragment)) {
+                return true;
+            } else {
+                fragment = storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true);
+                //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states.
+                if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
+                if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
+                return formula.isInFragment(fragment);
+            }
         }
         
         template<typename SparseMarkovAutomatonModelType>
@@ -107,7 +117,12 @@ namespace storm {
             std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(result)));
         }
-                
+        
+        template<typename SparseMarkovAutomatonModelType>
+        std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) {
+            return multiobjective::performPcaa(this->getModel(), checkTask.getFormula());
+        }
+        
         template class SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<double>>;
     }
 }

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@@ -26,6 +26,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
             
         private:
             // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices.

src/modelchecker/multiobjective/Pcaa.cpp

@@ -9,6 +9,8 @@
 #include "src/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h"
 #include "src/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h"
 #include "src/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h"
+#include "src/settings//SettingsManager.h"
+#include "src/settings/modules/MultiObjectiveSettings.h"
 
 #include "src/exceptions/InvalidArgumentException.h"
 
@@ -22,6 +24,12 @@ namespace storm {
                 STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported.");
                 
 #ifdef STORM_HAVE_CARL
+                
+                // If we consider an MA, ensure that it is closed
+                if(model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                    STORM_LOG_THROW(dynamic_cast<storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType> const *>(&model)->isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula on non-closed Markov automaton.");
+                }
+                
                 auto preprocessorResult = SparsePcaaPreprocessor<SparseModelType>::preprocess(model, formula);
                 STORM_LOG_DEBUG("Preprocessing done. Result: " << preprocessorResult);
                 
@@ -41,7 +49,12 @@ namespace storm {
                         break;
                 }
 
-                return query->check();
+                auto result = query->check();
+                
+                if(settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isExportPlotSet()) {
+                    query->exportPlotOfCurrentApproximation(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotDirectory());
+                }
+                return result;
 #else
                 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi-objective model checking requires carl.");
                 return nullptr;

src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp

@@ -1,46 +0,0 @@
-#include "src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h"
-
-#include "src/utility/macros.h"
-#include "src/logic/Formulas.h"
-#include "src/logic/FragmentSpecification.h"
-
-#include "src/models/sparse/StandardRewardModel.h"
-
-#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
-#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
-
-#include "src/modelchecker/multiobjective/pcaa.h"
-
-#include "src/exceptions/InvalidArgumentException.h"
-
-namespace storm {
-    namespace modelchecker {
-        template<typename SparseMaModelType>
-        SparseMaMultiObjectiveModelChecker<SparseMaModelType>::SparseMaMultiObjectiveModelChecker(SparseMaModelType const& model) : SparseMarkovAutomatonCslModelChecker<SparseMaModelType>(model) {
-            // Intentionally left empty.
-        }
-        
-        template<typename SparseMaModelType>
-        bool SparseMaMultiObjectiveModelChecker<SparseMaModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
-            // A formula without multi objective (sub)formulas can be handled by the base class
-            if(SparseMarkovAutomatonCslModelChecker<SparseMaModelType>::canHandle(checkTask)) return true;
-            //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude this.
-            if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
-            if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
-            return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
-        }
-        
-        template<typename SparseMaModelType>
-        std::unique_ptr<CheckResult> SparseMaMultiObjectiveModelChecker<SparseMaModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) {
-            STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported.");
-            STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula in non-closed Markov automaton.");
-
-            return multiobjective::performPcaa(this->getModel(), checkTask.getFormula());
-        }
-        
-        
-                
-        template class SparseMaMultiObjectiveModelChecker<storm::models::sparse::MarkovAutomaton<double>>;
-    //    template class SparseMaMultiObjectiveModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
-    }
-}

src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h

@@ -1,27 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMAMULTIOBJECTIVEMODELCHECKER_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMAMULTIOBJECTIVEMODELCHECKER_H_
-
-#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
-
-namespace storm {
-    namespace modelchecker {
-        template<class SparseMaModelType>
-        class SparseMaMultiObjectiveModelChecker : public SparseMarkovAutomatonCslModelChecker<SparseMaModelType> {
-        public:
-            typedef typename SparseMaModelType::ValueType ValueType;
-            typedef typename SparseMaModelType::RewardModelType RewardModelType;
-            
-            explicit SparseMaMultiObjectiveModelChecker(SparseMaModelType const& model);
-            
-            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
-
-            virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
-            
-        private:
-
-
-        };
-    } // namespace modelchecker
-} // namespace storm
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMAMULTIOBJECTIVEMODELCHECKER_H_ */

src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp

@@ -1,43 +0,0 @@
-#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h"
-
-#include "src/utility/macros.h"
-#include "src/logic/Formulas.h"
-#include "src/logic/FragmentSpecification.h"
-
-#include "src/models/sparse/StandardRewardModel.h"
-
-#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
-#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
-
-#include "src/modelchecker/multiobjective/pcaa.h"
-
-namespace storm {
-    namespace modelchecker {
-        template<typename SparseMdpModelType>
-        SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::SparseMdpMultiObjectiveModelChecker(SparseMdpModelType const& model) : SparseMdpPrctlModelChecker<SparseMdpModelType>(model) {
-            // Intentionally left empty.
-        }
-        
-        template<typename SparseMdpModelType>
-        bool SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
-            // A formula without multi objective (sub)formulas can be handled by the base class
-            if(SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandle(checkTask)) return true;
-            //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude this.
-            if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
-            if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
-            return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
-        }
-        
-        template<typename SparseMdpModelType>
-        std::unique_ptr<CheckResult> SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) {
-            STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi Objective Model checking on model with multiple initial states is not supported.");
-            return multiobjective::performPcaa(this->getModel(), checkTask.getFormula());
-        }
-        
-                
-        template class SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>>;
-#ifdef STORM_HAVE_CARL
-        template class SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
-#endif
-    }
-}

src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h

@@ -1,27 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_
-
-#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
-
-namespace storm {
-    namespace modelchecker {
-        template<class SparseMdpModelType>
-        class SparseMdpMultiObjectiveModelChecker : public SparseMdpPrctlModelChecker<SparseMdpModelType> {
-        public:
-            typedef typename SparseMdpModelType::ValueType ValueType;
-            typedef typename SparseMdpModelType::RewardModelType RewardModelType;
-            
-            explicit SparseMdpMultiObjectiveModelChecker(SparseMdpModelType const& model);
-            
-            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
-
-            virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
-            
-        private:
-
-
-        };
-    } // namespace modelchecker
-} // namespace storm
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ */

src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp

@@ -1,422 +0,0 @@
-#include "src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h"
-
-#include <cmath>
-
-#include "src/adapters/CarlAdapter.h"
-#include "src/models/sparse/MarkovAutomaton.h"
-#include "src/models/sparse/StandardRewardModel.h"
-#include "src/transformer/EndComponentEliminator.h"
-#include "src/utility/macros.h"
-#include "src/utility/vector.h"
-
-#include "src/exceptions/InvalidOperationException.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            template <class SparseMaModelType>
-            SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::SparseMaMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker<SparseMaModelType>(data) {
-                // Set the (discretized) state action rewards.
-                this->discreteActionRewards.resize(data.objectives.size());
-                for(auto objIndex : this->objectivesWithNoUpperTimeBound) {
-                    typename SparseMaModelType::RewardModelType const& rewModel = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName);
-                    STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected.");
-                    this->discreteActionRewards[objIndex] = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector<ValueType>(this->data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
-                    if(rewModel.hasStateRewards()) {
-                        // Note that state rewards are earned over time and thus play no role for probabilistic states
-                        for(auto markovianState : this->data.getMarkovianStatesOfPreprocessedModel()) {
-                            this->discreteActionRewards[objIndex][this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[markovianState]] += rewModel.getStateReward(markovianState) / this->data.preprocessedModel.getExitRate(markovianState);
-                        }
-                    }
-                }
-            }
-            
-            template <class SparseMaModelType>
-            void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
-                
-                // Split the preprocessed model into transitions from/to probabilistic/Markovian states.
-                SubModel MS = createSubModel(true, weightedRewardVector);
-                SubModel PS = createSubModel(false, weightedRewardVector);
-
-                // Apply digitization to Markovian transitions
-                ValueType digitizationConstant = getDigitizationConstant();
-                digitize(MS, digitizationConstant);
-                
-                // Get for each occurring (digitized) timeBound the indices of the objectives with that bound.
-                TimeBoundMap lowerTimeBounds;
-                TimeBoundMap upperTimeBounds;
-                digitizeTimeBounds(lowerTimeBounds, upperTimeBounds, digitizationConstant);
-                
-                // Initialize a minMaxSolver to compute an optimal scheduler (w.r.t. PS) for each epoch
-                // The end components that stay in PS will be removed.
-                // Note that the end component elimination could be omitted if we forbid zeno behavior
-                std::unique_ptr<MinMaxSolverData> minMax = initMinMaxSolverData(PS);
-                
-                // Store the optimal choices of PS as computed by the minMax solver.
-                std::vector<uint_fast64_t> optimalChoicesAtCurrentEpoch(PS.getNumberOfStates(), std::numeric_limits<uint_fast64_t>::max());
-                
-                // create a linear equation solver for the model induced by the optimal choice vector.
-                // the solver will be updated whenever the optimal choice vector has changed.
-                // We choose Jacobi since we call the solver very frequently on 'easy' inputs (note that jacobi without preconditioning has very little overhead).
-                LinEqSolverData linEq;
-                linEq.factory.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Jacobi);
-                linEq.factory.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None);
-                linEq.b.resize(PS.getNumberOfStates());
-                
-                // Stores the objectives for which we need to compute values in the current time epoch.
-                storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound;
-                
-                auto lowerTimeBoundIt = lowerTimeBounds.begin();
-                auto upperTimeBoundIt = upperTimeBounds.begin();
-                uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first);
-                while(true) {
-                    // Update the objectives that are considered at the current time epoch as well as the (weighted) reward vectors.
-                    updateDataToCurrentEpoch(MS, PS, *minMax, consideredObjectives, currentEpoch, weightVector, lowerTimeBoundIt, lowerTimeBounds, upperTimeBoundIt, upperTimeBounds);
-                    
-                    // Compute the values that can be obtained at probabilistic states in the current time epoch
-                    performPSStep(PS, MS, *minMax, linEq, optimalChoicesAtCurrentEpoch,  consideredObjectives);
-                    
-                    // Compute values that can be obtained at Markovian states after letting one (digitized) time unit pass.
-                    // Only perform such a step if there is time left.
-                    if(currentEpoch>0) {
-                        performMSStep(MS, PS, consideredObjectives);
-                        --currentEpoch;
-                    } else {
-                        break;
-                    }
-                }
-                
-                // compose the results from MS and PS
-                storm::utility::vector::setVectorValues(this->weightedResult, MS.states, MS.weightedSolutionVector);
-                storm::utility::vector::setVectorValues(this->weightedResult, PS.states, PS.weightedSolutionVector);
-                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
-                    storm::utility::vector::setVectorValues(this->objectiveResults[objIndex], MS.states, MS.objectiveSolutionVectors[objIndex]);
-                    storm::utility::vector::setVectorValues(this->objectiveResults[objIndex], PS.states, PS.objectiveSolutionVectors[objIndex]);
-                }
-            }
-            
-            
-            template <class SparseMaModelType>
-            typename SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::SubModel SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::createSubModel(bool createMS, std::vector<ValueType> const& weightedRewardVector) const {
-                SubModel result;
-                
-                storm::storage::BitVector probabilisticStates = ~this->data.getMarkovianStatesOfPreprocessedModel();
-                result.states = createMS ? this->data.getMarkovianStatesOfPreprocessedModel() : probabilisticStates;
-                result.choices = this->data.preprocessedModel.getTransitionMatrix().getRowIndicesOfRowGroups(result.states);
-                STORM_LOG_ASSERT(!createMS || result.states.getNumberOfSetBits() == result.choices.getNumberOfSetBits(), "row groups for Markovian states should consist of exactly one row");
-                
-                //We need to add diagonal entries for selfloops on Markovian states.
-                result.toMS = this->data.preprocessedModel.getTransitionMatrix().getSubmatrix(true, result.states, this->data.getMarkovianStatesOfPreprocessedModel(), createMS);
-                result.toPS = this->data.preprocessedModel.getTransitionMatrix().getSubmatrix(true, result.states, probabilisticStates, false);
-                STORM_LOG_ASSERT(result.getNumberOfStates() == result.states.getNumberOfSetBits() && result.getNumberOfStates() == result.toMS.getRowGroupCount() && result.getNumberOfStates() == result.toPS.getRowGroupCount(), "Invalid state count for subsystem");
-                STORM_LOG_ASSERT(result.getNumberOfChoices() == result.choices.getNumberOfSetBits() && result.getNumberOfChoices() == result.toMS.getRowCount() && result.getNumberOfChoices() == result.toPS.getRowCount(), "Invalid state count for subsystem");
-                
-                result.weightedRewardVector.resize(result.getNumberOfChoices());
-                storm::utility::vector::selectVectorValues(result.weightedRewardVector, result.choices, weightedRewardVector);
-                result.objectiveRewardVectors.resize(this->data.objectives.size());
-                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
-                    std::vector<ValueType>& objVector = result.objectiveRewardVectors[objIndex];
-                    objVector = std::vector<ValueType>(result.weightedRewardVector.size(), storm::utility::zero<ValueType>());
-                    if(this->objectivesWithNoUpperTimeBound.get(objIndex)) {
-                        storm::utility::vector::selectVectorValues(objVector, result.choices, this->discreteActionRewards[objIndex]);
-                    } else {
-                        typename SparseMaModelType::RewardModelType const& rewModel = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName);
-                        STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected.");
-                        STORM_LOG_ASSERT(!rewModel.hasStateRewards(), "State rewards for bounded objectives for MAs are not expected (bounded rewards are not supported).");
-                        if(rewModel.hasStateActionRewards()) {
-                            storm::utility::vector::selectVectorValues(objVector, result.choices, rewModel.getStateActionRewardVector());
-                        }
-                    }
-                }
-                
-                result.weightedSolutionVector.resize(result.getNumberOfStates());
-                storm::utility::vector::selectVectorValues(result.weightedSolutionVector, result.states, this->weightedResult);
-                result.objectiveSolutionVectors.resize(this->data.objectives.size());
-                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
-                    result.objectiveSolutionVectors[objIndex].resize(result.weightedSolutionVector.size());
-                    storm::utility::vector::selectVectorValues(result.objectiveSolutionVectors[objIndex], result.states, this->objectiveResults[objIndex]);
-                }
-                
-                result.auxChoiceValues.resize(result.getNumberOfChoices());
-                
-                return result;
-            }
-            
-            template <class SparseMaModelType>
-            template <typename VT, typename std::enable_if<storm::NumberTraits<VT>::SupportsExponential, int>::type>
-            VT SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::getDigitizationConstant() const {
-                STORM_LOG_DEBUG("Retrieving digitization constant");
-                // We need to find a delta such that for each objective it holds that lowerbound/delta , upperbound/delta are natural numbers and
-                // If there is a lower and an upper bound:
-                //     1 - e^(-maxRate lowerbound) * (1 + maxRate delta) ^ (lowerbound / delta) + 1-e^(-maxRate upperbound) * (1 + maxRate delta) ^ (upperbound / delta) + (1-e^(-maxRate delta) <= maximumLowerUpperBoundGap
-                // If there is only an upper bound:
-                //     1-e^(-maxRate upperbound) * (1 + maxRate delta) ^ (upperbound / delta) <= maximumLowerUpperBoundGap
-                
-                // Initialize some data for fast and easy access
-                VT const maxRate = this->data.preprocessedModel.getMaximalExitRate();
-                std::vector<std::pair<VT, VT>> eToPowerOfMinusMaxRateTimesBound;
-                VT smallestNonZeroBound = storm::utility::zero<VT>();
-                for(auto const& obj : this->data.objectives) {
-                    eToPowerOfMinusMaxRateTimesBound.emplace_back();
-                    if(obj.lowerTimeBound){
-                        STORM_LOG_ASSERT(!storm::utility::isZero(*obj.lowerTimeBound), "Got zero-valued lower bound."); // should have been handled in preprocessing
-                        STORM_LOG_ASSERT(!obj.upperTimeBound || *obj.lowerTimeBound < *obj.upperTimeBound, "Got point intervall or empty intervall on time bounded property which is not supported"); // should also have been handled in preprocessing
-                        eToPowerOfMinusMaxRateTimesBound.back().first = std::exp(-maxRate * (*obj.lowerTimeBound));
-                        smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? *obj.lowerTimeBound : std::min(smallestNonZeroBound, *obj.lowerTimeBound);
-                    }
-                    if(obj.upperTimeBound){
-                        STORM_LOG_ASSERT(!storm::utility::isZero(*obj.upperTimeBound), "Got zero-valued upper bound."); // should have been handled in preprocessing
-                        eToPowerOfMinusMaxRateTimesBound.back().second = std::exp(-maxRate * (*obj.upperTimeBound));
-                        smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? *obj.upperTimeBound : std::min(smallestNonZeroBound, *obj.upperTimeBound);
-                    }
-                }
-                if(storm::utility::isZero(smallestNonZeroBound)) {
-                    // There are no time bounds. In this case, one is a valid digitization constant.
-                    return storm::utility::one<VT>();
-                }
-                
-                // We brute-force a delta, since a direct computation is apparently not easy.
-                // Also note that the number of times this loop runs is a lower bound for the number of minMaxSolver invocations.
-                // Hence, this brute-force approach will most likely not be a bottleneck.
-                uint_fast64_t smallestStepBound = 1;
-                VT delta = smallestNonZeroBound / smallestStepBound;
-                while(true) {
-                    bool deltaValid = true;
-                    for(auto const& obj : this->data.objectives) {
-                        if((obj.lowerTimeBound && *obj.lowerTimeBound/delta != std::floor(*obj.lowerTimeBound/delta)) ||
-                           (obj.upperTimeBound && *obj.upperTimeBound/delta != std::floor(*obj.upperTimeBound/delta))) {
-                            deltaValid = false;
-                            break;
-                        }
-                    }
-                    if(deltaValid) {
-                        for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
-                            auto const& obj = this->data.objectives[objIndex];
-                            VT precisionOfObj = storm::utility::zero<VT>();
-                            if(obj.lowerTimeBound) {
-                                precisionOfObj += storm::utility::one<VT>() - (eToPowerOfMinusMaxRateTimesBound[objIndex].first * storm::utility::pow(storm::utility::one<VT>() + maxRate * delta, *obj.lowerTimeBound / delta) )
-                                + storm::utility::one<VT>() - std::exp(-maxRate * delta);
-                            }
-                            if(obj.upperTimeBound) {
-                                precisionOfObj += storm::utility::one<VT>() - (eToPowerOfMinusMaxRateTimesBound[objIndex].second * storm::utility::pow(storm::utility::one<VT>() + maxRate * delta, *obj.upperTimeBound / delta) );
-                            }
-                            if(precisionOfObj > this->maximumLowerUpperBoundGap) {
-                                deltaValid = false;
-                                break;
-                            }
-                        }
-                    }
-                    if(deltaValid) {
-                        break;
-                    }
-                    ++smallestStepBound;
-                    STORM_LOG_ASSERT(delta>smallestNonZeroBound / smallestStepBound, "Digitization constant is expected to become smaller in every iteration");
-                    delta = smallestNonZeroBound / smallestStepBound;
-                }
-                STORM_LOG_DEBUG("Found digitization constant: " << delta << ". At least " << smallestStepBound << " digitization steps will be necessarry");
-                return delta;
-            }
-            
-            template <class SparseMaModelType>
-            template <typename VT, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type>
-            VT SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::getDigitizationConstant() const {
-                  STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type.");
-            }
-            
-            template <class SparseMaModelType>
-            template <typename VT, typename std::enable_if<storm::NumberTraits<VT>::SupportsExponential, int>::type>
-            void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::digitize(SubModel& MS, VT const& digitizationConstant) const {
-                std::vector<VT> rateVector(MS.getNumberOfChoices());
-                storm::utility::vector::selectVectorValues(rateVector, MS.states, this->data.preprocessedModel.getExitRates());
-                for(uint_fast64_t row = 0; row < rateVector.size(); ++row) {
-                    VT const eToMinusRateTimesDelta = std::exp(-rateVector[row] * digitizationConstant);
-                    for(auto& entry : MS.toMS.getRow(row)) {
-                        entry.setValue((storm::utility::one<VT>() - eToMinusRateTimesDelta) * entry.getValue());
-                        if(entry.getColumn() == row) {
-                            entry.setValue(entry.getValue() + eToMinusRateTimesDelta);
-                        }
-                    }
-                    for(auto& entry : MS.toPS.getRow(row)) {
-                        entry.setValue((storm::utility::one<VT>() - eToMinusRateTimesDelta) * entry.getValue());
-                    }
-                    MS.weightedRewardVector[row] *= storm::utility::one<VT>() - eToMinusRateTimesDelta;
-                    for(auto& objVector : MS.objectiveRewardVectors) {
-                        objVector[row] *= storm::utility::one<VT>() - eToMinusRateTimesDelta;
-                    }
-                }
-            }
-            
-            template <class SparseMaModelType>
-            template <typename VT, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type>
-            void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::digitize(SubModel& subModel, VT const& digitizationConstant) const {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type.");
-            }
-
-            template <class SparseMaModelType>
-            template <typename VT, typename std::enable_if<storm::NumberTraits<VT>::SupportsExponential, int>::type>
-            void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) {
-                
-                VT const maxRate = this->data.preprocessedModel.getMaximalExitRate();
-                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
-                    auto const& obj = this->data.objectives[objIndex];
-                    VT errorTowardsZero;
-                    VT errorAwayFromZero;
-                    if(obj.lowerTimeBound) {
-                        uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>((*obj.lowerTimeBound)/digitizationConstant);
-                        auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
-                        timeBoundIt->second.set(objIndex);
-                        VT digitizationError = storm::utility::one<VT>();
-                        digitizationError -= std::exp(-maxRate * (*obj.lowerTimeBound)) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
-                        errorTowardsZero = -digitizationError;
-                        errorAwayFromZero = storm::utility::one<VT>() - std::exp(-maxRate * digitizationConstant);;
-                    } else {
-                        errorTowardsZero = storm::utility::zero<VT>();
-                        errorAwayFromZero = storm::utility::zero<VT>();
-                    }
-                    if(obj.upperTimeBound) {
-                        uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>((*obj.upperTimeBound)/digitizationConstant);
-                        auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
-                        timeBoundIt->second.set(objIndex);
-                        VT digitizationError = storm::utility::one<VT>();
-                        digitizationError -= std::exp(-maxRate * (*obj.upperTimeBound)) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
-                        errorAwayFromZero += digitizationError;
-                    }
-                    STORM_LOG_ASSERT(errorTowardsZero + errorAwayFromZero <= this->maximumLowerUpperBoundGap, "Precision not sufficient.");
-                    if (obj.rewardsArePositive) {
-                        this->offsetsToLowerBound[objIndex] = -errorTowardsZero;
-                        this->offsetsToUpperBound[objIndex] = errorAwayFromZero;
-                    } else {
-                        this->offsetsToLowerBound[objIndex] = -errorAwayFromZero;
-                        this->offsetsToUpperBound[objIndex] = errorTowardsZero;
-                    }
-                }
-            } 
-            
-            template <class SparseMaModelType>
-            template <typename VT, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type>
-            void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type.");
-            }
-            
-            template <class SparseMaModelType>
-            std::unique_ptr<typename SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::MinMaxSolverData> SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::initMinMaxSolverData(SubModel const& PS) const {
-                std::unique_ptr<MinMaxSolverData> result(new MinMaxSolverData());
-                
-                result->b.resize(result->matrix.getRowCount());
-                result->x.resize(result->matrix.getRowGroupCount());
-                for(uint_fast64_t state=0; state < result->fromPSStateMapping.size(); ++state) {
-                    if(result->fromPSStateMapping[state] < result->x.size()) {
-                        result->x[result->fromPSStateMapping[state]] = PS.weightedSolutionVector[state];
-                    }
-                }
-                
-                storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxSolverFactory;
-                result->solver = minMaxSolverFactory.create(result->matrix);
-                result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
-                result->solver->setTrackScheduler(true);
-                result->solver->allocateAuxMemory(storm::solver::MinMaxLinearEquationSolverOperation::SolveEquations);
-                
-                return result;
-            }
-
-            template <class SparseMaModelType>
-            void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector<ValueType> const& weightVector, TimeBoundMap::iterator& lowerTimeBoundIt, TimeBoundMap const& lowerTimeBounds, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) {
-                
-                //Note that lower time bounds are always strict. Hence, we need to react when the current epoch equals the stored bound.
-                if(lowerTimeBoundIt != lowerTimeBounds.end() && currentEpoch == lowerTimeBoundIt->first) {
-                    for(auto objIndex : lowerTimeBoundIt->second) {
-                        // No more reward is earned for this objective.
-                        storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], -weightVector[objIndex]);
-                        storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], -weightVector[objIndex]);
-                        MS.objectiveRewardVectors[objIndex] = std::vector<ValueType>(MS.objectiveRewardVectors[objIndex].size(), storm::utility::zero<ValueType>());
-                        PS.objectiveRewardVectors[objIndex] = std::vector<ValueType>(PS.objectiveRewardVectors[objIndex].size(), storm::utility::zero<ValueType>());
-                    }
-                    ++lowerTimeBoundIt;
-                }
-                
-                if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) {
-                    consideredObjectives |= upperTimeBoundIt->second;
-                    for(auto objIndex : upperTimeBoundIt->second) {
-                        // This objective now plays a role in the weighted sum
-                        storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], weightVector[objIndex]);
-                        storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], weightVector[objIndex]);
-                    }
-                    ++upperTimeBoundIt;
-                }
-                
-                // Update the solver data
-                PS.toMS.multiplyWithVector(MS.weightedSolutionVector, PS.auxChoiceValues);
-                storm::utility::vector::addVectors(PS.auxChoiceValues, PS.weightedRewardVector, PS.auxChoiceValues);
-                storm::utility::vector::selectVectorValues(minMax.b, minMax.toPSChoiceMapping, PS.auxChoiceValues);
-            }
-            
-            template <class SparseMaModelType>
-            void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector<uint_fast64_t>& optimalChoicesAtCurrentEpoch,  storm::storage::BitVector const& consideredObjectives) const {
-                // compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector
-                std::vector<uint_fast64_t> newOptimalChoices(PS.getNumberOfStates());
-                minMax.solver->solveEquations(minMax.x, minMax.b);
-                this->transformReducedSolutionToOriginalModel(minMax.matrix, minMax.x, minMax.solver->getScheduler()->getChoices(), minMax.toPSChoiceMapping, minMax.fromPSStateMapping, PS.toPS, PS.weightedSolutionVector, newOptimalChoices);
-                // check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed
-                if(linEq.solver == nullptr || newOptimalChoices != optimalChoicesAtCurrentEpoch) {
-                    optimalChoicesAtCurrentEpoch.swap(newOptimalChoices);
-                    linEq.solver = nullptr;
-                    storm::storage::SparseMatrix<ValueType> linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true);
-                    linEqMatrix.convertToEquationSystem();
-                    linEq.solver = linEq.factory.create(std::move(linEqMatrix));
-                    linEq.solver->allocateAuxMemory(storm::solver::LinearEquationSolverOperation::SolveEquations);
-                }
-                
-                // Get the results for the individual objectives.
-                // Note that we do not consider an estimate for each objective (as done in the unbounded phase) since the results from the previous epoch are already pretty close
-                for(auto objIndex : consideredObjectives) {
-                    auto const& objectiveRewardVectorPS = PS.objectiveRewardVectors[objIndex];
-                    auto const& objectiveSolutionVectorMS = MS.objectiveSolutionVectors[objIndex];
-                    // compute rhs of equation system, i.e., PS.toMS * x + Rewards
-                    // To safe some time, only do this for the obtained optimal choices
-                    auto itGroupIndex = PS.toPS.getRowGroupIndices().begin();
-                    auto itChoiceOffset = optimalChoicesAtCurrentEpoch.begin();
-                    for(auto& bValue : linEq.b) {
-                        uint_fast64_t row = (*itGroupIndex) + (*itChoiceOffset);
-                        bValue = objectiveRewardVectorPS[row];
-                        for(auto const& entry : PS.toMS.getRow(row)){
-                            bValue += entry.getValue() * objectiveSolutionVectorMS[entry.getColumn()];
-                        }
-                        ++itGroupIndex;
-                        ++itChoiceOffset;
-                    }
-                    linEq.solver->solveEquations(PS.objectiveSolutionVectors[objIndex], linEq.b);
-                }
-            }
-
-            template <class SparseMaModelType>
-            void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::performMSStep(SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives) const {
-                
-                MS.toMS.multiplyWithVector(MS.weightedSolutionVector, MS.auxChoiceValues);
-                storm::utility::vector::addVectors(MS.weightedRewardVector, MS.auxChoiceValues, MS.weightedSolutionVector);
-                MS.toPS.multiplyWithVector(PS.weightedSolutionVector, MS.auxChoiceValues);
-                storm::utility::vector::addVectors(MS.weightedSolutionVector, MS.auxChoiceValues, MS.weightedSolutionVector);
-                
-                for(auto objIndex : consideredObjectives) {
-                    MS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues);
-                    storm::utility::vector::addVectors(MS.objectiveRewardVectors[objIndex], MS.auxChoiceValues, MS.objectiveSolutionVectors[objIndex]);
-                    MS.toPS.multiplyWithVector(PS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues);
-                    storm::utility::vector::addVectors(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues, MS.objectiveSolutionVectors[objIndex]);
-                }
-            }
-            
-            
-            template class SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>;
-            template double SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::getDigitizationConstant<double>() const;
-            template void SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::digitize<double>(SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::SubModel& subModel, double const& digitizationConstant) const;
-            template void SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::digitizeTimeBounds<double>(SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::TimeBoundMap& lowerTimeBounds, SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant);
-#ifdef STORM_HAVE_CARL
-//            template class SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
-   //         template storm::RationalNumber SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::getDigitizationConstant<storm::RationalNumber>() const;
- //           template void SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::digitize<storm::RationalNumber>(SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::SubModel& subModel, storm::RationalNumber const& digitizationConstant) const;
-//            template void SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::digitizeTimeBounds<storm::RationalNumber>(SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::TimeBoundMap& lowerTimeBounds, SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant);
-#endif
-            
-        }
-    }
-}

src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h

@@ -1,157 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMAMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMAMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_
-
-#include <vector>
-#include <type_traits>
-
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h"
-#include "src/solver/LinearEquationSolver.h"
-#include "src/solver/GmmxxLinearEquationSolver.h"
-#include "src/solver/MinMaxLinearEquationSolver.h"
-#include "src/utility/NumberTraits.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            /*!
-             * Helper Class that takes preprocessed multi objective data and a weight vector and ...
-             * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
-             * - extracts the scheduler that induces this maximum
-             * - computes for each objective the value induced by this scheduler
-             */
-            template <class SparseMaModelType>
-            class SparseMaMultiObjectiveWeightVectorChecker : public SparseMultiObjectiveWeightVectorChecker<SparseMaModelType> {
-            public:
-                typedef typename SparseMaModelType::ValueType ValueType;
-                typedef SparseMultiObjectivePreprocessorData<SparseMaModelType> PreprocessorData;
-                
-                SparseMaMultiObjectiveWeightVectorChecker(PreprocessorData const& data);
-                
-            private:
-                
-                /*
-                 * Stores (digitized) time bounds in descending order
-                 */
-                typedef std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> TimeBoundMap;
-                
-                /*
-                 * Stores the ingredients of a sub model
-                 */
-                struct SubModel {
-                    storm::storage::BitVector states; // The states that are part of this sub model
-                    storm::storage::BitVector choices; // The choices that are part of this sub model
-                    
-                    storm::storage::SparseMatrix<ValueType> toMS; // Transitions to Markovian states
-                    storm::storage::SparseMatrix<ValueType> toPS; // Transitions to probabilistic states
-                    
-                    std::vector<ValueType> weightedRewardVector;
-                    std::vector<std::vector<ValueType>> objectiveRewardVectors;
-                    
-                    std::vector<ValueType> weightedSolutionVector;
-                    std::vector<std::vector<ValueType>> objectiveSolutionVectors;
-                    
-                    std::vector<ValueType> auxChoiceValues; //stores auxiliary values for every choice
-                    
-                    uint_fast64_t getNumberOfStates() const { return toMS.getRowGroupCount(); };
-                    uint_fast64_t getNumberOfChoices() const { return toMS.getRowCount(); };
-                };
-      
-                /*
-                 * Stores the data that is relevant to invoke the minMaxSolver and retrieve the result.
-                 */
-                struct MinMaxSolverData {
-                    std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver; // the solver itself
-                    
-                    storm::storage::SparseMatrix<ValueType> matrix; // the considered matrix
-                    std::vector<uint_fast64_t> toPSChoiceMapping;  // maps rows of the considered matrix to choices of the PS SubModel
-                    std::vector<uint_fast64_t> fromPSStateMapping; // maps states of the PS SubModel to row groups of the considered matrix
-                    
-                    std::vector<ValueType> b;
-                    std::vector<ValueType> x;
-                };
-                
-                struct LinEqSolverData {
-                    storm::solver::GmmxxLinearEquationSolverFactory<ValueType> factory;
-                    std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver;
-                    
-                    std::vector<ValueType> b;
-                };
-                
-                /*!
-                 *
-                 * @param weightVector the weight vector of the current check
-                 * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this.
-                 */
-                virtual void boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) override;
-                
-                /*!
-                 * Retrieves the data for a submodel of the data->preprocessedModel
-                 * @param createMS if true, the submodel containing the Markovian states is created.
-                 *                 if false, the submodel containing the probabilistic states is created.
-                 */
-                SubModel createSubModel(bool createMS, std::vector<ValueType> const& weightedRewardVector) const;
-                
-                /*!
-                 * Retrieves the delta used for digitization
-                 */
-                template <typename VT = ValueType, typename std::enable_if<storm::NumberTraits<VT>::SupportsExponential, int>::type = 0>
-                VT getDigitizationConstant() const;
-                template <typename VT = ValueType, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type = 0>
-                VT getDigitizationConstant() const;
-                
-                /*!
-                 * Digitizes the given matrix and vectors w.r.t. the given digitization constant and the given rate vector.
-                 */
-                template <typename VT = ValueType, typename std::enable_if<storm::NumberTraits<VT>::SupportsExponential, int>::type = 0>
-                void digitize(SubModel& subModel, VT const& digitizationConstant) const;
-                template <typename VT = ValueType, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type = 0>
-                void digitize(SubModel& subModel, VT const& digitizationConstant) const;
-                
-                /* 
-                 * Fills the given maps with the digitized time bounds. Also sets the offsetsToLowerBound / offsetsToUpperBound values
-                 * according to the digitization error
-                 */
-                template <typename VT = ValueType, typename std::enable_if<storm::NumberTraits<VT>::SupportsExponential, int>::type = 0>
-                void digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant);
-                template <typename VT = ValueType, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type = 0>
-                void digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant);
-                
-                
-                /*!
-                 * Computes a reduction of the PStoPS submodel which does not contain end components in which no choice with reward is taken.
-                 * With the reduction, a MinMaxSolver is initialized.
-                 */
-                std::unique_ptr<MinMaxSolverData> initMinMaxSolverData(SubModel const& PS) const;
-                
-                /*
-                 * Updates the reward vectors within the split model,
-                 * the reward vector of the reduced PStoPS model, and
-                 * objectives that are considered at the current time epoch.
-                 */
-                void updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector<ValueType> const& weightVector, TimeBoundMap::iterator& lowerTimeBoundIt, TimeBoundMap const& lowerTimeBounds, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds);
-                
-                /*
-                 * Performs a step for the probabilistic states, that is
-                 * * Compute an optimal scheduler for the weighted reward sum
-                 * * Compute the values for the individual objectives w.r.t. that scheduler
-                 * 
-                 * The resulting values represent the rewards at probabilistic states that are obtained at the current time epoch.
-                 */
-                void performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector<uint_fast64_t>& optimalChoicesAtCurrentEpoch,  storm::storage::BitVector const& consideredObjectives) const;
-                
-                /*
-                 * Performs a step for the Markovian states, that is
-                 * * Compute values for the weighted reward sum as well as for the individual objectives
-                 *
-                 * The resulting values represent the rewards at Markovian states that are obtained after one (digitized) time unit has passed.
-                 */
-                void performMSStep(SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives) const;
-                
-            };
-            
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMAMULTIOBJECTIVEWEIGHTEDVECTORCHECKER_H_ */

src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp

@@ -1,117 +0,0 @@
-#include "src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h"
-
-#include "src/adapters/CarlAdapter.h"
-#include "src/models/sparse/Mdp.h"
-#include "src/models/sparse/StandardRewardModel.h"
-#include "src/utility/macros.h"
-#include "src/utility/vector.h"
-
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            template <class SparseMdpModelType>
-            SparseMdpMultiObjectiveWeightVectorChecker<SparseMdpModelType>::SparseMdpMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker<SparseMdpModelType>(data) {
-                // set the state action rewards
-                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
-                    typename SparseMdpModelType::RewardModelType const& rewModel = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName);
-                    STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Reward model has transition rewards which is not expected.");
-                    this->discreteActionRewards[objIndex] = rewModel.getTotalRewardVector(this->data.preprocessedModel.getTransitionMatrix());
-                }
-            }
-            
-            template <class SparseMdpModelType>
-            void SparseMdpMultiObjectiveWeightVectorChecker<SparseMdpModelType>::boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
-                // Allocate some memory so this does not need to happen for each time epoch
-                std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(this->data.preprocessedModel.getNumberOfStates());
-                std::vector<ValueType> choiceValues(weightedRewardVector.size());
-                std::vector<ValueType> temporaryResult(this->data.preprocessedModel.getNumberOfStates());
-                std::vector<ValueType> zeroReward(weightedRewardVector.size(), storm::utility::zero<ValueType>());
-                // Get for each occurring timeBound the indices of the objectives with that bound.
-                std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> lowerTimeBounds;
-                std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> upperTimeBounds;
-                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
-                    auto const& obj = this->data.objectives[objIndex];
-                    if(obj.lowerTimeBound) {
-                        auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(storm::utility::convertNumber<uint_fast64_t>(*obj.lowerTimeBound), storm::storage::BitVector(this->data.objectives.size(), false))).first;
-                        STORM_LOG_WARN_COND(storm::utility::convertNumber<ValueType>(timeBoundIt->first) == (*obj.lowerTimeBound), "Rounded non-integral bound " << *obj.lowerTimeBound << " to " << timeBoundIt->first  << ".");
-                        timeBoundIt->second.set(objIndex);
-                    }
-                    if(obj.upperTimeBound) {
-                        auto timeBoundIt = upperTimeBounds.insert(std::make_pair(storm::utility::convertNumber<uint_fast64_t>(*obj.upperTimeBound), storm::storage::BitVector(this->data.objectives.size(), false))).first;
-                        STORM_LOG_WARN_COND(storm::utility::convertNumber<ValueType>(timeBoundIt->first) == (*obj.upperTimeBound), "Rounded non-integral bound " << *obj.upperTimeBound << " to " << timeBoundIt->first  << ".");
-                        timeBoundIt->second.set(objIndex);
-                        
-                        // There is no error for the values of these objectives.
-                        this->offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>();
-                        this->offsetsToUpperBound[objIndex] = storm::utility::zero<ValueType>();
-                    }
-                }
-                
-                // Stores the objectives for which we need to compute values in the current time epoch.
-                storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound;
-                
-                // Stores objectives for which the current epoch passed their lower bound
-                storm::storage::BitVector lowerBoundViolatedObjectives(consideredObjectives.size(), false);
-                
-                auto lowerTimeBoundIt = lowerTimeBounds.begin();
-                auto upperTimeBoundIt = upperTimeBounds.begin();
-                uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first - 1, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first); // consider lowerBound - 1 since we are interested in the first epoch that passes the bound
-                
-                while(currentEpoch > 0) {
-                    //For lower time bounds we need to react when the currentEpoch passed the bound
-                    // Hence, we substract 1 from the lower time bounds.
-                    if(lowerTimeBoundIt != lowerTimeBounds.end() && currentEpoch == lowerTimeBoundIt->first - 1) {
-                        lowerBoundViolatedObjectives |= lowerTimeBoundIt->second;
-                        for(auto objIndex : lowerTimeBoundIt->second) {
-                            // No more reward is earned for this objective.
-                            storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], -weightVector[objIndex]);
-                        }
-                        ++lowerTimeBoundIt;
-                    }
-                    
-                    if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) {
-                        consideredObjectives |= upperTimeBoundIt->second;
-                        for(auto objIndex : upperTimeBoundIt->second) {
-                            // This objective now plays a role in the weighted sum
-                            storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], weightVector[objIndex]);
-                        }
-                        ++upperTimeBoundIt;
-                    }
-                    
-                    // Get values and scheduler for weighted sum of objectives
-                    this->data.preprocessedModel.getTransitionMatrix().multiplyWithVector(this->weightedResult, choiceValues);
-                    storm::utility::vector::addVectors(choiceValues, weightedRewardVector, choiceValues);
-                    storm::utility::vector::reduceVectorMax(choiceValues, this->weightedResult, this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), &optimalChoicesInCurrentEpoch);
-                    
-                    // get values for individual objectives
-                    // TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results.
-                    for(auto objIndex : consideredObjectives) {
-                        std::vector<ValueType>& objectiveResult = this->objectiveResults[objIndex];
-                        std::vector<ValueType> const& objectiveRewards = lowerBoundViolatedObjectives.get(objIndex) ? zeroReward : this->discreteActionRewards[objIndex];
-                        auto rowGroupIndexIt = this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices().begin();
-                        auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin();
-                        for(ValueType& stateValue : temporaryResult){
-                            uint_fast64_t row = (*rowGroupIndexIt) + (*optimalChoiceIt);
-                            ++rowGroupIndexIt;
-                            ++optimalChoiceIt;
-                            stateValue = objectiveRewards[row];
-                            for(auto const& entry : this->data.preprocessedModel.getTransitionMatrix().getRow(row)) {
-                                stateValue += entry.getValue() * objectiveResult[entry.getColumn()];
-                            }
-                        }
-                        objectiveResult.swap(temporaryResult);
-                    }
-                    --currentEpoch;
-                }
-            }
-            
-            template class SparseMdpMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>;
-#ifdef STORM_HAVE_CARL
-            template class SparseMdpMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
-#endif
-            
-        }
-    }
-}

src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h

@@ -1,45 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_
-
-#include <vector>
-
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            /*!
-             * Helper Class that takes preprocessed multi objective data and a weight vector and ...
-             * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
-             * - extracts the scheduler that induces this maximum
-             * - computes for each objective the value induced by this scheduler
-             */
-            template <class SparseMdpModelType>
-            class SparseMdpMultiObjectiveWeightVectorChecker : public SparseMultiObjectiveWeightVectorChecker<SparseMdpModelType> {
-            public:
-                typedef typename SparseMdpModelType::ValueType ValueType;
-                typedef SparseMultiObjectivePreprocessorData<SparseMdpModelType> PreprocessorData;
-            
-                SparseMdpMultiObjectiveWeightVectorChecker(PreprocessorData const& data);
-                
-            private:
-                
-                /*!
-                 * For each time epoch (starting with the maximal stepBound occurring in the objectives), this method
-                 * - determines the objectives that are relevant in the current time epoch
-                 * - determines the maximizing scheduler for the weighted reward vector of these objectives
-                 * - computes the values of these objectives w.r.t. this scheduler
-                 *
-                 * @param weightVector the weight vector of the current check
-                 * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this.
-                 */
-                virtual void boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) override;
-  
-            };
-            
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEWEIGHTEDVECTORCHECKER_H_ */

src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp

@@ -1,353 +0,0 @@
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h"
-
-#include "src/adapters/CarlAdapter.h"
-#include "src/models/sparse/Mdp.h"
-#include "src/models/sparse/MarkovAutomaton.h"
-#include "src/models/sparse/StandardRewardModel.h"
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h"
-#include "src/utility/constants.h"
-#include "src/utility/vector.h"
-#include "src/settings//SettingsManager.h"
-#include "src/settings/modules/MultiObjectiveSettings.h"
-#include "src/settings/modules/GeneralSettings.h"
-
-#include "src/exceptions/UnexpectedException.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            
-            template <class SparseModelType, typename RationalNumberType>
-            typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::ResultData SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::check(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker) {
-                ResultData resultData;
-                resultData.overApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope();
-                resultData.underApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope();
-                
-                // Set the maximum gap between lower and upper bound of the weightVectorChecker result.
-                // This is the maximal edge length of the box we have to consider around each computed point
-                // We pick the gap such that the maximal distance between two points within this box is less than the given precision divided by two.
-                SparseModelValueType gap = storm::utility::convertNumber<SparseModelValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision());
-                gap /= (storm::utility::one<SparseModelValueType>() + storm::utility::one<SparseModelValueType>());
-                gap /= storm::utility::sqrt(static_cast<SparseModelValueType>(preprocessorData.objectives.size()));
-                weightVectorChecker->setMaximumLowerUpperBoundGap(gap);
-                
-                if(!checkIfPreprocessingWasConclusive(preprocessorData)) {
-                    switch(preprocessorData.queryType) {
-                        case PreprocessorData::QueryType::Achievability:
-                            achievabilityQuery(preprocessorData, weightVectorChecker, resultData);
-                            break;
-                        case PreprocessorData::QueryType::Numerical:
-                            numericalQuery(preprocessorData, weightVectorChecker, resultData);
-                            break;
-                        case PreprocessorData::QueryType::Pareto:
-                            paretoQuery(preprocessorData, weightVectorChecker, resultData);
-                            break;
-                        default:
-                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type");
-                    }
-                }
-                return resultData;
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::checkIfPreprocessingWasConclusive(PreprocessorData const& preprocessorData) {
-                if(preprocessorData.objectives.empty()) {
-                    return true;
-                }
-                for(auto const& preprocessorResult : preprocessorData.solutionsFromPreprocessing) {
-                    if(preprocessorResult.first == PreprocessorData::PreprocessorObjectiveSolution::False ||
-                       preprocessorResult.first == PreprocessorData::PreprocessorObjectiveSolution::Undefined) {
-                        return true;
-                    }
-                }
-                return false;
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::achievabilityQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) {
-                // Get a point that represents the thresholds
-                Point thresholds;
-                thresholds.reserve(preprocessorData.objectives.size());
-                storm::storage::BitVector strictThresholds(preprocessorData.objectives.size());
-                for(uint_fast64_t objIndex = 0; objIndex < preprocessorData.objectives.size(); ++objIndex) {
-                    thresholds.push_back(storm::utility::convertNumber<RationalNumberType>(*preprocessorData.objectives[objIndex].threshold));
-                    strictThresholds.set(objIndex, preprocessorData.objectives[objIndex].thresholdIsStrict);
-                }
-                // repeatedly refine the over/ under approximation until the threshold point is either in the under approx. or not in the over approx.
-                storm::storage::BitVector individualObjectivesToBeChecked(preprocessorData.objectives.size(), true);
-                do {
-                    WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked);
-                    performRefinementStep(std::move(separatingVector), preprocessorData.produceSchedulers, weightVectorChecker, resultData);
-                    if(!checkIfThresholdsAreSatisfied(resultData.overApproximation(), thresholds, strictThresholds)){
-                        resultData.setThresholdsAreAchievable(false);
-                    }
-                    if(checkIfThresholdsAreSatisfied(resultData.underApproximation(), thresholds, strictThresholds)){
-                        resultData.setThresholdsAreAchievable(true);
-                    }
-                } while(!resultData.isThresholdsAreAchievableSet() && !maxStepsPerformed(resultData));
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::numericalQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) {
-                STORM_LOG_ASSERT(preprocessorData.indexOfOptimizingObjective, "Detected numerical query but index of optimizing objective is not set.");
-                // initialize some data
-                uint_fast64_t optimizingObjIndex = *preprocessorData.indexOfOptimizingObjective;
-                Point thresholds;
-                thresholds.reserve(preprocessorData.objectives.size());
-                storm::storage::BitVector strictThresholds(preprocessorData.objectives.size(), false);
-                std::vector<storm::storage::geometry::Halfspace<RationalNumberType>> thresholdConstraints;
-                thresholdConstraints.reserve(preprocessorData.objectives.size()-1);
-                for(uint_fast64_t objIndex = 0; objIndex < preprocessorData.objectives.size(); ++objIndex) {
-                    if(preprocessorData.objectives[objIndex].threshold) {
-                        thresholds.push_back(storm::utility::convertNumber<RationalNumberType>(*preprocessorData.objectives[objIndex].threshold));
-                        WeightVector normalVector(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>());
-                        normalVector[objIndex] = -storm::utility::one<RationalNumberType>();
-                        thresholdConstraints.emplace_back(std::move(normalVector), -thresholds.back());
-                        strictThresholds.set(objIndex, preprocessorData.objectives[objIndex].thresholdIsStrict);
-                    } else {
-                        thresholds.push_back(storm::utility::zero<RationalNumberType>());
-                    }
-                }
-                // Note: If we have a single objective (i.e., no objectives with thresholds), thresholdsAsPolytope gets no constraints
-                auto thresholdsAsPolytope = storm::storage::geometry::Polytope<RationalNumberType>::create(thresholdConstraints);
-                WeightVector directionOfOptimizingObjective(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>());
-                directionOfOptimizingObjective[optimizingObjIndex] = storm::utility::one<RationalNumberType>();
-                
-                // Try to find one valid solution
-                storm::storage::BitVector individualObjectivesToBeChecked(preprocessorData.objectives.size(), true);
-                individualObjectivesToBeChecked.set(optimizingObjIndex, false);
-                do {
-                    WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked);
-                    performRefinementStep(std::move(separatingVector), preprocessorData.produceSchedulers, weightVectorChecker, resultData);
-                    //Pick the threshold for the optimizing objective low enough so valid solutions are not excluded
-                    thresholds[optimizingObjIndex] = std::min(thresholds[optimizingObjIndex], resultData.refinementSteps().back().getLowerBoundPoint()[optimizingObjIndex]);
-                    if(!checkIfThresholdsAreSatisfied(resultData.overApproximation(), thresholds, strictThresholds)){
-                        resultData.setThresholdsAreAchievable(false);
-                    }
-                    if(checkIfThresholdsAreSatisfied(resultData.underApproximation(), thresholds, strictThresholds)){
-                        resultData.setThresholdsAreAchievable(true);
-                    }
-                } while(!resultData.isThresholdsAreAchievableSet() && !maxStepsPerformed(resultData));
-                if(resultData.getThresholdsAreAchievable()) {
-                    STORM_LOG_DEBUG("Found a solution that satisfies the objective thresholds.");
-                    individualObjectivesToBeChecked.clear();
-                    // Improve the found solution.
-                    // Note that we do not have to care whether a threshold is strict anymore, because the resulting optimum should be
-                    // the supremum over all strategies. Hence, one could combine a scheduler inducing the optimum value (but possibly violating strict
-                    // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds.
-                    while(true) {
-                        std::pair<Point, bool> optimizationRes = resultData.underApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective);
-                        STORM_LOG_THROW(optimizationRes.second, storm::exceptions::UnexpectedException, "The underapproximation is either unbounded or empty.");
-                        thresholds[optimizingObjIndex] = optimizationRes.first[optimizingObjIndex];
-                        resultData.setNumericalResult(thresholds[optimizingObjIndex]);
-                        STORM_LOG_DEBUG("Best solution found so far is " << resultData.template getNumericalResult<double>() << ".");
-                        //Compute an upper bound for the optimum and check for convergence
-                        optimizationRes = resultData.overApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective);
-                        if(optimizationRes.second) {
-                            resultData.setPrecisionOfResult(optimizationRes.first[optimizingObjIndex] - thresholds[optimizingObjIndex]);
-                            STORM_LOG_DEBUG("Solution can be improved by at most " << resultData.template getPrecisionOfResult<double>());
-                        }
-                        if(targetPrecisionReached(resultData) || maxStepsPerformed(resultData)) {
-                            resultData.setOptimumIsAchievable(checkIfThresholdsAreSatisfied(resultData.underApproximation(), thresholds, strictThresholds));
-                            break;
-                        }
-                        WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked);
-                        performRefinementStep(std::move(separatingVector), preprocessorData.produceSchedulers, weightVectorChecker, resultData);
-                    }
-                }
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::paretoQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) {
-                //First consider the objectives individually
-                for(uint_fast64_t objIndex = 0; objIndex<preprocessorData.objectives.size() && !maxStepsPerformed(resultData); ++objIndex) {
-                    WeightVector direction(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>());
-                    direction[objIndex] = storm::utility::one<RationalNumberType>();
-                    performRefinementStep(std::move(direction), preprocessorData.produceSchedulers, weightVectorChecker, resultData);
-                }
-                
-                while(true) {
-                    // Get the halfspace of the underApproximation with maximal distance to a vertex of the overApproximation
-                    std::vector<storm::storage::geometry::Halfspace<RationalNumberType>> underApproxHalfspaces = resultData.underApproximation()->getHalfspaces();
-                    std::vector<Point> overApproxVertices = resultData.overApproximation()->getVertices();
-                    uint_fast64_t farestHalfspaceIndex = underApproxHalfspaces.size();
-                    RationalNumberType farestDistance = storm::utility::zero<RationalNumberType>();
-                    for(uint_fast64_t halfspaceIndex = 0; halfspaceIndex < underApproxHalfspaces.size(); ++halfspaceIndex) {
-                        for(auto const& vertex : overApproxVertices) {
-                            RationalNumberType distance = -underApproxHalfspaces[halfspaceIndex].euclideanDistance(vertex);
-                            if(distance > farestDistance) {
-                                farestHalfspaceIndex = halfspaceIndex;
-                                farestDistance = distance;
-                            }
-                        }
-                    }
-                    resultData.setPrecisionOfResult(farestDistance);
-                    STORM_LOG_DEBUG("Current precision of the approximation of the pareto curve is " << resultData.template getPrecisionOfResult<double>());
-                    if(targetPrecisionReached(resultData) || maxStepsPerformed(resultData)) {
-                        break;
-                    }
-                    WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector();
-                    performRefinementStep(std::move(direction), preprocessorData.produceSchedulers, weightVectorChecker, resultData);
-                }
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::WeightVector SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked) {
-                STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(pointToBeSeparated)) << ".");
-                
-                if(underApproximation->isEmpty()) {
-                    // In this case, every weight vector is  separating
-                    uint_fast64_t objIndex = individualObjectivesToBeChecked.getNextSetIndex(0) % pointToBeSeparated.size();
-                    WeightVector result(pointToBeSeparated.size(), storm::utility::zero<RationalNumberType>());
-                    result[objIndex] = storm::utility::one<RationalNumberType>();
-                    individualObjectivesToBeChecked.set(objIndex, false);
-                    return result;
-                }
-                
-                // Reaching this point means that the underApproximation contains halfspaces. The seperating vector has to be the normal vector of one of these halfspaces.
-                // We pick one with maximal distance to the given point. However, weight vectors that correspond to checking individual objectives take precedence.
-                std::vector<storm::storage::geometry::Halfspace<RationalNumberType>> halfspaces = underApproximation->getHalfspaces();
-                uint_fast64_t farestHalfspaceIndex = halfspaces.size();
-                RationalNumberType farestDistance = -storm::utility::one<RationalNumberType>();
-                bool foundSeparatingSingleObjectiveVector = false;
-                for(uint_fast64_t halfspaceIndex = 0; halfspaceIndex < halfspaces.size(); ++halfspaceIndex) {
-                    // Note that we are looking for a halfspace that does not contain the point. Thus, the returned distances are negated.
-                    RationalNumberType distance = -halfspaces[halfspaceIndex].euclideanDistance(pointToBeSeparated);
-                    if(distance >= storm::utility::zero<RationalNumberType>()) {
-                        storm::storage::BitVector nonZeroVectorEntries = ~storm::utility::vector::filterZero<RationalNumberType>(halfspaces[halfspaceIndex].normalVector());
-                        bool isSingleObjectiveVector = nonZeroVectorEntries.getNumberOfSetBits() == 1 && individualObjectivesToBeChecked.get(nonZeroVectorEntries.getNextSetIndex(0));
-                        // Check if this halfspace is better than the current one
-                        if((!foundSeparatingSingleObjectiveVector && isSingleObjectiveVector ) || (foundSeparatingSingleObjectiveVector==isSingleObjectiveVector && distance>farestDistance)) {
-                            foundSeparatingSingleObjectiveVector = foundSeparatingSingleObjectiveVector || isSingleObjectiveVector;
-                            farestHalfspaceIndex = halfspaceIndex;
-                            farestDistance = distance;
-                        }
-                    }
-                }
-                if(foundSeparatingSingleObjectiveVector) {
-                    storm::storage::BitVector nonZeroVectorEntries = ~storm::utility::vector::filterZero<RationalNumberType>(halfspaces[farestHalfspaceIndex].normalVector());
-                    individualObjectivesToBeChecked.set(nonZeroVectorEntries.getNextSetIndex(0), false);
-                }
-                
-                STORM_LOG_THROW(farestHalfspaceIndex<halfspaces.size(), storm::exceptions::UnexpectedException, "There is no seperating vector.");
-                STORM_LOG_DEBUG("Found separating  weight vector: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(halfspaces[farestHalfspaceIndex].normalVector())) << ".");
-                return halfspaces[farestHalfspaceIndex].normalVector();
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::performRefinementStep(WeightVector&& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& result) {
-                // Normalize the direction vector so that the entries sum up to one
-                storm::utility::vector::scaleVectorInPlace(direction, storm::utility::one<RationalNumberType>() / std::accumulate(direction.begin(), direction.end(), storm::utility::zero<RationalNumberType>()));
-                // Check if we already did a refinement step with that direction vector. If this is the case, we increase the precision.
-                // We start with the most recent steps to consider the most recent result for this direction vector
-                boost::optional<SparseModelValueType> oldMaximumLowerUpperBoundGap;
-                for(auto stepIt = result.refinementSteps().rbegin(); stepIt != result.refinementSteps().rend(); ++stepIt) {
-                    if(stepIt->getWeightVector() == direction) {
-                        STORM_LOG_WARN("Performing multiple refinement steps with the same direction vector.");
-                        oldMaximumLowerUpperBoundGap = weightVectorChecker->getMaximumLowerUpperBoundGap();
-                        std::vector<RationalNumberType> lowerUpperDistances = stepIt->getUpperBoundPoint();
-                        storm::utility::vector::subtractVectors(lowerUpperDistances, stepIt->getLowerBoundPoint(), lowerUpperDistances);
-                        // shorten the distance between lower and upper bound for the new result by multiplying the current distance with 0.5
-                        // TODO: try other values/strategies?
-                        RationalNumberType distance = storm::utility::sqrt(storm::utility::vector::dotProduct(lowerUpperDistances, lowerUpperDistances));
-                        weightVectorChecker->setMaximumLowerUpperBoundGap(std::min(*oldMaximumLowerUpperBoundGap, storm::utility::convertNumber<SparseModelValueType>(distance) * storm::utility::convertNumber<SparseModelValueType>(0.5)));
-                        break;
-                    }
-                }
-                weightVectorChecker->check(storm::utility::vector::convertNumericVector<SparseModelValueType>(direction));
-                if(oldMaximumLowerUpperBoundGap) {
-                    // Reset the precision back to the previous values
-                    weightVectorChecker->setMaximumLowerUpperBoundGap(*oldMaximumLowerUpperBoundGap);
-                }
-                STORM_LOG_DEBUG("weighted objectives checker result (lower bounds) is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(weightVectorChecker->getLowerBoundsOfInitialStateResults())));
-                
-                if(saveScheduler) {
-                    result.refinementSteps().emplace_back(direction,
-                                                          storm::utility::vector::convertNumericVector<RationalNumberType>(weightVectorChecker->getLowerBoundsOfInitialStateResults()),
-                                                          storm::utility::vector::convertNumericVector<RationalNumberType>(weightVectorChecker->getUpperBoundsOfInitialStateResults()),
-                                                          weightVectorChecker->getScheduler());
-                } else {
-                    result.refinementSteps().emplace_back(direction,
-                                                          storm::utility::vector::convertNumericVector<RationalNumberType>(weightVectorChecker->getLowerBoundsOfInitialStateResults()),
-                                                          storm::utility::vector::convertNumericVector<RationalNumberType>(weightVectorChecker->getUpperBoundsOfInitialStateResults()));
-                }
-                updateOverApproximation(result.refinementSteps(), result.overApproximation());
-                updateUnderApproximation(result.refinementSteps(), result.underApproximation());
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::updateOverApproximation(std::vector<RefinementStep> const& refinementSteps, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& overApproximation) {
-                storm::storage::geometry::Halfspace<RationalNumberType> h(refinementSteps.back().getWeightVector(), storm::utility::vector::dotProduct(refinementSteps.back().getWeightVector(), refinementSteps.back().getUpperBoundPoint()));
-                
-                // Due to numerical issues, it might be the case that the updated overapproximation does not contain the underapproximation,
-                // e.g., when the new point is strictly contained in the underapproximation. Check if this is the case.
-                RationalNumberType maximumOffset = h.offset();
-                for(auto const& step : refinementSteps){
-                    maximumOffset = std::max(maximumOffset, storm::utility::vector::dotProduct(h.normalVector(), step.getLowerBoundPoint()));
-                }
-                if(maximumOffset > h.offset()){
-                    // We correct the issue by shifting the halfspace such that it contains the underapproximation
-                    h.offset() = maximumOffset;
-                    STORM_LOG_WARN("Numerical issues: The overapproximation would not contain the underapproximation. Hence, a halfspace is shifted by " << storm::utility::convertNumber<double>(h.euclideanDistance(refinementSteps.back().getUpperBoundPoint())) << ".");
-                }
-                overApproximation = overApproximation->intersection(h);
-                STORM_LOG_DEBUG("Updated OverApproximation to " << overApproximation->toString(true));
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::updateUnderApproximation(std::vector<RefinementStep> const& refinementSteps, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& underApproximation) {
-                std::vector<Point> paretoPoints;
-                paretoPoints.reserve(refinementSteps.size());
-                for(auto const& step : refinementSteps) {
-                    paretoPoints.push_back(step.getLowerBoundPoint());
-                }
-                underApproximation = storm::storage::geometry::Polytope<RationalNumberType>::createDownwardClosure(paretoPoints);
-                STORM_LOG_DEBUG("Updated UnderApproximation to " << underApproximation->toString(true));
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::checkIfThresholdsAreSatisfied(std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds) {
-                std::vector<storm::storage::geometry::Halfspace<RationalNumberType>> halfspaces = polytope->getHalfspaces();
-                for(auto const& h : halfspaces) {
-                    RationalNumberType distance = h.distance(thresholds);
-                    if(distance < storm::utility::zero<RationalNumberType>()) {
-                        return false;
-                    }
-                    if(distance == storm::utility::zero<RationalNumberType>()) {
-                        // In this case, the thresholds point is on the boundary of the polytope.
-                        // Check if this is problematic for the strict thresholds
-                        for(auto strictThreshold : strictThresholds) {
-                            if(h.normalVector()[strictThreshold] > storm::utility::zero<RationalNumberType>()) {
-                                return false;
-                            }
-                        }
-                    }
-                }
-                return true;
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::targetPrecisionReached(ResultData& resultData) {
-                resultData.setTargetPrecisionReached(resultData.isPrecisionOfResultSet() &&
-                                                 resultData.getPrecisionOfResult() < storm::utility::convertNumber<RationalNumberType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision()));
-                return resultData.getTargetPrecisionReached();
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::maxStepsPerformed(ResultData& resultData) {
-                resultData.setMaxStepsPerformed(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isMaxStepsSet() &&
-                                            resultData.refinementSteps().size() >= storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getMaxSteps());
-                return resultData.getMaxStepsPerformed();
-            }
-            
-#ifdef STORM_HAVE_CARL
-            template class SparseMultiObjectiveHelper<storm::models::sparse::Mdp<double>, storm::RationalNumber>;
-            template class SparseMultiObjectiveHelper<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>;
-            
-            template class SparseMultiObjectiveHelper<storm::models::sparse::Mdp<storm::RationalNumber>, storm::RationalNumber>;
-            template class SparseMultiObjectiveHelper<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>, storm::RationalNumber>;
-#endif
-        }
-    }
-}

src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h

@@ -1,99 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPER_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPER_H_
-
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h"
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h"
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h"
-#include "src/modelchecker/multiObjective/helper/SparseMultiObjectiveWeightVectorChecker.h"
-#include "src/storage/geometry/Polytope.h"
-#include "src/storage/TotalScheduler.h"
-
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            template <class SparseModelType, typename RationalNumberType>
-            class SparseMultiObjectiveHelper {
-            public:
-                typedef typename SparseModelType::ValueType SparseModelValueType;
-                
-                typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData;
-                typedef SparseMultiObjectiveResultData<RationalNumberType> ResultData;
-                typedef SparseMultiObjectiveRefinementStep<RationalNumberType> RefinementStep;
-                typedef std::shared_ptr<SparseMultiObjectiveWeightVectorChecker<SparseModelType>> WeightVectorCheckerType;
-                
-                typedef std::vector<RationalNumberType> Point;
-                typedef std::vector<RationalNumberType> WeightVector;
-                
-                static ResultData check(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker);
-                
-            private:
-                
-                /*
-                 * Checks whether the preprocessing was already conclusive, e.g., the result for one objective is undefined or false
-                 *
-                 * @return true iff preprocessing was conclusive
-                 */
-                static bool checkIfPreprocessingWasConclusive(PreprocessorData const& preprocessorData);
-                
-                static void achievabilityQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData);
-                static void numericalQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData);
-                static void paretoQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData);
-                
-                /*
-                 * Returns a weight vector w that separates the under approximation from the given point p, i.e.,
-                 * For each x in the under approximation, it holds that w*x <= w*p
-                 *
-                 * @param pointToBeSeparated the point that is to be seperated
-                 * @param underapproximation the current under approximation
-                 * @param objectivesToBeCheckedIndividually stores for each objective whether it still makes sense to check for this objective individually (i.e., with weight vector given by w_{objIndex} = 1 )
-                 */
-                static WeightVector findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked);
-
-                /*
-                 * Refines the current result w.r.t. the given direction vector.
-                 */
-                static void performRefinementStep(WeightVector&& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& resultData);
-                
-                /*
-                 * Updates the overapproximation after a refinement step has been performed
-                 *
-                 * @param refinementSteps the steps performed so far. The last entry should be the newest step, whose information is not yet included in the approximation.
-                 * @param overApproximation the current overApproximation that will be updated
-                 */
-                static void updateOverApproximation(std::vector<RefinementStep> const& refinementSteps, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& overApproximation);
-                
-                /*
-                 * Updates the underapproximation after a refinement step has been performed
-                 *
-                 * @param refinementSteps the steps performed so far. The last entry should be the newest step, whose information is not yet included in the approximation.
-                 * @param underApproximation the current underApproximation that will be updated
-                 */
-                static void updateUnderApproximation(std::vector<RefinementStep> const& refinementSteps, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& underApproximation);
-                
-                /*
-                 * Returns true iff there is a point in the given polytope that satisfies the given thresholds.
-                 * It is assumed that the given polytope contains the downward closure of its vertices.
-                 */
-                static bool checkIfThresholdsAreSatisfied(std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds);
-                
-                /*
-                 * Returns whether the desired precision (as given in the settings) is reached by the current result.
-                 * If the given resultData does not specify a precisionOfResult, false is returned.
-                 * Also sets the resultData.targetPrecisionReached flag accordingly.
-                 */
-                static bool targetPrecisionReached(ResultData& resultData);
-                
-                /*
-                 * Returns whether a maximum number of refinement steps is given in the settings and this threshold has been reached.
-                 * Also sets the resultData.maxStepsPerformed flag accordingly.
-                 */
-                static bool maxStepsPerformed(ResultData& resultData);
-            };
-            
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPER_H_ */

src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h

@@ -1,73 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_
-
-#include <iomanip>
-#include <boost/optional.hpp>
-
-#include "src/logic/Formulas.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            template <typename ValueType>
-            struct SparseMultiObjectiveObjectiveInformation {
-                // the original input formula
-                std::shared_ptr<storm::logic::Formula const> originalFormula;
-                
-                // the name of the considered reward model in the preprocessedModel
-                std::string rewardModelName;
-                
-                // true if all rewards for this objective are positive, false if all rewards are negative.
-                bool rewardsArePositive;
-                
-                // transformation from the values of the preprocessed model to the ones for the actual input model, i.e.,
-                // x is achievable in the preprocessed model iff factor*x + offset is achievable in the original model
-                ValueType toOriginalValueTransformationFactor;
-                ValueType toOriginalValueTransformationOffset;
-                
-                // The probability/reward threshold for the preprocessed model (if originalFormula specifies one).
-                // This is always a lower bound.
-                boost::optional<ValueType> threshold;
-                // True iff the specified threshold is strict, i.e., >
-                bool thresholdIsStrict = false;
-                
-                // The time bound(s) for the formula (if given by the originalFormula)
-                boost::optional<ValueType> lowerTimeBound;
-                boost::optional<ValueType> upperTimeBound;
-                
-                // Stores whether reward finiteness has been checked for this objective.
-                bool rewardFinitenessChecked;
-                
-                void printToStream(std::ostream& out) const {
-                    out << std::setw(30) << originalFormula->toString();
-                    out << " \t(toOrigVal:" << std::setw(3) << toOriginalValueTransformationFactor << "*x +" << std::setw(3) << toOriginalValueTransformationOffset << ", \t";
-                    out << "intern threshold:";
-                    if(threshold){
-                        out << (thresholdIsStrict ? " >" : ">=");
-                        out << std::setw(5) << (*threshold) << ",";
-                    } else {
-                        out << "   none,";
-                    }
-                    out << " \t";
-                    out << "intern reward model: " << std::setw(10) << rewardModelName;
-                    out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t";
-                    out << "time bounds:";
-                    if(lowerTimeBound) {
-                        if(upperTimeBound) {
-                            out << "[" << *lowerTimeBound << ", " <<  *upperTimeBound << "]";
-                        } else {
-                            out << ">=" << std::setw(5) << *lowerTimeBound;
-                        }
-                    } else if (upperTimeBound) {
-                        out << "<=" << std::setw(5) << *upperTimeBound;
-                    } else {
-                        out << " none";
-                    }
-                    out << ")" << std::endl;
-                 }
-            };
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_ */

src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp

@@ -1,363 +0,0 @@
- #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h"
-
-#include <memory>
-
-#include "src/adapters/CarlAdapter.h"
-#include "src/models/sparse/Mdp.h"
-#include "src/models/sparse/MarkovAutomaton.h"
-#include "src/models/sparse/StandardRewardModel.h"
-#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
-#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
-#include "src/modelchecker/results/ParetoCurveCheckResult.h"
-#include "src/storage/geometry/Polytope.h"
-#include "src/storage/geometry/Hyperrectangle.h"
-#include "src/settings//SettingsManager.h"
-#include "src/settings/modules/MultiObjectiveSettings.h"
-#include "src/settings/modules/GeneralSettings.h"
-#include "src/settings/modules/IOSettings.h"
-#include "src/utility/export.h"
-#include "src/utility/macros.h"
-#include "src/utility/vector.h"
-
-#include "src/exceptions/UnexpectedException.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            template<typename SparseModelType, typename RationalNumberType>
-            typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch, boost::optional<storm::utility::Stopwatch> const& helperStopwatch, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch) {
-                STORM_LOG_WARN_COND(!resultData.getMaxStepsPerformed(), "Multi-objective model checking has been aborted since the maximum number of refinement steps has been performed. The results are most likely incorrect.");
-                
-                std::unique_ptr<CheckResult> result(new ExplicitQualitativeCheckResult());;
-                
-                if(preprocessorData.originalFormula.hasQualitativeResult()) {
-                    result = postprocessAchievabilityQuery(preprocessorData, resultData);
-                } else if(preprocessorData.originalFormula.hasNumericalResult()){
-                    result = postprocessNumericalQuery(preprocessorData, resultData);
-                } else if (preprocessorData.originalFormula.hasParetoCurveResult()) {
-                    result = postprocessParetoQuery(preprocessorData, resultData);
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type");
-                }
-                
-                STORM_LOG_INFO(getInfo(result, preprocessorData, resultData, preprocessorStopwatch, helperStopwatch, postprocessorStopwatch));
-                
-                exportPlot(result, preprocessorData, resultData, preprocessorStopwatch, helperStopwatch, postprocessorStopwatch);
-                
-                return result;
-            }
-            
-            template<typename SparseModelType, typename RationalNumberType>
-            typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessAchievabilityQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
-                STORM_LOG_ASSERT(preprocessorData.queryType == PreprocessorData::QueryType::Achievability, "Expected an achievability query.");
-                uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0);
-                
-                //Incorporate the results from prerpocessing
-                for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
-                    switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) {
-                        case PreprocessorData::PreprocessorObjectiveSolution::None:
-                            // Nothing to be done
-                            break;
-                        case PreprocessorData::PreprocessorObjectiveSolution::False:
-                            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
-                        case PreprocessorData::PreprocessorObjectiveSolution::True:
-                            // Nothing to be done
-                            break;
-                        case PreprocessorData::PreprocessorObjectiveSolution::Undefined:
-                            STORM_LOG_ERROR("The result for the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " is not defined.");
-                            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
-                        default:
-                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected type of solution obtained in preprocessing.");
-                    }
-                }
-                
-                if(preprocessorData.objectives.empty()) {
-                    return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, true));
-                }
-                
-                // This might be due to reaching the max. number of refinement steps (so no exception is thrown)
-                STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable.");
-                
-                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, resultData.isThresholdsAreAchievableSet() &&resultData.getThresholdsAreAchievable()));
-            }
-            
-            template<typename SparseModelType, typename RationalNumberType>
-            typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessNumericalQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
-                
-                //The queryType might be achievability (when the numerical result was obtained in preprocessing)
-                STORM_LOG_ASSERT(preprocessorData.queryType == PreprocessorData::QueryType::Numerical ||
-                                 preprocessorData.queryType == PreprocessorData::QueryType::Achievability, "Expected a numerical or an achievability query.");
-                uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0);
-                
-                //Incorporate the results from prerpocessing
-                boost::optional<ValueType> preprocessorNumericalResult;
-                for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
-                    switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) {
-                        case PreprocessorData::PreprocessorObjectiveSolution::None:
-                            // Nothing to be done
-                            break;
-                        case PreprocessorData::PreprocessorObjectiveSolution::False:
-                            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
-                        case PreprocessorData::PreprocessorObjectiveSolution::True:
-                            // Nothing to be done
-                            break;
-                        case PreprocessorData::PreprocessorObjectiveSolution::Numerical:
-                            STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing");
-                            preprocessorNumericalResult = preprocessorData.solutionsFromPreprocessing[subformulaIndex].second;
-                            break;
-                        case PreprocessorData::PreprocessorObjectiveSolution::Unbounded:
-                            STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing");
-                            preprocessorNumericalResult = storm::utility::infinity<ValueType>();
-                            break;
-                        case PreprocessorData::PreprocessorObjectiveSolution::Undefined:
-                            STORM_LOG_ERROR("The result for the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " is not defined.");
-                            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
-                        default:
-                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected solution obtained in preprocessing.");
-                    }
-                }
-                
-                // Check whether the given thresholds are achievable
-                if(preprocessorData.objectives.empty() || (resultData.isThresholdsAreAchievableSet() && resultData.getThresholdsAreAchievable())) {
-                    // Get the numerical result
-                    if(preprocessorNumericalResult) {
-                        STORM_LOG_ASSERT(!resultData.isNumericalResultSet(), "Result was found in preprocessing but there is also one in the resultData");
-                        return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initState, *preprocessorNumericalResult));
-                    } else {
-                        STORM_LOG_ASSERT(resultData.isNumericalResultSet(), "Postprocessing for numerical query invoked, but no numerical result is given");
-                        STORM_LOG_ASSERT(preprocessorData.indexOfOptimizingObjective, "Postprocessing for numerical query invoked, but no index of optimizing objective is specified");
-                        ObjectiveInformation const& optimizingObjective = preprocessorData.objectives[*preprocessorData.indexOfOptimizingObjective];
-                        ValueType resultForOriginalModel = resultData.template getNumericalResult<ValueType>() * optimizingObjective.toOriginalValueTransformationFactor + optimizingObjective.toOriginalValueTransformationOffset;
-                        STORM_LOG_WARN_COND(resultData.getTargetPrecisionReached(), "The target precision for numerical queries has not been reached.");
-                        return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initState, resultForOriginalModel));
-                    }
-                } else {
-                    STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable.");  // This might be due to reaching the max. number of refinement steps (so no exception is thrown)
-                    
-                    return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
-                }
-            }
-            
-            template<typename SparseModelType, typename RationalNumberType>
-            typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessParetoQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
-                uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0);
-                
-                //Issue a warning for objectives that have been solved in preprocessing
-                for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
-                    switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) {
-                        case PreprocessorData::PreprocessorObjectiveSolution::None:
-                            // Nothing to be done
-                            break;
-                        case PreprocessorData::PreprocessorObjectiveSolution::False:
-                            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
-                        case PreprocessorData::PreprocessorObjectiveSolution::True:
-                            // Nothing to be done
-                            break;
-                        case PreprocessorData::PreprocessorObjectiveSolution::Numerical:
-                            STORM_LOG_WARN("The result of the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " was obtained in preprocessing and will not be incorporated in the check result. Objective Result is zero.");
-                            break;
-                        case PreprocessorData::PreprocessorObjectiveSolution::Unbounded:
-                            STORM_LOG_WARN("The result of the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " was obtained in preprocessing and will not be incorporated in the check result. Objective Result is infinity.");
-                            break;
-                        case PreprocessorData::PreprocessorObjectiveSolution::Undefined:
-                            STORM_LOG_ERROR("The result for the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " is not defined.");
-                            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
-                        default:
-                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected solution obtained in preprocessing.");
-                    }
-                }
-                
-                std::vector<std::vector<ValueType>> paretoOptimalPoints;
-                paretoOptimalPoints.reserve(resultData.refinementSteps().size());
-                for(auto const& step : resultData.refinementSteps()) {
-                    paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector<ValueType>(transformToOriginalValues(step.getLowerBoundPoint(), preprocessorData)));
-                }
-                return std::unique_ptr<CheckResult>(new ParetoCurveCheckResult<ValueType>(
-                          initState,
-                          std::move(paretoOptimalPoints),
-                          transformToOriginalValues(resultData.underApproximation(), preprocessorData)->template convertNumberRepresentation<ValueType>(),
-                          transformToOriginalValues(resultData.overApproximation(), preprocessorData)->template convertNumberRepresentation<ValueType>()));
-            }
-            
-            template<typename SparseModelType, typename RationalNumberType>
-            std::vector<RationalNumberType> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::transformToOriginalValues(std::vector<RationalNumberType> const& vector, PreprocessorData const& preprocessorData) {
-                std::vector<RationalNumberType> result;
-                result.reserve(vector.size());
-                for(uint_fast64_t objIndex = 0; objIndex < preprocessorData.objectives.size(); ++objIndex) {
-                    result.push_back(vector[objIndex] * storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[objIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[objIndex].toOriginalValueTransformationOffset));
-                }
-                return result;
-            }
-            
-            template<typename SparseModelType, typename RationalNumberType>
-            std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::transformToOriginalValues(std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& polytope, PreprocessorData const& preprocessorData) {
-                if(polytope->isEmpty()) {
-                    return storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope();
-                }
-                if(polytope->isUniversal()) {
-                    return storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope();
-                }
-                uint_fast64_t numObjectives = preprocessorData.objectives.size();
-                std::vector<std::vector<RationalNumberType>> transformationMatrix(numObjectives, std::vector<RationalNumberType>(numObjectives, storm::utility::zero<RationalNumberType>()));
-                std::vector<RationalNumberType> transformationVector;
-                transformationVector.reserve(numObjectives);
-                for(uint_fast64_t objIndex = 0; objIndex < numObjectives; ++objIndex) {
-                    transformationMatrix[objIndex][objIndex] = storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[objIndex].toOriginalValueTransformationFactor);
-                    transformationVector.push_back(storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[objIndex].toOriginalValueTransformationOffset));
-                }
-                return polytope->affineTransformation(transformationMatrix, transformationVector);
-            }
-            
-            
-            template<typename SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::exportPlot(std::unique_ptr<CheckResult> const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch, boost::optional<storm::utility::Stopwatch> const& helperStopwatch, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch) {
-                
-                if(!settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isExportPlotSet()) {
-                    return;
-                }
-                STORM_LOG_ERROR_COND(preprocessorData.objectives.size()==2, "Exporting plot requested but this is only implemented for the two-dimensional case.");
-                
-                auto transformedUnderApprox = transformToOriginalValues(resultData.underApproximation(), preprocessorData);
-                auto transformedOverApprox = transformToOriginalValues(resultData.overApproximation(), preprocessorData);
-                
-                // Get pareto points as well as a hyperrectangle that is used to guarantee that the resulting polytopes are bounded.
-                storm::storage::geometry::Hyperrectangle<RationalNumberType> boundaries(std::vector<RationalNumber>(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>()), std::vector<RationalNumber>(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>()));
-                std::vector<std::vector<RationalNumberType>> paretoPoints;
-                paretoPoints.reserve(resultData.refinementSteps().size());
-                for(auto const& step : resultData.refinementSteps()) {
-                    paretoPoints.push_back(transformToOriginalValues(step.getLowerBoundPoint(), preprocessorData));
-                    boundaries.enlarge(paretoPoints.back());
-                }
-                auto underApproxVertices = transformedUnderApprox->getVertices();
-                for(auto const& v : underApproxVertices) {
-                    boundaries.enlarge(v);
-                }
-                auto overApproxVertices = transformedOverApprox->getVertices();
-                for(auto const& v : overApproxVertices) {
-                    boundaries.enlarge(v);
-                }
-                
-                //Further enlarge the boundaries a little
-                storm::utility::vector::scaleVectorInPlace(boundaries.lowerBounds(), RationalNumberType(11) / RationalNumberType(10));
-                storm::utility::vector::scaleVectorInPlace(boundaries.upperBounds(), RationalNumberType(11) / RationalNumberType(10));
-                
-                auto boundariesAsPolytope = boundaries.asPolytope();
-                std::vector<std::string> columnHeaders = {"x", "y"};
-                
-                std::vector<std::vector<double>> pointsForPlotting;
-                underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder();
-                pointsForPlotting.reserve(underApproxVertices.size());
-                for(auto const& v : underApproxVertices) {
-                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
-                }
-                storm::utility::exportDataToCSVFile(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotDirectory() + "underapproximation.csv", pointsForPlotting, columnHeaders);
-                                                    
-                pointsForPlotting.clear();
-                overApproxVertices = transformedOverApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder();
-                pointsForPlotting.reserve(overApproxVertices.size());
-                for(auto const& v : overApproxVertices) {
-                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
-                }
-                storm::utility::exportDataToCSVFile(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotDirectory() + "overapproximation.csv", pointsForPlotting, columnHeaders);
-                                                    
-                pointsForPlotting.clear();
-                pointsForPlotting.reserve(paretoPoints.size());
-                for(auto const& v : paretoPoints) {
-                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
-                }
-                storm::utility::exportDataToCSVFile(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotDirectory() + "paretopoints.csv", pointsForPlotting, columnHeaders);
-                                                    
-                pointsForPlotting.clear();
-                auto boundVertices = boundariesAsPolytope->getVerticesInClockwiseOrder();
-                pointsForPlotting.reserve(4);
-                for(auto const& v : boundVertices) {
-                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
-                }
-                storm::utility::exportDataToCSVFile(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotDirectory() + "boundaries.csv", pointsForPlotting, columnHeaders);
-            }
-            
-            template<typename SparseModelType, typename RationalNumberType>
-            std::string SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::getInfo(std::unique_ptr<CheckResult> const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch, boost::optional<storm::utility::Stopwatch> const& helperStopwatch, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch) {
-                
-                std::stringstream statistics;
-                statistics << preprocessorData;
-                statistics << std::endl;
-                statistics << std::endl;
-                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                statistics << "                                                 Multi-objective Model Checking Result                                            " << std::endl;
-                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                statistics << std::endl;
-                statistics << *checkResult;
-                statistics << std::endl;
-                statistics << std::endl;
-                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                statistics << "                                                 Multi-objective Model Checking Statistics                                            " << std::endl;
-                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                statistics << std::endl;
-                statistics << "Recorded Runtimes (in seconds):" << std::endl;
-                storm::utility::Stopwatch combinedTime;
-                combinedTime.pause();
-                if(preprocessorStopwatch) {
-                    statistics << "\t Preprocessing:    " << std::setw(8) << *preprocessorStopwatch << std::endl;
-                    combinedTime.addToAccumulatedSeconds(preprocessorStopwatch->getAccumulatedSeconds());
-                }
-                if(helperStopwatch) {
-                    statistics << "\t       Iterations: " << std::setw(8) << *helperStopwatch << std::endl;
-                    combinedTime.addToAccumulatedSeconds(helperStopwatch->getAccumulatedSeconds());
-                }
-                if(postprocessorStopwatch) {
-                    statistics << "\t Postprocessing:   " << std::setw(8) << *postprocessorStopwatch << std::endl;
-                    combinedTime.addToAccumulatedSeconds(postprocessorStopwatch->getAccumulatedSeconds());
-                }
-                statistics << "\t Combined:         " << std::setw(8) << combinedTime << std::endl;
-                statistics << std::endl;
-                statistics << "Performed Refinement Steps: " << resultData.refinementSteps().size() << (resultData.getMaxStepsPerformed() ? " (computation aborted) " : "" ) << std::endl;
-                statistics << "Precision (Approximation): " << "Goal precision: " << settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision();
-                if(resultData.isPrecisionOfResultSet()) {
-                    statistics << " Achieved precision: " << storm::utility::convertNumber<double>(resultData.getPrecisionOfResult()) << ( resultData.getTargetPrecisionReached() ? "" : " (goal not achieved)");
-                }
-                statistics << std::endl;
-                statistics << "Convergence precision for iterative solvers: " << settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision() << std::endl;
-                statistics << std::endl;
-                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                statistics << "                                                 Data in CSV format                                                                    " << std::endl;
-                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                statistics << "model_Header;Constants;States;Choices;Transitions;Properties;" << std::endl;
-                statistics << "model_data;"
-                                << storm::settings::modules::IOSettings().getConstantDefinitionString() << ";"
-                                << preprocessorData.originalModel.getNumberOfStates() << ";"
-                                << preprocessorData.originalModel.getNumberOfChoices() << ";"
-                                << preprocessorData.originalModel.getNumberOfTransitions() << ";"
-                                << preprocessorData.originalFormula << ";"
-                                << std::endl;
-                statistics << "result_Header;Iterations;Time Combined;Accuracy;Time Iterations;" << std::endl;
-                statistics << "result_data;"
-                                << resultData.refinementSteps().size() << ";"
-                                << combinedTime << ";";
-                if(resultData.isPrecisionOfResultSet()) {
-                                statistics << storm::utility::convertNumber<double>(resultData.getPrecisionOfResult()) << ";";
-                } else {
-                    statistics << ";";
-                }
-                if(helperStopwatch) {
-                    statistics << *helperStopwatch << ";";
-                } else {
-                    statistics << ";";
-                }
-                statistics << std::endl;
-                return statistics.str();
-            }
-            
-            
-#ifdef STORM_HAVE_CARL
-            template class SparseMultiObjectivePostprocessor<storm::models::sparse::Mdp<double>, storm::RationalNumber>;
-            template class SparseMultiObjectivePostprocessor<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>;
-            
-            template class SparseMultiObjectivePostprocessor<storm::models::sparse::Mdp<storm::RationalNumber>, storm::RationalNumber>;
-            template class SparseMultiObjectivePostprocessor<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>, storm::RationalNumber>;
-#endif
-            
-        }
-    }
-}

src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h

@@ -1,55 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_
-
-
-#include <memory>
-#include <boost/optional.hpp>
-
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h"
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h"
-#include "src/modelchecker/results/CheckResult.h"
-#include "src/utility/Stopwatch.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            /*
-             * Helper Class to invoke the necessary preprocessing for multi objective model checking
-             */
-            template <class SparseModelType, typename RationalNumberType>
-            class SparseMultiObjectivePostprocessor {
-            public:
-                typedef typename SparseModelType::ValueType ValueType;
-                typedef typename SparseModelType::RewardModelType RewardModelType;
-                
-                typedef SparseMultiObjectiveObjectiveInformation<ValueType> ObjectiveInformation;
-                typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData;
-                typedef SparseMultiObjectiveResultData<RationalNumberType> ResultData;
-                
-                /*!
-                 * Postprocesses the multi objective model checking result.
-                 *
-                 * @param preprocessorData the data of the preprocessing
-                 * @param resultData the data of the model checking
-                 */
-                static std::unique_ptr<CheckResult> postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch = boost::none, boost::optional<storm::utility::Stopwatch> const& helperStopwatch = boost::none, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch = boost::none);
-                
-            private:
-                static std::unique_ptr<CheckResult> postprocessAchievabilityQuery(PreprocessorData const& preprocessorData, ResultData const& resultData);
-                static std::unique_ptr<CheckResult> postprocessNumericalQuery(PreprocessorData const& preprocessorData, ResultData const& resultData);
-                static std::unique_ptr<CheckResult> postprocessParetoQuery(PreprocessorData const& preprocessorData, ResultData const& resultData);
-                
-                static std::vector<RationalNumberType> transformToOriginalValues(std::vector<RationalNumberType> const& vector, PreprocessorData const& preprocessorData);
-                static std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> transformToOriginalValues(std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& polytope, PreprocessorData const& preprocessorData);
-                
-                static void exportPlot(std::unique_ptr<CheckResult> const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch, boost::optional<storm::utility::Stopwatch> const& helperStopwatch, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch);
-                
-                static std::string getInfo(std::unique_ptr<CheckResult> const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch, boost::optional<storm::utility::Stopwatch> const& helperStopwatch, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch);
-            };
-            
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_ */

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp

@@ -1,546 +0,0 @@
- #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h"
-
-#include "src/models/sparse/Mdp.h"
-#include "src/models/sparse/MarkovAutomaton.h"
-#include "src/models/sparse/StandardRewardModel.h"
-#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
-#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
-#include "src/storage/MaximalEndComponentDecomposition.h"
-#include "src/transformer/StateDuplicator.h"
-#include "src/transformer/SubsystemBuilder.h"
-#include "src/utility/macros.h"
-#include "src/utility/vector.h"
-#include "src/utility/graph.h"
-#include "src/utility/Stopwatch.h"
-
-#include "src/exceptions/InvalidPropertyException.h"
-#include "src/exceptions/UnexpectedException.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            template<typename SparseModelType>
-            typename SparseMultiObjectivePreprocessor<SparseModelType>::PreprocessorData SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) {
-                
-                PreprocessorData data(originalFormula, originalModel, SparseModelType(originalModel), storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates()));
-                
-                //Invoke preprocessing on the individual objectives
-                for(auto const& subFormula : originalFormula.getSubformulas()){
-                    STORM_LOG_DEBUG("Preprocessing objective " << *subFormula<< ".");
-                    data.objectives.emplace_back();
-                    ObjectiveInformation& currentObjective = data.objectives.back();
-                    currentObjective.originalFormula = subFormula;
-                    if(currentObjective.originalFormula->isOperatorFormula()) {
-                        preprocessFormula(currentObjective.originalFormula->asOperatorFormula(), data, currentObjective);
-                    } else {
-                        STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported");
-                    }
-                }
-                
-                //We can now remove all original reward models to save some memory
-                std::set<std::string> origRewardModels = originalFormula.getReferencedRewardModels();
-                for (auto const& rewModel : origRewardModels){
-                    data.preprocessedModel.removeRewardModel(rewModel);
-                }
-                
-                ensureRewardFiniteness(data);
-                handleObjectivesWithSolutionFromPreprocessing(data);
-                
-                // Set the query type. In case of a numerical query, also set the index of the objective to be optimized.
-                // Note: If there are only zero (or one) objectives left, we should not consider a pareto query!
-                storm::storage::BitVector objectivesWithoutThreshold(data.objectives.size());
-                for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
-                    objectivesWithoutThreshold.set(objIndex, !data.objectives[objIndex].threshold);
-                }
-                uint_fast64_t numOfObjectivesWithoutThreshold = objectivesWithoutThreshold.getNumberOfSetBits();
-                if(numOfObjectivesWithoutThreshold == 0) {
-                    data.queryType = PreprocessorData::QueryType::Achievability;
-                } else if (numOfObjectivesWithoutThreshold == 1) {
-                    data.queryType = PreprocessorData::QueryType::Numerical;
-                    data.indexOfOptimizingObjective = objectivesWithoutThreshold.getNextSetIndex(0);
-                } else if (numOfObjectivesWithoutThreshold == data.objectives.size()) {
-                    data.queryType = PreprocessorData::QueryType::Pareto;
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The number of objectives without threshold is not valid. It should be either 0 (achievabilityQuery), 1 (numericalQuery), or " << data.objectives.size() << " (paretoQuery). Got " << numOfObjectivesWithoutThreshold << " instead.");
-                }
-                return data;
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::updatePreprocessedModel(PreprocessorData& data, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping) {
-                data.preprocessedModel = std::move(newPreprocessedModel);
-                // the given newToOldStateIndexMapping reffers to the indices of the former preprocessedModel as 'old indices'
-                for(auto & preprocessedModelStateIndex : newToOldStateIndexMapping){
-                    preprocessedModelStateIndex = data.newToOldStateIndexMapping[preprocessedModelStateIndex];
-                }
-                data.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping);
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
-                
-                // Get a unique name for the new reward model.
-                currentObjective.rewardModelName = "objective" + std::to_string(data.objectives.size());
-                while(data.preprocessedModel.hasRewardModel(currentObjective.rewardModelName)){
-                    currentObjective.rewardModelName = "_" + currentObjective.rewardModelName;
-                }
-                
-                currentObjective.toOriginalValueTransformationFactor = storm::utility::one<ValueType>();
-                currentObjective.toOriginalValueTransformationOffset = storm::utility::zero<ValueType>();
-                currentObjective.rewardsArePositive = true;
-                
-                bool formulaMinimizes = false;
-                if(formula.hasBound()) {
-                    currentObjective.threshold = storm::utility::convertNumber<ValueType>(formula.getBound().threshold);
-                    currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType);
-                    //Note that we minimize for upper bounds since we are looking for the EXISTENCE of a satisfying scheduler
-                    formulaMinimizes = !storm::logic::isLowerBound(formula.getBound().comparisonType);
-                } else if (formula.hasOptimalityType()){
-                    formulaMinimizes = storm::solver::minimize(formula.getOptimalityType());
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize");
-                }
-                if(formulaMinimizes) {
-                    // We negate all the values so we can consider the maximum for this objective
-                    // Thus, all objectives will be maximized.
-                    currentObjective.rewardsArePositive = false;
-                    currentObjective.toOriginalValueTransformationFactor = -storm::utility::one<ValueType>();
-                }
-                
-                if(formula.isProbabilityOperatorFormula()){
-                    preprocessFormula(formula.asProbabilityOperatorFormula(), data, currentObjective);
-                } else if(formula.isRewardOperatorFormula()){
-                    preprocessFormula(formula.asRewardOperatorFormula(), data, currentObjective);
-                } else if(formula.isTimeOperatorFormula()){
-                    preprocessFormula(formula.asTimeOperatorFormula(), data, currentObjective);
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported");
-                }
-                
-                if(currentObjective.threshold) {
-                    currentObjective.threshold = (currentObjective.threshold.get() - currentObjective.toOriginalValueTransformationOffset) / currentObjective.toOriginalValueTransformationFactor;
-                }
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
-                currentObjective.rewardFinitenessChecked = true;
-                bool isProb0Formula = false;
-                bool isProb1Formula = false;
-                if(currentObjective.threshold && !currentObjective.thresholdIsStrict) {
-                    isProb0Formula = !currentObjective.rewardsArePositive && storm::utility::isZero(*currentObjective.threshold);
-                    isProb1Formula = currentObjective.rewardsArePositive && storm::utility::isOne(*currentObjective.threshold);
-                }
-                
-                if(formula.getSubformula().isUntilFormula()){
-                    preprocessFormula(formula.getSubformula().asUntilFormula(), data, currentObjective, isProb0Formula, isProb1Formula);
-                } else if(formula.getSubformula().isBoundedUntilFormula()){
-                    preprocessFormula(formula.getSubformula().asBoundedUntilFormula(), data, currentObjective);
-                } else if(formula.getSubformula().isGloballyFormula()){
-                    preprocessFormula(formula.getSubformula().asGloballyFormula(), data, currentObjective, isProb0Formula, isProb1Formula);
-                } else if(formula.getSubformula().isEventuallyFormula()){
-                    preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, isProb0Formula, isProb1Formula);
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
-                }
-            }
-
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
-                // Check if the reward model is uniquely specified
-                STORM_LOG_THROW((formula.hasRewardModelName() && data.preprocessedModel.hasRewardModel(formula.getRewardModelName()))
-                                || data.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model.");
-                
-                // reward finiteness has to be checked later iff infinite reward is possible for the subformula
-                currentObjective.rewardFinitenessChecked = formula.getSubformula().isCumulativeRewardFormula() || (formula.getSubformula().isEventuallyFormula() && !currentObjective.rewardsArePositive);
-                
-                if(formula.getSubformula().isEventuallyFormula()){
-                    preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, false, false, formula.getOptionalRewardModelName());
-                } else if(formula.getSubformula().isCumulativeRewardFormula()) {
-                    preprocessFormula(formula.getSubformula().asCumulativeRewardFormula(), data, currentObjective, formula.getOptionalRewardModelName());
-                } else if(formula.getSubformula().isTotalRewardFormula()) {
-                    preprocessFormula(formula.getSubformula().asTotalRewardFormula(), data, currentObjective, formula.getOptionalRewardModelName());
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
-                }
-            }
-
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
-                // Time formulas are only supported for Markov automata
-                STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata.");
-                
-                // reward finiteness does not need to be checked if we want to minimize time
-                currentObjective.rewardFinitenessChecked = !currentObjective.rewardsArePositive;
-                
-                if(formula.getSubformula().isEventuallyFormula()){
-                    preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, false, false);
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
-                }
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula) {
-                CheckTask<storm::logic::Formula, ValueType> phiTask(formula.getLeftSubformula());
-                CheckTask<storm::logic::Formula, ValueType> psiTask(formula.getRightSubformula());
-                storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.preprocessedModel);
-                STORM_LOG_THROW(mc.canHandle(phiTask) && mc.canHandle(psiTask), storm::exceptions::InvalidPropertyException, "The subformulas of " << formula << " should be propositional.");
-                storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
-                storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
-                
-                if(!(psiStates & data.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) {
-                    // The probability is always one
-                    data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical;
-                    data.solutionsFromPreprocessing[data.objectives.size()-1].second = currentObjective.rewardsArePositive ? storm::utility::one<ValueType>() : -storm::utility::one<ValueType>();
-                    return;
-                }
-                
-                auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(data.preprocessedModel, ~phiStates | psiStates);
-                updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping);
-                
-                storm::storage::BitVector newPsiStates(data.preprocessedModel.getNumberOfStates(), false);
-                for(auto const& oldPsiState : psiStates){
-                    //note that psiStates are always located in the second copy
-                    newPsiStates.set(duplicatorResult.secondCopyOldToNewStateIndexMapping[oldPsiState], true);
-                }
-                
-                if(isProb0Formula || isProb1Formula) {
-                    storm::storage::BitVector subsystemStates;
-                    storm::storage::BitVector noIncomingTransitionFromFirstCopyStates;
-                    if(isProb0Formula) {
-                        storm::storage::BitVector statesReachableInSecondCopy = storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), duplicatorResult.gateStates & (~newPsiStates), duplicatorResult.secondCopy, storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), false));
-                        subsystemStates = statesReachableInSecondCopy | (duplicatorResult.firstCopy & storm::utility::graph::performProb0E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, newPsiStates));
-                        noIncomingTransitionFromFirstCopyStates = newPsiStates;
-                    } else {
-                        storm::storage::BitVector statesReachableInSecondCopy = storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), newPsiStates, duplicatorResult.secondCopy, storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), false));
-                        data.preprocessedModel.getStateLabeling().setStates(data.prob1StatesLabel, data.preprocessedModel.getStateLabeling().getStates(data.prob1StatesLabel) & statesReachableInSecondCopy);
-                        subsystemStates = statesReachableInSecondCopy | storm::utility::graph::performProb1E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, newPsiStates);
-                        noIncomingTransitionFromFirstCopyStates = duplicatorResult.gateStates & (~newPsiStates);
-                    }
-                    if((subsystemStates & data.preprocessedModel.getInitialStates()).empty()) {
-                        data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::False;
-                    } else {
-                        data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::True;
-                        // Get a subsystem that deletes actions for which the property would be violated
-                        storm::storage::BitVector consideredActions(data.preprocessedModel.getTransitionMatrix().getRowCount(), true);
-                        for(auto state : duplicatorResult.firstCopy) {
-                            for(uint_fast64_t action = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; action < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state +1]; ++action) {
-                                for(auto const& entry : data.preprocessedModel.getTransitionMatrix().getRow(action)) {
-                                    if(noIncomingTransitionFromFirstCopyStates.get(entry.getColumn())) {
-                                        consideredActions.set(action, false);
-                                        break;
-                                    }
-                                }
-                            }
-                        }
-                        if(!subsystemStates.full() || !consideredActions.full()) {
-                            auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, subsystemStates, consideredActions);
-                            updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping);
-                        }
-                    }
-                } else {
-                    // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from the firstCopy to a psiState
-                    std::vector<ValueType> objectiveRewards(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
-                    for (auto const& firstCopyState : duplicatorResult.firstCopy) {
-                        for (uint_fast64_t row = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState]; row < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState + 1]; ++row) {
-                            objectiveRewards[row] = data.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, newPsiStates);
-                        }
-                    }
-                    if(!currentObjective.rewardsArePositive) {
-                        storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one<ValueType>());
-                    }
-                    data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards));
-                }
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
-                
-                if(formula.hasDiscreteTimeBound()) {
-                    currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getDiscreteTimeBound());
-                } else {
-                    if(data.originalModel.isOfType(storm::models::ModelType::Mdp)) {
-                        STORM_LOG_THROW(formula.getIntervalBounds().first == std::round(formula.getIntervalBounds().first), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with discrete lower time bound but got " << formula << ".");
-                        STORM_LOG_THROW(formula.getIntervalBounds().second == std::round(formula.getIntervalBounds().second), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with discrete upper time bound but got " << formula << ".");
-                    } else {
-                        STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula which can not be checked for the current model type.");
-                        STORM_LOG_THROW(formula.getIntervalBounds().second > formula.getIntervalBounds().first, storm::exceptions::InvalidPropertyException, "Neither empty nor point intervalls are allowed but got " << formula << ".");
-                    }
-                    if(!storm::utility::isZero(formula.getIntervalBounds().first)) {
-                        currentObjective.lowerTimeBound = storm::utility::convertNumber<ValueType>(formula.getIntervalBounds().first);
-                    }
-                    currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getIntervalBounds().second);
-                }
-                preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false);
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula) {
-                // The formula will be transformed to an until formula for the complementary event.
-                // If the original formula minimizes, the complementary one will maximize and vice versa.
-                // Hence, the decision whether to consider positive or negative rewards flips.
-                currentObjective.rewardsArePositive = !currentObjective.rewardsArePositive;
-                // To transform from the value of the preprocessed model back to the value of the original model, we have to add 1 to the result.
-                // The transformation factor has already been set correctly.
-                currentObjective.toOriginalValueTransformationOffset = storm::utility::one<ValueType>();
-                
-                auto negatedSubformula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer());
-                
-                // We need to swap the two flags isProb0Formula and isProb1Formula
-                preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), data, currentObjective, isProb1Formula, isProb0Formula);
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective,  bool isProb0Formula, bool isProb1Formula, boost::optional<std::string> const& optionalRewardModelName) {
-                if(formula.isReachabilityProbabilityFormula()){
-                    preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data, currentObjective, isProb0Formula, isProb1Formula);
-                    return;
-                }
-                
-                CheckTask<storm::logic::Formula, ValueType> targetTask(formula.getSubformula());
-                storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.preprocessedModel);
-                STORM_LOG_THROW(mc.canHandle(targetTask), storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " should be propositional.");
-                storm::storage::BitVector targetStates = mc.check(targetTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
-                
-                if(!(targetStates & data.preprocessedModel.getInitialStates()).empty()) {
-                    // The value is always zero
-                    data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical;
-                    data.solutionsFromPreprocessing[data.objectives.size()-1].second = storm::utility::zero<ValueType>();
-                    return;
-                }
-                
-                auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(data.preprocessedModel, targetStates);
-                updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping);
-                
-                // Add a reward model that gives zero reward to the actions of states of the second copy.
-                RewardModelType objectiveRewards(boost::none);
-                if(formula.isReachabilityRewardFormula()) {
-                    objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "");
-                    objectiveRewards.reduceToStateBasedRewards(data.preprocessedModel.getTransitionMatrix(), false);
-                    if(objectiveRewards.hasStateRewards()) {
-                        storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), duplicatorResult.secondCopy, storm::utility::zero<ValueType>());
-                    }
-                    if(objectiveRewards.hasStateActionRewards()) {
-                        for(auto secondCopyState : duplicatorResult.secondCopy) {
-                            std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[secondCopyState], data.preprocessedModel.getTransitionMatrix().getRowGroupSize(secondCopyState), storm::utility::zero<ValueType>());
-                        }
-                    }
-                } else if(formula.isReachabilityTimeFormula() && data.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) {
-                    objectiveRewards = RewardModelType(std::vector<ValueType>(data.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>()));
-                    storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), data.getMarkovianStatesOfPreprocessedModel() & duplicatorResult.firstCopy, storm::utility::one<ValueType>());
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton) ?  "nor reachability time" : "") << ". This is not supported.");
-                }
-                if(!currentObjective.rewardsArePositive){
-                    if(objectiveRewards.hasStateRewards()) {
-                        storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>());
-                    }
-                    if(objectiveRewards.hasStateActionRewards()) {
-                        storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>());
-                    }
-                }
-                data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards));
-                
-                // States of the first copy from which the second copy is not reachable with prob 1 under any scheduler can
-                // be removed as the expected reward/time is not defined for these states.
-                // We also need to enforce that the second copy will be reached eventually with prob 1.
-                data.preprocessedModel.getStateLabeling().setStates(data.prob1StatesLabel, data.preprocessedModel.getStateLabeling().getStates(data.prob1StatesLabel) & duplicatorResult.secondCopy);
-                storm::storage::BitVector subsystemStates =  duplicatorResult.secondCopy | storm::utility::graph::performProb1E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, duplicatorResult.gateStates);
-                if((subsystemStates & data.preprocessedModel.getInitialStates()).empty()) {
-                    data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Undefined;
-                } else if(!subsystemStates.full()) {
-                    auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, subsystemStates, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true));
-                    updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping);
-                }
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
-                STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type.");
-                STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << ".");
-                if(formula.getDiscreteTimeBound()==0) {
-                    data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical;
-                    data.solutionsFromPreprocessing[data.objectives.size()-1].second = storm::utility::zero<ValueType>();
-                    return;
-                }
-                currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getDiscreteTimeBound());
-                
-                RewardModelType objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "");
-                objectiveRewards.reduceToStateBasedRewards(data.preprocessedModel.getTransitionMatrix(), false);
-                if(!currentObjective.rewardsArePositive){
-                    if(objectiveRewards.hasStateRewards()) {
-                        storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>());
-                    }
-                    if(objectiveRewards.hasStateActionRewards()) {
-                        storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>());
-                    }
-                }
-                data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards));
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::TotalRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
-                RewardModelType objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "");
-                objectiveRewards.reduceToStateBasedRewards(data.preprocessedModel.getTransitionMatrix(), false);
-                if(!currentObjective.rewardsArePositive){
-                    if(objectiveRewards.hasStateRewards()) {
-                        storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>());
-                    }
-                    if(objectiveRewards.hasStateActionRewards()) {
-                        storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>());
-                    }
-                }
-                data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards));
-            }
-            
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::ensureRewardFiniteness(PreprocessorData& data) {
-                bool negativeRewardsOccur = false;
-                bool positiveRewardsOccur = false;
-                for(auto& obj : data.objectives) {
-                    if (!obj.rewardFinitenessChecked) {
-                        negativeRewardsOccur |= !obj.rewardsArePositive;
-                        positiveRewardsOccur |= obj.rewardsArePositive;
-                    }
-                }
-                storm::storage::BitVector actionsWithNegativeReward;
-                if(negativeRewardsOccur) {
-                    actionsWithNegativeReward = ensureNegativeRewardFiniteness(data);
-                } else {
-                    actionsWithNegativeReward = storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), false);
-                }
-                if(positiveRewardsOccur) {
-                    ensurePositiveRewardFiniteness(data, actionsWithNegativeReward);
-                }
-            }
-            
-            template<typename SparseModelType>
-            storm::storage::BitVector SparseMultiObjectivePreprocessor<SparseModelType>::ensureNegativeRewardFiniteness(PreprocessorData& data) {
-
-                storm::storage::BitVector actionsWithNonNegativeReward(data.preprocessedModel.getTransitionMatrix().getRowCount(), true);
-                storm::storage::BitVector objectivesWithNegativeReward(data.objectives.size(), false);
-                for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
-                    if (!data.objectives[objIndex].rewardFinitenessChecked && !data.objectives[objIndex].rewardsArePositive) {
-                        data.objectives[objIndex].rewardFinitenessChecked = true;
-                        actionsWithNonNegativeReward &= storm::utility::vector::filterZero(data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getTotalRewardVector(data.preprocessedModel.getTransitionMatrix()));
-                        objectivesWithNegativeReward.set(objIndex, true);
-                    }
-                }
-                
-                storm::storage::BitVector statesWithNegativeRewardForAllChoices(data.preprocessedModel.getNumberOfStates(), false);
-                storm::storage::BitVector submatrixRows = actionsWithNonNegativeReward;
-                for(uint_fast64_t state = 0; state < data.preprocessedModel.getNumberOfStates(); ++state) {
-                    // state has negative reward for all choices iff there is no bit set in actionsWithNonNegativeReward for all actions of state
-                    if(actionsWithNonNegativeReward.getNextSetIndex(data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]) >= data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]) {
-                        statesWithNegativeRewardForAllChoices.set(state, true);
-                        // enable one row for the current state to avoid deleting the row group
-                        submatrixRows.set(data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], true);
-                    }
-                }
-                storm::storage::SparseMatrix<ValueType> transitionsWithNonNegativeReward = data.preprocessedModel.getTransitionMatrix().restrictRows(submatrixRows);
-                
-                storm::storage::BitVector allStates(data.preprocessedModel.getNumberOfStates(), true);
-                storm::storage::BitVector statesNeverReachingNegativeRewardForSomeScheduler = storm::utility::graph::performProb0E(transitionsWithNonNegativeReward, transitionsWithNonNegativeReward.getRowGroupIndices(), transitionsWithNonNegativeReward.transpose(true), allStates, statesWithNegativeRewardForAllChoices);
-                storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), data.preprocessedModel.getBackwardTransitions(), allStates, statesNeverReachingNegativeRewardForSomeScheduler);
-                if((statesReachingNegativeRewardsFinitelyOftenForSomeScheduler & data.preprocessedModel.getInitialStates()).empty()) {
-                    STORM_LOG_WARN("For every scheduler, the induced reward for one or more of the objectives that minimize rewards is infinity.");
-                    for(auto objIndex : objectivesWithNegativeReward) {
-                        if(data.objectives[objIndex].threshold) {
-                            data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::False;
-                        } else {
-                            data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
-                        }
-                    }
-                } else if(!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) {
-                    auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true));
-                    updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping);
-                    return (~actionsWithNonNegativeReward) % subsystemBuilderResult.subsystemActions;
-                }
-                return ~actionsWithNonNegativeReward;
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::ensurePositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward) {
-                storm::utility::Stopwatch sw;
-                auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getBackwardTransitions());
-                STORM_LOG_DEBUG("Maximal end component decomposition for ensuring positive reward finiteness took " << sw << " seconds.");
-                if(mecDecomposition.empty()) {
-                    return;
-                }
-                for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
-                    auto& obj = data.objectives[objIndex];
-                    if (!obj.rewardFinitenessChecked && obj.rewardsArePositive) {
-                        obj.rewardFinitenessChecked = true;
-                        // Find maximal end components that contain a state with positive reward
-                        storm::storage::BitVector actionsWithPositiveRewards = storm::utility::vector::filterGreaterZero(data.preprocessedModel.getRewardModel(obj.rewardModelName).getTotalRewardVector(data.preprocessedModel.getTransitionMatrix()));
-                        for(auto const& mec : mecDecomposition) {
-                            bool ecHasActionWithPositiveReward = false;
-                            for(auto const& stateActionsPair : mec) {
-                                for(auto const& action : stateActionsPair.second) {
-                                    STORM_LOG_THROW(!actionsWithNegativeReward.get(action), storm::exceptions::InvalidPropertyException, "Found an end componet that contains rewards for a maximizing and a minimizing objective. This is not supported");
-                                    // Note: we could also check whether some sub EC exists that does not contain negative rewards.
-                                    ecHasActionWithPositiveReward |= (actionsWithPositiveRewards.get(action));
-                                }
-                            }
-                            if(ecHasActionWithPositiveReward) {
-                                if(obj.threshold) {
-                                    data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::True;
-                                } else {
-                                    data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
-                                }
-                                break;
-                            }
-                        }
-                    }
-                }
-            }
-            
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::handleObjectivesWithSolutionFromPreprocessing(PreprocessorData& data) {
-                // Set solution for objectives for which there are no rewards left
-                for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
-                    if(data.solutionsFromPreprocessing[objIndex].first == PreprocessorData::PreprocessorObjectiveSolution::None &&
-                       data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).isAllZero()) {
-                        data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical;
-                        data.solutionsFromPreprocessing[objIndex].second = storm::utility::zero<ValueType>();
-                    }
-                }
-                
-                // Translate numerical solutions from preprocessing to Truth values (if the objective specifies a threshold) or to values for the original model (otherwise).
-                for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
-                    if(data.solutionsFromPreprocessing[objIndex].first == PreprocessorData::PreprocessorObjectiveSolution::Numerical) {
-                        ValueType& value = data.solutionsFromPreprocessing[objIndex].second;
-                        ObjectiveInformation const& obj = data.objectives[objIndex];
-                        if(obj.threshold) {
-                            if((obj.thresholdIsStrict && value > (*obj.threshold)) || (!obj.thresholdIsStrict && value >= (*obj.threshold))) {
-                                data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::True;
-                            } else {
-                                data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::False;
-                            }
-                        } else {
-                            value = value * obj.toOriginalValueTransformationFactor + obj.toOriginalValueTransformationOffset;
-                        }
-                    }
-                }
-                
-                // Only keep the objectives for which we have no solution yet
-                storm::storage::BitVector objWithNoSolution = storm::utility::vector::filter<std::pair<typename PreprocessorData::PreprocessorObjectiveSolution, ValueType>>(data.solutionsFromPreprocessing, [&] (std::pair<typename PreprocessorData::PreprocessorObjectiveSolution, ValueType> const& value) -> bool { return value.first == PreprocessorData::PreprocessorObjectiveSolution::None; });
-                data.objectives = storm::utility::vector::filterVector(data.objectives, objWithNoSolution);
-            }
-            
-            
-            template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<double>>;
-            template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<double>>;
-            
-#ifdef STORM_HAVE_CARL
-            template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<storm::RationalNumber>>;
-            template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
-#endif
-
-            
-        }
-    }
-}

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h

@@ -1,102 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSOR_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSOR_H_
-
-#include <memory>
-
-#include "src/logic/Formulas.h"
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h"
-#include "src/storage/BitVector.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            /*
-             * Helper Class to invoke the necessary preprocessing for multi objective model checking
-             */
-            template <class SparseModelType>
-            class SparseMultiObjectivePreprocessor {
-            public:
-                typedef typename SparseModelType::ValueType ValueType;
-                typedef typename SparseModelType::RewardModelType RewardModelType;
-                typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData;
-                typedef SparseMultiObjectiveObjectiveInformation<ValueType> ObjectiveInformation;
-                
-                /*!
-                 * Preprocesses the given model w.r.t. the given formulas.
-                 * @param originalModel The considered model
-                 * @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level, i.e., the formula is simple.
-                 */
-                static PreprocessorData preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel);
-                
-            private:
-                
-                /*!
-                 * Updates the preprocessed model stored in the given data to the given model.
-                 * The given newToOldStateIndexMapping should give for each state in the newPreprocessedModel
-                 * the index of the state in the current data.preprocessedModel.
-                 */
-                static void updatePreprocessedModel(PreprocessorData& data, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping);
-                
-                /*!
-                 * Apply the neccessary preprocessing for the given formula.
-                 * @param formula the current (sub)formula
-                 * @param data the information collected so far
-                 * @param isProb0Formula true iff the considered objective is of the form P<=0 [..]
-                 * @param isProb1Formula true iff the considered objective is of the form P>=1 [..]
-                 * @param currentObjective the currently considered objective. The given formula should be a a (sub)formula of this objective
-                 * @param optionalRewardModelName the reward model name that is considered for the formula (if available)
-                 */
-                static void preprocessFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula);
-                static void preprocessFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula);
-                static void preprocessFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula, boost::optional<std::string> const& optionalRewardModelName = boost::none);
-                static void preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none);
-                static void preprocessFormula(storm::logic::TotalRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none);
-                
-                /*!
-                 * Checks whether the occurring reward properties are guaranteed to be finite for all states.
-                 * if not, further preprocessing is applied.
-                 *
-                 * For reward properties that maximize, it is checked whether the reward is unbounded for some scheduler
-                 * (i.e., an EC with (only positive) rewards is reachable).
-                 * If yes, the objective is removed as we can combine any scheduler with the scheduler above
-                 * to obtain arbitrary high values. Note that in case of achievability or numerical queries, this combination might
-                 * (theoretically) violate thresholds by some small epsilon. This is ignored as we are working with numerical methods anyway...
-                 *
-                 * For reward properties that minimize, all states from which only infinite reward is possible are removed.
-                 * Note that this excludes solutions of numerical queries where the minimum is infinity...
-                 */
-                static void ensureRewardFiniteness(PreprocessorData& data);
-                
-                /*!
-                 * Checks reward finiteness for the negative rewards and returns the set of actions in the
-                 * preprocessedModel that give negative rewards for some objective
-                 */
-                static storm::storage::BitVector ensureNegativeRewardFiniteness(PreprocessorData& data);
-                
-                /*!
-                 * Checks reward finiteness for the positive rewards
-                 */
-                static void ensurePositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward);
-                
-                /*!
-                 * Handles the objectives for which a solution has been found in preprocessing, that is:
-                 * * Set the solution for objectives for which no reward is left to zero
-                 * * Translate numerical solutions for objectives with a threshold to either True or False
-                 * * Translate numerical solutions for objectives without a threshold to a value for the original model
-                 * * Only keep the objectives for which there is no solution yet
-                 */
-                static void handleObjectivesWithSolutionFromPreprocessing(PreprocessorData& data);
-                
-            };
-            
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSOR_H_ */

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h

@@ -1,135 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_
-
-#include <vector>
-#include <memory>
-#include <iomanip>
-#include <type_traits>
-#include <boost/optional.hpp>
-
-#include "src/logic/Formulas.h"
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h"
-#include "src/models/sparse/MarkovAutomaton.h"
-#include "src/storage/BitVector.h"
-#include "src/utility/macros.h"
-#include "src/utility/constants.h"
-
-#include "src/exceptions/UnexpectedException.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            template <class SparseModelType>
-            struct SparseMultiObjectivePreprocessorData {
-                
-                enum class QueryType { Achievability, Numerical, Pareto };
-                enum class PreprocessorObjectiveSolution { None, False, True, Numerical, Unbounded, Undefined };
-                
-                storm::logic::MultiObjectiveFormula const& originalFormula;
-                
-                // Stores the result for this objective obtained from preprocessing.
-                // In case of a numerical result, the value is stored in the second entry of the pair. Otherwise, the second entry can be ignored.
-                std::vector<std::pair<PreprocessorObjectiveSolution, typename SparseModelType::ValueType>> solutionsFromPreprocessing;
-                
-                SparseModelType const& originalModel;
-                SparseModelType preprocessedModel;
-                std::vector<uint_fast64_t> newToOldStateIndexMapping;
-                std::string prob1StatesLabel;
-                
-                QueryType queryType;
-                std::vector<SparseMultiObjectiveObjectiveInformation<typename SparseModelType::ValueType>> objectives;
-                boost::optional<uint_fast64_t> indexOfOptimizingObjective;
-                
-                bool produceSchedulers;
-                
-                SparseMultiObjectivePreprocessorData(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, SparseModelType&& preprocessedModel, std::vector<uint_fast64_t>&& newToOldStateIndexMapping) : originalFormula(originalFormula), solutionsFromPreprocessing(originalFormula.getNumberOfSubformulas(), std::make_pair(PreprocessorObjectiveSolution::None, storm::utility::zero<typename SparseModelType::ValueType>())), originalModel(originalModel), preprocessedModel(preprocessedModel), newToOldStateIndexMapping(newToOldStateIndexMapping), produceSchedulers(false) {
-                    
-                    // get a unique name for the labels of states that have to be reached with probability 1 and add the label
-                    this->prob1StatesLabel = "prob1";
-                    while(this->preprocessedModel.hasLabel(this->prob1StatesLabel)) {
-                        this->prob1StatesLabel = "_" + this->prob1StatesLabel;
-                    }
-                    this->preprocessedModel.getStateLabeling().addLabel(this->prob1StatesLabel, storm::storage::BitVector(this->preprocessedModel.getNumberOfStates(), true));
-                }
-                
-                template<typename MT = SparseModelType>
-                typename std::enable_if<std::is_same<MT, storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType>>::value, storm::storage::BitVector const&>::type
-                getMarkovianStatesOfPreprocessedModel() const {
-                    return preprocessedModel.getMarkovianStates();
-                }
-                
-                template<typename MT = SparseModelType>
-                typename std::enable_if<!std::is_same<MT, storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType>>::value, storm::storage::BitVector const&>::type
-                getMarkovianStatesOfPreprocessedModel() const {
-                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Tried to retrieve Markovian states but the considered model is not an MA.");
-                }
-                
-                void printToStream(std::ostream& out) const {
-                    out << std::endl;
-                    out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                    out << "                                                       Multi-objective Preprocessor Data                                               " << std::endl;
-                    out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                    out << std::endl;
-                    out << "Original Formula: " << std::endl;
-                    out << "--------------------------------------------------------------" << std::endl;
-                    out << "\t" << originalFormula << std::endl;
-                    bool hasOneObjectiveSolvedInPreprocessing = false;
-                    for(uint_fast64_t subformulaIndex = 0; subformulaIndex < originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
-                        if(!hasOneObjectiveSolvedInPreprocessing && solutionsFromPreprocessing[subformulaIndex].first != PreprocessorObjectiveSolution::None) {
-                            hasOneObjectiveSolvedInPreprocessing = true;
-                            out << std::endl;
-                            out << "Solutions of objectives obtained from Preprocessing: " << std::endl;
-                            out << "--------------------------------------------------------------" << std::endl;
-                        }
-                        switch(solutionsFromPreprocessing[subformulaIndex].first) {
-                            case PreprocessorObjectiveSolution::None:
-                                break;
-                            case PreprocessorObjectiveSolution::False:
-                                out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= false" << std::endl;
-                                break;
-                            case PreprocessorObjectiveSolution::True:
-                                out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= true" << std::endl;
-                                break;
-                            case PreprocessorObjectiveSolution::Numerical:
-                                out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= " << solutionsFromPreprocessing[subformulaIndex].second << std::endl;
-                                break;
-                            case PreprocessorObjectiveSolution::Unbounded:
-                                out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= unbounded" << std::endl;
-                                break;
-                            case PreprocessorObjectiveSolution::Undefined:
-                                out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= undefined" << std::endl;
-                                break;
-                            default:
-                                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "no case for PreprocessorObjectiveSolution.");
-                        }
-                    }
-                    out << std::endl;
-                    out << "Objectives:" << std::endl;
-                    out << "--------------------------------------------------------------" << std::endl;
-                    for (auto const& obj : objectives) {
-                        obj.printToStream(out);
-                    }
-                    out << "--------------------------------------------------------------" << std::endl;
-                    out << std::endl;
-                    out << "Original Model Information:" << std::endl;
-                    originalModel.printModelInformationToStream(out);
-                    out << std::endl;
-                    out << "Preprocessed Model Information:" << std::endl;
-                    preprocessedModel.printModelInformationToStream(out);
-                    out << std::endl;
-                    out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                }
-           
-                
-                friend std::ostream& operator<<(std::ostream& out, SparseMultiObjectivePreprocessorData<SparseModelType> const& data) {
-                    data.printToStream(out);
-                    return out;
-                }
-                
-            };
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_ */

src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h

@@ -1,63 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEREFINEMENTSTEP_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEREFINEMENTSTEP_H_
-
-#include <vector>
-#include <boost/optional.hpp>
-
-#include "src/storage/TotalScheduler.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            template <typename RationalNumberType>
-            class SparseMultiObjectiveRefinementStep {
-                
-            public:
-                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& lowerBoundPoint, std::vector<RationalNumberType> const& upperBoundPoint, storm::storage::TotalScheduler const& scheduler) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint), scheduler(scheduler) {
-                    //Intentionally left empty
-                }
-                
-                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& lowerBoundPoint, std::vector<RationalNumberType>&& upperBoundPoint, storm::storage::TotalScheduler&& scheduler) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint), scheduler(scheduler) {
-                    //Intentionally left empty
-                }
-                
-                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& lowerBoundPoint, std::vector<RationalNumberType> const& upperBoundPoint) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint) {
-                    //Intentionally left empty
-                }
-                
-                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& lowerBoundPoint, std::vector<RationalNumberType>&& upperBoundPoint) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint) {
-                    //Intentionally left empty
-                }
-                
-                std::vector<RationalNumberType> const& getWeightVector() const {
-                    return weightVector;
-                }
-                
-                std::vector<RationalNumberType> const& getLowerBoundPoint() const {
-                    return lowerBoundPoint;
-                }
-                
-                std::vector<RationalNumberType> const& getUpperBoundPoint() const {
-                    return upperBoundPoint;
-                }
-                
-                bool hasScheduler() const {
-                    return static_cast<bool>(scheduler);
-                }
-                
-                storm::storage::TotalScheduler const& getScheduler() const {
-                    return scheduler.get();
-                }
-                
-            private:
-                std::vector<RationalNumberType> const weightVector;
-                std::vector<RationalNumberType> const lowerBoundPoint;
-                std::vector<RationalNumberType> const upperBoundPoint;
-                boost::optional<storm::storage::TotalScheduler> const scheduler;
-            };
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEREFINEMENTSTEP_H_ */

src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h

@@ -1,135 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVERESULTDATA_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVERESULTDATA_H_
-
-#include <vector>
-#include <memory>
-#include <boost/optional.hpp>
-
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h"
-#include "src/storage/geometry/Polytope.h"
-#include "src/utility/macros.h"
-
-#include "src/exceptions/InvalidStateException.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-
-            template <typename RationalNumberType>
-            class SparseMultiObjectiveResultData {
-                
-            public:
-                std::vector<SparseMultiObjectiveRefinementStep<RationalNumberType>>& refinementSteps() {
-                    return steps;
-                }
-                std::vector<SparseMultiObjectiveRefinementStep<RationalNumberType>> const& refinementSteps() const {
-                    return steps;
-                }
-                
-                std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& overApproximation() {
-                    return overApprox;
-                }
-                std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& overApproximation() const {
-                    return overApprox;
-                }
-                
-                std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& underApproximation() {
-                    return underApprox;
-                }
-                std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& underApproximation() const {
-                    return underApprox;
-                }
-
-                void setThresholdsAreAchievable(bool value) {
-                    thresholdsAreAchievable = value ? Tribool::True : Tribool::False;
-                }
-                bool isThresholdsAreAchievableSet() const {
-                    return thresholdsAreAchievable != Tribool::Indeterminate;
-                }
-                bool getThresholdsAreAchievable() const {
-                    STORM_LOG_THROW(isThresholdsAreAchievableSet(), storm::exceptions::InvalidStateException, "Could not retrieve whether thresholds are acheivable: value not set.");
-                    return thresholdsAreAchievable == Tribool::True;
-                }
-
-                void setNumericalResult(RationalNumberType value) {
-                    numericalResult = value;
-                }
-                bool isNumericalResultSet() const {
-                    return static_cast<bool>(numericalResult);
-                }
-                template<typename TargetValueType = RationalNumberType>
-                TargetValueType getNumericalResult() const {
-                    return storm::utility::convertNumber<TargetValueType>(numericalResult.get());
-                }
-                
-                void setOptimumIsAchievable(bool value) {
-                    optimumIsAchievable = value ? Tribool::True : Tribool::False;
-                }
-                bool isOptimumIsAchievableSet() const {
-                    return optimumIsAchievable != Tribool::Indeterminate;
-                }
-                bool getOptimumIsAchievableAchievable() const {
-                    STORM_LOG_THROW(isOptimumIsAchievableSet(), storm::exceptions::InvalidStateException, "Could not retrieve whether the computed optimum is acheivable: value not set.");
-                    return optimumIsAchievable == Tribool::True;
-                }
-                
-                void setPrecisionOfResult(RationalNumberType value) {
-                    precisionOfResult = value;
-                }
-                bool isPrecisionOfResultSet() const {
-                    return static_cast<bool>(precisionOfResult);
-                }
-                template<typename TargetValueType = RationalNumberType>
-                TargetValueType getPrecisionOfResult() const {
-                    return storm::utility::convertNumber<TargetValueType>(precisionOfResult.get());
-                }
-                
-                void setTargetPrecisionReached(bool value) {
-                    targetPrecisionReached = value;
-                }
-                bool getTargetPrecisionReached() const {
-                    return targetPrecisionReached;
-                }
-                
-                void setMaxStepsPerformed(bool value) {
-                    maxStepsPerformed = value;
-                }
-                bool getMaxStepsPerformed() const {
-                    return maxStepsPerformed;
-                }
-                
-            private:
-                
-                enum class Tribool { False, True, Indeterminate };
-                
-                //Stores the results for the individual iterations
-                std::vector<SparseMultiObjectiveRefinementStep<RationalNumberType>> steps;
-                //Stores an overapproximation of the set of achievable values
-                std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> overApprox;
-                //Stores an underapproximation of the set of achievable values
-                std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> underApprox;
-                
-                // Stores the result of an achievability query (if applicable).
-                // For a numerical query, stores whether there is one feasible solution.
-                Tribool thresholdsAreAchievable = Tribool::Indeterminate;
-                
-                //Stores the result of a numerical query (if applicable).
-                boost::optional<RationalNumberType> numericalResult;
-                //For numerical queries, this is true iff there is an actual scheduler that induces the computed supremum (i.e., supremum == maximum)
-                Tribool optimumIsAchievable = Tribool::Indeterminate;
-                
-                //Stores the achieved precision for numerical and pareto queries
-                boost::optional<RationalNumberType> precisionOfResult;
-                
-                //Stores whether the precision of the result is sufficient (only applicable to numerical and pareto queries)
-                bool targetPrecisionReached = true;
-
-                //Stores whether the computation was aborted due to performing too many refinement steps
-                bool maxStepsPerformed = false;
-
-            };
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVERESULTDATA_H_ */

src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp

@@ -1,242 +0,0 @@
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h"
-
-#include <map>
-
-#include "src/adapters/CarlAdapter.h"
-#include "src/models/sparse/Mdp.h"
-#include "src/models/sparse/MarkovAutomaton.h"
-#include "src/models/sparse/StandardRewardModel.h"
-#include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
-#include "src/solver/MinMaxLinearEquationSolver.h"
-#include "src/transformer/EndComponentEliminator.h"
-#include "src/utility/graph.h"
-#include "src/utility/macros.h"
-#include "src/utility/vector.h"
-
-#include "src/exceptions/IllegalFunctionCallException.h"
-#include "src/exceptions/NotImplementedException.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-
-            template <class SparseModelType>
-            SparseMultiObjectiveWeightVectorChecker<SparseModelType>::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), objectivesWithNoUpperTimeBound(data.objectives.size()), discreteActionRewards(data.objectives.size()), checkHasBeenCalled(false), objectiveResults(data.objectives.size()), offsetsToLowerBound(data.objectives.size()), offsetsToUpperBound(data.objectives.size()) {
-                
-                // set the unbounded objectives
-                for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
-                    objectivesWithNoUpperTimeBound.set(objIndex, !data.objectives[objIndex].upperTimeBound);
-                }
-                // Enlarge the set of prob1 states to the states that are only reachable via prob1 states
-                statesThatAreAllowedToBeVisitedInfinitelyOften = ~storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getInitialStates(), ~data.preprocessedModel.getStates(data.prob1StatesLabel), storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), false));
-            }
-            
-            
-            template <class SparseModelType>
-            void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::check(std::vector<ValueType> const& weightVector) {
-                checkHasBeenCalled=true;
-                STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(weightVector)));
-                std::vector<ValueType> weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
-                for(auto objIndex : objectivesWithNoUpperTimeBound) {
-                    storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]);
-                }
-                unboundedWeightedPhase(weightedRewardVector);
-                unboundedIndividualPhase(weightVector);
-                // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound
-                for(auto const& obj : this->data.objectives) {
-                    if(obj.lowerTimeBound || obj.upperTimeBound) {
-                        boundedPhase(weightVector, weightedRewardVector);
-                        break;
-                    }
-                }
-                STORM_LOG_DEBUG("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(getLowerBoundsOfInitialStateResults())));
-            }
-            
-            template <class SparseModelType>
-            void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::setMaximumLowerUpperBoundGap(ValueType const& value) {
-                this->maximumLowerUpperBoundGap = value;
-            }
-            
-            template <class SparseModelType>
-            typename SparseMultiObjectiveWeightVectorChecker<SparseModelType>::ValueType const& SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getMaximumLowerUpperBoundGap() const {
-                return this->maximumLowerUpperBoundGap;
-            }
-            
-            template <class SparseModelType>
-            std::vector<typename SparseMultiObjectiveWeightVectorChecker<SparseModelType>::ValueType> SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getLowerBoundsOfInitialStateResults() const {
-                STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
-                uint_fast64_t initstate = *this->data.preprocessedModel.getInitialStates().begin();
-                std::vector<ValueType> res;
-                res.reserve(this->data.objectives.size());
-                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
-                    res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToLowerBound[objIndex]);
-                }
-                return res;
-            }
-            
-            template <class SparseModelType>
-            std::vector<typename SparseMultiObjectiveWeightVectorChecker<SparseModelType>::ValueType> SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getUpperBoundsOfInitialStateResults() const {
-                STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
-                uint_fast64_t initstate = *this->data.preprocessedModel.getInitialStates().begin();
-                std::vector<ValueType> res;
-                res.reserve(this->data.objectives.size());
-                for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
-                    res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToUpperBound[objIndex]);
-                }
-                return res;
-            }
-            
-            template <class SparseModelType>
-            storm::storage::TotalScheduler const& SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getScheduler() const {
-                STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
-                for(auto const& obj : this->data.objectives) {
-                    STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives.");
-                }
-                return scheduler;
-            }
-            
-            template <class SparseModelType>
-            void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector) {
-                if(this->objectivesWithNoUpperTimeBound.empty()) {
-                    this->weightedResult = std::vector<ValueType>(data.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>());
-                    this->scheduler = storm::storage::TotalScheduler(data.preprocessedModel.getNumberOfStates());
-                    return;
-                }
-                // Remove end components in which no reward is earned
-                
-                auto ecEliminatorResult = storm::transformer::EndComponentEliminator<ValueType>::transform(data.preprocessedModel.getTransitionMatrix(), storm::utility::vector::filterZero(weightedRewardVector), storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true), storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true));
-                
-                std::vector<ValueType> subRewardVector(ecEliminatorResult.newToOldRowMapping.size());
-                storm::utility::vector::selectVectorValues(subRewardVector, ecEliminatorResult.newToOldRowMapping, weightedRewardVector);
-                std::vector<ValueType> subResult(ecEliminatorResult.matrix.getRowGroupCount());
-                
-                storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> solverFactory;
-                std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(ecEliminatorResult.matrix);
-                solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
-                solver->setTrackScheduler(true);
-                solver->solveEquations(subResult, subRewardVector);
-                
-                this->weightedResult = std::vector<ValueType>(data.preprocessedModel.getNumberOfStates());
-                std::vector<uint_fast64_t> optimalChoices(data.preprocessedModel.getNumberOfStates());
-                
-                transformReducedSolutionToOriginalModel(ecEliminatorResult.matrix, subResult, solver->getScheduler()->getChoices(), ecEliminatorResult.newToOldRowMapping, ecEliminatorResult.oldToNewStateMapping, this->data.preprocessedModel.getTransitionMatrix(), this->weightedResult, optimalChoices);
-                
-                this->scheduler = storm::storage::TotalScheduler(std::move(optimalChoices));
-            }
-            
-            template <class SparseModelType>
-            void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::unboundedIndividualPhase(std::vector<ValueType> const& weightVector) {
-                
-                storm::storage::SparseMatrix<ValueType> deterministicMatrix = data.preprocessedModel.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true);
-                storm::storage::SparseMatrix<ValueType> deterministicBackwardTransitions = deterministicMatrix.transpose();
-                std::vector<ValueType> deterministicStateRewards(deterministicMatrix.getRowCount());
-                storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
-                
-                // We compute an estimate for the results of the individual objectives which is obtained from the weighted result and the result of the objectives computed so far.
-                // Note that weightedResult = Sum_{i=1}^{n} w_i * objectiveResult_i.
-                std::vector<ValueType> weightedSumOfUncheckedObjectives = weightedResult;
-                ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound);
-                
-                for(uint_fast64_t const& objIndex : storm::utility::vector::getSortedIndices(weightVector)) {
-                    if(objectivesWithNoUpperTimeBound.get(objIndex)){
-                        offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>();
-                        offsetsToUpperBound[objIndex] = storm::utility::zero<ValueType>();
-                        storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]);
-                        storm::storage::BitVector statesWithRewards =  ~storm::utility::vector::filterZero(deterministicStateRewards);
-                        // As target states, we pick the states from which no reward is reachable.
-                        storm::storage::BitVector targetStates = ~storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards);
-                        
-                        // Compute the estimate for this objective
-                        if(!storm::utility::isZero(weightVector[objIndex])) {
-                            objectiveResults[objIndex] = weightedSumOfUncheckedObjectives;
-                            storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one<ValueType>() / sumOfWeightsOfUncheckedObjectives);
-                        }
-                        
-                        // Make sure that the objectiveResult is initialized in some way
-                        objectiveResults[objIndex].resize(data.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>());
-                        
-                        // Invoke the linear equation solver
-                        objectiveResults[objIndex] = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeReachabilityRewards(deterministicMatrix,
-                                                                                                                                               deterministicBackwardTransitions,
-                                                                                                                                               deterministicStateRewards,
-                                                                                                                                               targetStates,
-                                                                                                                                               false, //no qualitative checking,
-                                                                                                                                               linearEquationSolverFactory,
-                                                                                                                                               objectiveResults[objIndex]);
-                        // Update the estimate for the next objectives.
-                        if(!storm::utility::isZero(weightVector[objIndex])) {
-                            storm::utility::vector::addScaledVector(weightedSumOfUncheckedObjectives, objectiveResults[objIndex], -weightVector[objIndex]);
-                            sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex];
-                        }
-                    } else {
-                        objectiveResults[objIndex] = std::vector<ValueType>(data.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>());
-                    }
-                }
-            }
-            
-            template <class SparseModelType>
-            void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix<ValueType> const& reducedMatrix,
-                                                         std::vector<ValueType> const& reducedSolution,
-                                                         std::vector<uint_fast64_t> const& reducedOptimalChoices,
-                                                         std::vector<uint_fast64_t> const& reducedToOriginalChoiceMapping,
-                                                         std::vector<uint_fast64_t> const& originalToReducedStateMapping,
-                                                         storm::storage::SparseMatrix<ValueType> const& originalMatrix,
-                                                         std::vector<ValueType>& originalSolution,
-                                                         std::vector<uint_fast64_t>& originalOptimalChoices) const {
-              
-                storm::storage::BitVector statesWithUndefinedScheduler(originalMatrix.getRowGroupCount(), false);
-                for(uint_fast64_t state = 0; state < originalMatrix.getRowGroupCount(); ++state) {
-                    uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state];
-                    // Check if the state exists in the reduced model
-                    if(stateInReducedModel < reducedMatrix.getRowGroupCount()) {
-                        originalSolution[state] = reducedSolution[stateInReducedModel];
-                        // Check if the chosen row originaly belonged to the current state
-                        uint_fast64_t chosenRowInReducedModel = reducedMatrix.getRowGroupIndices()[stateInReducedModel] + reducedOptimalChoices[stateInReducedModel];
-                        uint_fast64_t chosenRowInOriginalModel = reducedToOriginalChoiceMapping[chosenRowInReducedModel];
-                        if(chosenRowInOriginalModel >= originalMatrix.getRowGroupIndices()[state] &&
-                           chosenRowInOriginalModel <  originalMatrix.getRowGroupIndices()[state+1]) {
-                            originalOptimalChoices[state] = chosenRowInOriginalModel - originalMatrix.getRowGroupIndices()[state];
-                        } else {
-                            statesWithUndefinedScheduler.set(state);
-                        }
-                    } else {
-                        // if the state does not exist in the reduced model, it means that the result is always zero, independent of the scheduler.
-                        // Hence, we don't have to set the scheduler explicitly
-                        originalSolution[state] = storm::utility::zero<ValueType>();
-                    }
-                }
-                while(!statesWithUndefinedScheduler.empty()) {
-                    for(auto state : statesWithUndefinedScheduler) {
-                        // Try to find a choice that stays inside the EC (i.e., for which all successors are represented by the same state in the reduced model)
-                        // And at least one successor has a defined scheduler.
-                        // This way, a scheduler is chosen that leads (with probability one) to the state of the EC for which the scheduler is defined
-                        uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state];
-                        for(uint_fast64_t row = originalMatrix.getRowGroupIndices()[state]; row < originalMatrix.getRowGroupIndices()[state+1]; ++row) {
-                            bool rowStaysInEC = true;
-                            bool rowLeadsToDefinedScheduler = false;
-                            for(auto const& entry : originalMatrix.getRow(row)) {
-                                rowStaysInEC &= ( stateInReducedModel == originalToReducedStateMapping[entry.getColumn()]);
-                                rowLeadsToDefinedScheduler |= !statesWithUndefinedScheduler.get(entry.getColumn());
-                            }
-                            if(rowStaysInEC && rowLeadsToDefinedScheduler) {
-                                originalOptimalChoices[state] = row - originalMatrix.getRowGroupIndices()[state];
-                                statesWithUndefinedScheduler.set(state, false);
-                            }
-                        }
-                    }
-                }
-            }
-            
-            
-            
-            template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>;
-            template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>;
-#ifdef STORM_HAVE_CARL
-            template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
-            template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
-#endif
-            
-        }
-    }
-}

src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h

@@ -1,138 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_
-
-#include <vector>
-
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h"
-#include "src/storage/TotalScheduler.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace helper {
-            
-            /*!
-             * Helper Class that takes preprocessed multi objective data and a weight vector and ...
-             * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
-             * - extracts the scheduler that induces this maximum
-             * - computes for each objective the value induced by this scheduler
-             */
-            template <class SparseModelType>
-            class SparseMultiObjectiveWeightVectorChecker {
-            public:
-                typedef typename SparseModelType::ValueType ValueType;
-                typedef typename SparseModelType::RewardModelType RewardModelType;
-                typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData;
-                
-                SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data);
-                
-                /*!
-                 * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
-                 * - extracts the scheduler that induces this maximum
-                 * - computes for each objective the value induced by this scheduler
-                 */
-                void check(std::vector<ValueType> const& weightVector);
-                
-                /*!
-                 * Sets the maximum gap that is allowed between the lower and upper bound of the result of some objective.
-                 */
-                void setMaximumLowerUpperBoundGap(ValueType const& value);
-                
-                /*!
-                 * Retrieves the maximum gap that is allowed between the lower and upper bound of the result of some objective.
-                 */
-                ValueType const& getMaximumLowerUpperBoundGap() const;
-                
-                /*!
-                 * Retrieves the results of the individual objectives at the initial state of the given model.
-                 * Note that check(..) has to be called before retrieving results. Otherwise, an exception is thrown.
-                 * Also note that there is no guarantee that the lower/upper bounds are sound
-                 * as long as the underlying solution methods are unsound (e.g., standard value iteration).
-                 */
-                std::vector<ValueType> getLowerBoundsOfInitialStateResults() const;
-                std::vector<ValueType> getUpperBoundsOfInitialStateResults() const;
-                
-                /*!
-                 * Retrieves a scheduler that induces the current values
-                 * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown.
-                 */
-                storm::storage::TotalScheduler const& getScheduler() const;
-                
-                
-            protected:
-                
-                /*!
-                 * Determines the scheduler that maximizes the weighted reward vector of the unbounded objectives
-                 *
-                 * @param weightedRewardVector the weighted rewards (only considering the unbounded objectives)
-                 */
-                void unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector);
-                
-                /*!
-                 * Computes the values of the objectives that do not have a stepBound w.r.t. the scheduler computed in the unboundedWeightedPhase
-                 *
-                 * @param weightVector the weight vector of the current check
-                 */
-                void unboundedIndividualPhase(std::vector<ValueType> const& weightVector);
-                
-                /*!
-                 * For each time epoch (starting with the maximal stepBound occurring in the objectives), this method
-                 * - determines the objectives that are relevant in the current time epoch
-                 * - determines the maximizing scheduler for the weighted reward vector of these objectives
-                 * - computes the values of these objectives w.r.t. this scheduler
-                 *
-                 * @param weightVector the weight vector of the current check
-                 * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this.
-                 */
-                virtual void boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) = 0;
-                
-                /*!
-                 * Transforms the results of a min-max-solver that considers a reduced model (without end components) to a result for the original (unreduced) model
-                 */
-                void transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix<ValueType> const& reducedMatrix,
-                                                             std::vector<ValueType> const& reducedSolution,
-                                                             std::vector<uint_fast64_t> const& reducedOptimalChoices,
-                                                             std::vector<uint_fast64_t> const& reducedToOriginalChoiceMapping,
-                                                             std::vector<uint_fast64_t> const& originalToReducedStateMapping,
-                                                             storm::storage::SparseMatrix<ValueType> const& originalMatrix,
-                                                             std::vector<ValueType>& originalSolution,
-                                                             std::vector<uint_fast64_t>& originalOptimalChoices) const;
-                
-                
-                // stores the considered information of the multi-objective model checking problem
-                PreprocessorData const& data;
-                // stores the indices of the objectives for which there is no upper time bound
-                storm::storage::BitVector objectivesWithNoUpperTimeBound;
-                // stores the (discretized) state action rewards for each objective.
-                std::vector<std::vector<ValueType>>discreteActionRewards;
-                
-                // stores the set of states for which it is allowed to visit them infinitely often
-                // This means that, if one of the states is part of a neutral EC, it is allowed to
-                // stay in this EC forever.
-                storm::storage::BitVector statesThatAreAllowedToBeVisitedInfinitelyOften;
-                
-                // becomes true after the first call of check(..)
-                bool checkHasBeenCalled;
-                
-                // stores the maximum gap that is allowed between the lower and upper bound of the result of some objective.
-                ValueType maximumLowerUpperBoundGap;
-                
-                // The result for the weighted reward vector (for all states of the model)
-                std::vector<ValueType> weightedResult;
-                // The lower bounds of the results for the individual objectives (w.r.t. all states of the model)
-                std::vector<std::vector<ValueType>> objectiveResults;
-                // Stores for each objective the distance between the computed result (w.r.t. the initial state) and a lower/upper bound for the actual result.
-                // The distances are stored as a (possibly negative) offset that has to be added to to the objectiveResults.
-                // Note that there is no guarantee that the lower/upper bounds are sound as long as the underlying solution method is not sound (e.g. standard value iteration).
-                std::vector<ValueType> offsetsToLowerBound;
-                std::vector<ValueType> offsetsToUpperBound;
-                
-                // The scheduler that maximizes the weighted rewards
-                storm::storage::TotalScheduler scheduler;
-                
-            };
-            
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEWEIGHTEDVECTORCHECKER_H_ */

src/modelchecker/multiobjective/pcaa/SparsePCAAPreprocessor.cpp

@@ -66,10 +66,12 @@ namespace storm {
                 result.actionsWithPositiveReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false);
                 result.actionsWithNegativeReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false);
                 for(uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) {
-                    if(result.objectives[objIndex].rewardsArePositive) {
-                        result.actionsWithPositiveReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix()));
-                    } else {
-                        result.actionsWithNegativeReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix()));
+                    if(!result.objectives[objIndex].upperTimeBound) {
+                        if(result.objectives[objIndex].rewardsArePositive) {
+                            result.actionsWithPositiveReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix()));
+                        } else {
+                            result.actionsWithNegativeReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix()));
+                        }
                     }
                 }
                 
@@ -371,6 +373,8 @@ namespace storm {
                         result.possiblyRecurrentStates |= statesInCurrentECWithNeutralAction;
                     }else{
                         // Check if the ec contains neutral sub ecs. This is done by adding the subECs to our list of ECs
+                        // A neutral subEC only consist of states that can stay in statesInCurrentECWithNeutralAction
+                        statesInCurrentECWithNeutralAction = storm::utility::graph::performProb0E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions,statesInCurrentECWithNeutralAction, ~statesInCurrentECWithNeutralAction);
                         auto subECs = storm::storage::MaximalEndComponentDecomposition<ValueType>(result.preprocessedModel.getTransitionMatrix(), backwardTransitions, statesInCurrentECWithNeutralAction);
                         ecs.reserve(ecs.size() + subECs.size());
                         for(auto& ec : subECs){

src/modelchecker/multiobjective/pcaa/SparsePCAAPreprocessorReturnType.h

@@ -39,9 +39,9 @@ namespace storm {
                 // Maps any state of the preprocessed model to the corresponding state of the original Model
                 std::vector<uint_fast64_t> newToOldStateIndexMapping;
                 
-                // The actions of the preprocessed model that have positive reward assigned for at least one objective
+                // The actions of the preprocessed model that have positive reward assigned for at least one objective (objectives with an upper time-bound are ignored!)
                 storm::storage::BitVector actionsWithPositiveReward;
-                // The actions of the preprocessed model that have negative reward assigned for at least one objective
+                // The actions of the preprocessed model that have negative reward assigned for at least one objective (objectives with an upper time-bound are ignored!)
                 storm::storage::BitVector actionsWithNegativeReward;
                 // The actions of the preprocessed model that are part of an EC
                 storm::storage::BitVector ecActions;

src/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp

@@ -115,7 +115,6 @@ namespace storm {
                     STORM_LOG_THROW(optimizationRes.second, storm::exceptions::UnexpectedException, "The underapproximation is either unbounded or empty.");
                     result = optimizationRes.first[indexOfOptimizingObjective];
                     STORM_LOG_DEBUG("Best solution found so far is ~" << storm::utility::convertNumber<double>(result) << ".");
-                    thresholds[indexOfOptimizingObjective] = result;
                     //Compute an upper bound for the optimum and check for convergence
                     optimizationRes = this->overApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective);
                     if(optimizationRes.second) {
@@ -125,7 +124,10 @@ namespace storm {
                             return result;
                         } else {
                             STORM_LOG_DEBUG("Solution can be improved by at most " << storm::utility::convertNumber<double>(precisionOfResult));
+                            thresholds[indexOfOptimizingObjective] = optimizationRes.first[indexOfOptimizingObjective];
                         }
+                    } else {
+                        thresholds[indexOfOptimizingObjective] = result + storm::utility::one<GeometryValueType>();
                     }
                     WeightVector separatingVector = this->findSeparatingVector(thresholds);
                     this->performRefinementStep(std::move(separatingVector));

src/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp

@@ -7,10 +7,12 @@
 #include "src/modelchecker/multiobjective/pcaa/PcaaObjective.h"
 #include "src/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h"
 #include "src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h"
-#include "src/utility/constants.h"
-#include "src/utility/vector.h"
 #include "src/settings//SettingsManager.h"
 #include "src/settings/modules/MultiObjectiveSettings.h"
+#include "src/storage/geometry/Hyperrectangle.h"
+#include "src/utility/constants.h"
+#include "src/utility/vector.h"
+#include "src/utility/export.h"
 
 #include "src/exceptions/UnexpectedException.h"
 
@@ -44,12 +46,6 @@ namespace storm {
                 this->weightVectorChecker = std::unique_ptr<SparsePcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>>(new SparseMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates));
             }
             
-         //   template<>
-         //   void SparsePcaaQuery<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton<storm::RationalNumber> const& model, std::vector<PcaaObjective<storm::RationalNumber>> const& objectives, storm::storage::BitVector const& actionsWithNegativeReward, storm::storage::BitVector const& ecActions, storm::storage::BitVector const& possiblyRecurrentStates) {
-         //       this->weightVectorChecker = std::unique_ptr<SparsePcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>>(new SparseMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates));
-       //     }
-            
-            
             template <class SparseModelType, typename GeometryValueType>
             typename SparsePcaaQuery<SparseModelType, GeometryValueType>::WeightVector SparsePcaaQuery<SparseModelType, GeometryValueType>::findSeparatingVector(Point const& pointToBeSeparated) {
                 STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(pointToBeSeparated)) << ".");
@@ -193,12 +189,75 @@ namespace storm {
                 return polytope->affineTransformation(transformationMatrix, transformationVector);
             }
             
+            template<typename SparseModelType, typename GeometryValueType>
+            void SparsePcaaQuery<SparseModelType, GeometryValueType>::exportPlotOfCurrentApproximation(std::string const& destinationDir) const {
+               
+                STORM_LOG_ERROR_COND(objectives.size()==2, "Exporting plot requested but this is only implemented for the two-dimensional case.");
+                
+                auto transformedUnderApprox = transformPolytopeToOriginalModel(underApproximation);
+                auto transformedOverApprox = transformPolytopeToOriginalModel(overApproximation);
+                
+                // Get pareto points as well as a hyperrectangle that is used to guarantee that the resulting polytopes are bounded.
+                storm::storage::geometry::Hyperrectangle<GeometryValueType> boundaries(std::vector<GeometryValueType>(objectives.size(), storm::utility::zero<GeometryValueType>()), std::vector<GeometryValueType>(objectives.size(), storm::utility::zero<GeometryValueType>()));
+                std::vector<std::vector<GeometryValueType>> paretoPoints;
+                paretoPoints.reserve(refinementSteps.size());
+                for(auto const& step : refinementSteps) {
+                    paretoPoints.push_back(transformPointToOriginalModel(step.lowerBoundPoint));
+                    boundaries.enlarge(paretoPoints.back());
+                }
+                auto underApproxVertices = transformedUnderApprox->getVertices();
+                for(auto const& v : underApproxVertices) {
+                    boundaries.enlarge(v);
+                }
+                auto overApproxVertices = transformedOverApprox->getVertices();
+                for(auto const& v : overApproxVertices) {
+                    boundaries.enlarge(v);
+                }
+                
+                //Further enlarge the boundaries a little
+                storm::utility::vector::scaleVectorInPlace(boundaries.lowerBounds(), GeometryValueType(15) / GeometryValueType(10));
+                storm::utility::vector::scaleVectorInPlace(boundaries.upperBounds(), GeometryValueType(15) / GeometryValueType(10));
+                
+                auto boundariesAsPolytope = boundaries.asPolytope();
+                std::vector<std::string> columnHeaders = {"x", "y"};
+                
+                std::vector<std::vector<double>> pointsForPlotting;
+                underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder();
+                pointsForPlotting.reserve(underApproxVertices.size());
+                for(auto const& v : underApproxVertices) {
+                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
+                }
+                storm::utility::exportDataToCSVFile(destinationDir + "underapproximation.csv", pointsForPlotting, columnHeaders);
+                
+                pointsForPlotting.clear();
+                overApproxVertices = transformedOverApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder();
+                pointsForPlotting.reserve(overApproxVertices.size());
+                for(auto const& v : overApproxVertices) {
+                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
+                }
+                storm::utility::exportDataToCSVFile(destinationDir + "overapproximation.csv", pointsForPlotting, columnHeaders);
+                
+                pointsForPlotting.clear();
+                pointsForPlotting.reserve(paretoPoints.size());
+                for(auto const& v : paretoPoints) {
+                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
+                }
+                storm::utility::exportDataToCSVFile(destinationDir + "paretopoints.csv", pointsForPlotting, columnHeaders);
+                
+                pointsForPlotting.clear();
+                auto boundVertices = boundariesAsPolytope->getVerticesInClockwiseOrder();
+                pointsForPlotting.reserve(4);
+                for(auto const& v : boundVertices) {
+                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
+                }
+                storm::utility::exportDataToCSVFile(destinationDir + "boundaries.csv", pointsForPlotting, columnHeaders);
+            }
+            
 #ifdef STORM_HAVE_CARL
             template class SparsePcaaQuery<storm::models::sparse::Mdp<double>, storm::RationalNumber>;
             template class SparsePcaaQuery<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>;
             
             template class SparsePcaaQuery<storm::models::sparse::Mdp<storm::RationalNumber>, storm::RationalNumber>;
-        //    template class SparsePcaaQuery<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>, storm::RationalNumber>;
 #endif
         }
     }

src/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h

@@ -27,6 +27,14 @@ namespace storm {
                  */
                 virtual std::unique_ptr<CheckResult> check() = 0;
                 
+                /*
+                 * Exports the current approximations and the currently processed points into respective .csv files located at the given directory.
+                 * The polytopes are represented as the set of vertices. 
+                 * Note that the approximations will be intersected with a  (sufficiently large) hyperrectangle in order to ensure that the polytopes are bounded
+                 * This only works for 2 dimensional queries.
+                 */
+                void exportPlotOfCurrentApproximation(std::string const& destinationDir) const;
+                
             protected:
                 
                 /*

src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -14,6 +14,8 @@
 
 #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
 
+#include "src/modelchecker/multiobjective/pcaa.h"
+
 #include "src/solver/LpSolver.h"
 
 #include "src/settings/modules/GeneralSettings.h"
@@ -41,7 +43,15 @@ namespace storm {
         template<typename SparseMdpModelType>
         bool SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true));
+            if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true))) {
+                return true;
+            } else {
+                // Check whether we consider a multi-objective formula
+                // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states.
+                if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
+                if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
+                return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
+            }
         }
         
         template<typename SparseMdpModelType>
@@ -145,7 +155,12 @@ namespace storm {
             std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(),  subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
 		}
-                
+        
+        template<typename SparseMdpModelType>
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) {
+            return multiobjective::performPcaa(this->getModel(), checkTask.getFormula());
+        }
+        
         template class SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>>;
 
 #ifdef STORM_HAVE_CARL

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -27,6 +27,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
             
         private:
             // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices.

src/utility/export.h

@@ -41,7 +41,7 @@ namespace storm {
         }
         */
             
-        void exportStringToFile(std::string const& str, std::string filepath) {
+        inline void exportStringToFile(std::string const& str, std::string filepath) {
             std::ofstream filestream;
             filestream.open(filepath);
             STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
@@ -49,7 +49,7 @@ namespace storm {
         }
         
         template <typename ValueType>
-        void exportDataToCSVFile(std::string filepath, std::vector<std::vector<ValueType>> const& data, boost::optional<std::vector<std::string>> const& columnHeaders) {
+        inline void exportDataToCSVFile(std::string filepath, std::vector<std::vector<ValueType>> const& data, boost::optional<std::vector<std::string>> const& columnHeaders) {
             std::ofstream filestream;
             filestream.open(filepath);
             STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << ".");

src/utility/storm.h

@@ -71,8 +71,6 @@
 #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
 #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h"
 #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
-#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h"
-#include "src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h"
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 
@@ -306,20 +304,11 @@ namespace storm {
     template<typename ValueType>
     std::unique_ptr<storm::modelchecker::CheckResult> verifySparseMdp(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
         std::unique_ptr<storm::modelchecker::CheckResult> result;
-        if(task.getFormula().isMultiObjectiveFormula()) {
-            storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
-            if (modelchecker.canHandle(task)) {
-                result = modelchecker.check(task);
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported.");
-            }
+        storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
+        if (modelchecker.canHandle(task)) {
+            result = modelchecker.check(task);
         } else {
-            storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
-            if (modelchecker.canHandle(task)) {
-                result = modelchecker.check(task);
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported.");
-            }
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported.");
         }
         return result;
     }
@@ -331,20 +320,11 @@ namespace storm {
         if (!ma->isClosed()) {
             ma->close();
         }
-        if(task.getFormula().isMultiObjectiveFormula()) {
-            storm::modelchecker::SparseMaMultiObjectiveModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
-            if (modelchecker.canHandle(task)) {
-                result = modelchecker.check(task);
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported.");
-            }
+        storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
+        if (modelchecker.canHandle(task)) {
+            result = modelchecker.check(task);
         } else {
-            storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
-            if (modelchecker.canHandle(task)) {
-                result = modelchecker.check(task);
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported.");
-            }
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported.");
         }
         return result;
     }

test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp → test/functional/modelchecker/SparseMaPcaaModelCheckerTest.cpp

@@ -3,7 +3,7 @@
 
 #ifdef STORM_HAVE_HYPRO
 
-#include "src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h"
+#include "src/modelchecker/multiobjective/pcaa.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ParetoCurveCheckResult.h"
@@ -16,7 +16,7 @@
 
 
 /* Rationals for MAs not supported at this point
-TEST(SparseMaMultiObjectiveModelCheckerTest, serverRationalNumbers) {
+TEST(SparseMaPcaaModelCheckerTest, serverRationalNumbers) {
     
     std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/ma/server/server.ma";
     std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto
@@ -29,7 +29,7 @@ TEST(SparseMaMultiObjectiveModelCheckerTest, serverRationalNumbers) {
     storm::generator::NextStateGeneratorOptions options(formulas);
     std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> ma = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build()->as<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>();
     
-    storm::modelchecker::SparseMaMultiObjectiveModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> checker(*ma);
+    storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> checker(*ma);
     
     std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[0], true));
     ASSERT_TRUE(result->isParetoCurveCheckResult());
@@ -47,7 +47,7 @@ TEST(SparseMaMultiObjectiveModelCheckerTest, serverRationalNumbers) {
 }*/
 
 
-TEST(SparseMaMultiObjectiveModelCheckerTest, server) {
+TEST(SparseMaPcaaModelCheckerTest, server) {
     
     std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/ma/server/server.ma";
     std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto
@@ -59,9 +59,9 @@ TEST(SparseMaMultiObjectiveModelCheckerTest, server) {
     program = storm::utility::prism::preprocess(program, "");
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
     std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::MarkovAutomaton<double>>();
-    storm::modelchecker::SparseMaMultiObjectiveModelChecker<storm::models::sparse::MarkovAutomaton<double>> checker(*ma);
+    storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<double>> checker(*ma);
     
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
+    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula());
     ASSERT_TRUE(result->isParetoCurveCheckResult());
     
     std::vector<double> p = {11.0/6.0, 1.0/2.0};

test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp

@@ -1,395 +0,0 @@
-#include "gtest/gtest.h"
-#include "storm-config.h"
-
-#ifdef STORM_HAVE_HYPRO
-
-#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h"
-#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
-#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
-#include "src/models/sparse/Mdp.h"
-#include "src/settings/modules/GeneralSettings.h"
-#include "src/settings/SettingsManager.h"
-#include "src/utility/storm.h"
-
-
-
-TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual1Objective) {
-    
-    std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/multiobjective1.nm";
-    std::string formulasAsString = "multi(Rmax=? [ F s=2 ], P>=1 [ s=0 U s=1 ]) ";
-    formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P>=1 [ F s=1 ]) ";
-    
-    // programm, model,  formula
-    storm::prism::Program program = storm::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, "");
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
-    uint_fast64_t const initState = *mdp->getInitialStates().begin();
-    
-    storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(7.647057, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(7.647057, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-}
-
-TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual0Objective) {
-    
-    std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/multiobjective1.nm";
-    std::string formulasAsString = "multi(Rmax=? [ F s=2 ], P<=0 [ s=0 U s=1 ]) ";
-    formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P<=0 [ F s=1 ]) ";
-    
-    // programm, model,  formula
-    storm::prism::Program program = storm::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, "");
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
-    uint_fast64_t const initState = *mdp->getInitialStates().begin();
-    
-    storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-}
-
-TEST(SparseMdpMultiObjectiveModelCheckerTest, preprocessorResultsTest) {
-    
-    std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/multiobjective2.nm";
-    std::string formulasAsString = "multi(Rmin=? [ F s=2 ], P>=1 [ s!=1 U s=2 ]) ";
-    formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P>=1 [ s!=1 U s=2 ]) ";
-    formulasAsString += "; \n multi(R<=0 [ F s=2 ], P>=1 [ s!=1 U s=2 ]) ";
-    formulasAsString += "; \n multi(R>0 [ F s=2 ], P>=1 [ s!=1 U s=2 ]) ";
-    formulasAsString += "; \n multi(Rmin=? [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) ";
-    formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) ";
-    formulasAsString += "; \n multi(R>=300 [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) ";
-    formulasAsString += "; \n multi(R<10 [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) ";
-    formulasAsString += "; \n multi(Rmin=? [ C ]) ";
-    formulasAsString += "; \n multi(Rmax=? [ C ]) ";
-    formulasAsString += "; \n multi(R>1 [ C ]) ";
-    formulasAsString += "; \n multi(R<1 [ C ]) ";
-    formulasAsString += "; \n multi(Pmax=? [ G true ]) ";
-    formulasAsString += "; \n multi(Pmin=? [ G true ]) ";
-    formulasAsString += "; \n multi(P>0.9 [ G true ]) ";
-    formulasAsString += "; \n multi(P>1 [ G true ]) ";
-    formulasAsString += "; \n multi(Pmax=? [ G false ]) ";
-    formulasAsString += "; \n multi(P>0 [ G false ]) ";
-    formulasAsString += "; \n multi(Pmin=? [ F \"init\" ]) ";
-    formulasAsString += "; \n multi(P>0.5 [ F \"init\" ]) ";
-    
-    // programm, model,  formula
-    storm::prism::Program program = storm::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, "");
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
-    uint_fast64_t const initState = *mdp->getInitialStates().begin();
-    
-    storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[2], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[3], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[4], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(10.0, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[5], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_EQ(storm::utility::infinity<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[6], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[7], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[8], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_EQ(storm::utility::infinity<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[9], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_EQ(storm::utility::infinity<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[10], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[11], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[12], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_EQ(storm::utility::one<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[13], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_EQ(storm::utility::one<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[14], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[15], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[16], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_EQ(storm::utility::zero<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[17], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[18], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_EQ(storm::utility::one<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[19], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    
-}
-
-TEST(SparseMdpMultiObjectiveModelCheckerTest, consensus) {
-    
-    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/consensus/consensus2_3_2.nm";
-    std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical
-    formulasAsString += "; \n multi(P>=0.1 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (true)
-    formulasAsString += "; \n multi(P>=0.11 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (false)
-    
-    // programm, model,  formula
-    storm::prism::Program program = storm::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, "");
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
-    uint_fast64_t const initState = *mdp->getInitialStates().begin();;
-    
-    storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[2], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-}
-
-TEST(SparseMdpMultiObjectiveModelCheckerTest, zeroconf) {
-    
-    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/zeroconf/zeroconf4.nm";
-    std::string formulasAsString = "multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical
-    formulasAsString += "; \n multi(P>=0.0003 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ])"; // achievability (true)
-    formulasAsString += "; \n multi(P>=0.00031 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ])"; // achievability (false)
-    
-    // programm, model,  formula
-    storm::prism::Program program = storm::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, "");
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
-    uint_fast64_t const initState = *mdp->getInitialStates().begin();
-    
-    storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[2], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-}
-
-TEST(SparseMdpMultiObjectiveModelCheckerTest, zeroconfTb) {
-    
-    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/zeroconf-tb/zeroconf-tb2_14.nm";
-    std::string formulasAsString = " multi(Pmax=? [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // numerical
-    formulasAsString += "; \n  multi(P>=0.00000008 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (true)
-    formulasAsString += "; \n  multi(P>=0.000000081 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (false)
-    
-    // programm, model,  formula
-    storm::prism::Program program = storm::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, "");
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
-    uint_fast64_t const initState = *mdp->getInitialStates().begin();
-    
-    storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(8.059348391417451e-8, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[2], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-}
-
-TEST(SparseMdpMultiObjectiveModelCheckerTest, team3with2objectives) {
-    
-    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/team/team2obj_3.nm";
-    std::string formulasAsString = " multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // numerical
-    formulasAsString += "; \n  multi(P>=0.871 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (true)
-    formulasAsString += "; \n  multi(P>=0.872 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (false)
-    
-    // programm, model,  formula
-    storm::prism::Program program = storm::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, "");
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
-    uint_fast64_t const initState = *mdp->getInitialStates().begin();
-    
-    storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(0.8714285710612256, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[2], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-}
-
-TEST(SparseMdpMultiObjectiveModelCheckerTest, team3with3objectives) {
-    
-    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/team/team3obj_3.nm";
-    std::string formulasAsString = "multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ],  P>=0.5 [ F task2_completed ])"; // numerical
-    formulasAsString += "; \n  multi(P>=0.744 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ],  P>=0.5 [ F task2_completed ])"; // achievability (true)
-    formulasAsString += "; \n  multi(P>=0.745 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ],  P>=0.5 [ F task2_completed ])"; // achievability (false)
-    
-    // programm, model,  formula
-    storm::prism::Program program = storm::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, "");
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
-    uint_fast64_t const initState = *mdp->getInitialStates().begin();
-    
-    storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[2], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-}
-
-TEST(SparseMdpMultiObjectiveModelCheckerTest, scheduler) {
-    
-    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/scheduler/scheduler05.nm";
-    std::string formulasAsString = "multi(R{\"time\"}min=?[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [  F \"tasks_complete\" ]) "; // numerical
-    formulasAsString += "; \n  multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [  F \"tasks_complete\" ]) "; // achievability (true)
-    formulasAsString += "; \n  multi(R{\"time\"}<= 11.777 [ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [  F \"tasks_complete\" ]) "; // achievability (false)
-    
-    // programm, model,  formula
-    storm::prism::Program program = storm::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, "");
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
-    uint_fast64_t const initState = *mdp->getInitialStates().begin();
-    
-    storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(11.77777778, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[2], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-}
-
-TEST(SparseMdpMultiObjectiveModelCheckerTest, dpm) {
-    
-    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/dpm/dpm100.nm";
-    std::string formulasAsString = "multi(R{\"power\"}min=? [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // numerical
-    formulasAsString += "; \n  multi(R{\"power\"}<=121.613 [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // achievability (true)
-    formulasAsString += "; \n  multi(R{\"power\"}<=121.612 [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // achievability (false)
-    
-    // programm, model,  formula
-    storm::prism::Program program = storm::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, "");
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
-    uint_fast64_t const initState = *mdp->getInitialStates().begin();
-    
-    storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0], true));
-    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(121.61288420945114, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-    result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[2], true));
-    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
-    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
-    
-}
-
-
-
-
-#endif /* STORM_HAVE_HYPRO */

test/functional/modelchecker/SparseMdpPcaaModelCheckerTest.cpp

@@ -0,0 +1,228 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_HYPRO
+
+#include "src/modelchecker/multiobjective/pcaa.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/models/sparse/Mdp.h"
+#include "src/settings/modules/GeneralSettings.h"
+#include "src/settings/SettingsManager.h"
+#include "src/utility/storm.h"
+
+
+TEST(SparseMdpPcaaModelCheckerTest, consensus) {
+    
+    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/consensus/consensus2_3_2.nm";
+    std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical
+    formulasAsString += "; \n multi(P>=0.1 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (true)
+    formulasAsString += "; \n multi(P>=0.11 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (false)
+    
+    // programm, model,  formula
+    storm::prism::Program program = storm::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, "");
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();;
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+}
+
+TEST(SparseMdpPcaaModelCheckerTest, zeroconf) {
+    
+    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/zeroconf/zeroconf4.nm";
+    std::string formulasAsString = "multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical
+    formulasAsString += "; \n multi(P>=0.0003 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ])"; // achievability (true)
+    formulasAsString += "; \n multi(P>=0.00031 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ])"; // achievability (false)
+    
+    // programm, model,  formula
+    storm::prism::Program program = storm::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, "");
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+}
+
+TEST(SparseMdpPcaaModelCheckerTest, zeroconfTb) {
+    
+    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/zeroconf-tb/zeroconf-tb2_14.nm";
+    std::string formulasAsString = " multi(Pmax=? [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // numerical
+    formulasAsString += "; \n  multi(P>=0.00000008 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (true)
+    formulasAsString += "; \n  multi(P>=0.000000081 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (false)
+    
+    // programm, model,  formula
+    storm::prism::Program program = storm::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, "");
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_NEAR(8.059348391417451e-8, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+}
+
+TEST(SparseMdpPcaaModelCheckerTest, team3with2objectives) {
+    
+    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/team/team2obj_3.nm";
+    std::string formulasAsString = " multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // numerical
+    formulasAsString += "; \n  multi(P>=0.871 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (true)
+    formulasAsString += "; \n  multi(P>=0.872 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (false)
+    
+    // programm, model,  formula
+    storm::prism::Program program = storm::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, "");
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_NEAR(0.8714285710612256, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+}
+
+TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) {
+    
+    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/team/team3obj_3.nm";
+    std::string formulasAsString = "multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ],  P>=0.5 [ F task2_completed ])"; // numerical
+    formulasAsString += "; \n  multi(P>=0.744 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ],  P>=0.5 [ F task2_completed ])"; // achievability (true)
+    formulasAsString += "; \n  multi(P>=0.745 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ],  P>=0.5 [ F task2_completed ])"; // achievability (false)
+    
+    // programm, model,  formula
+    storm::prism::Program program = storm::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, "");
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+}
+
+TEST(SparseMdpPcaaModelCheckerTest, scheduler) {
+    
+    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/scheduler/scheduler05.nm";
+    std::string formulasAsString = "multi(R{\"time\"}min=?[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [  F \"tasks_complete\" ]) "; // numerical
+    formulasAsString += "; \n  multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [  F \"tasks_complete\" ]) "; // achievability (true)
+    formulasAsString += "; \n  multi(R{\"time\"}<= 11.777 [ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [  F \"tasks_complete\" ]) "; // achievability (false)
+    
+    // programm, model,  formula
+    storm::prism::Program program = storm::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, "");
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_NEAR(11.77777778, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+}
+
+TEST(SparseMdpPcaaModelCheckerTest, dpm) {
+    
+    std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/dpm/dpm100.nm";
+    std::string formulasAsString = "multi(R{\"power\"}min=? [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // numerical
+    formulasAsString += "; \n  multi(R{\"power\"}<=121.613 [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // achievability (true)
+    formulasAsString += "; \n  multi(R{\"power\"}<=121.612 [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // achievability (false)
+    
+    // programm, model,  formula
+    storm::prism::Program program = storm::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, "");
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_NEAR(121.61288420945114, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+    result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula());
+    ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+    EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
+    
+}
+
+
+
+
+#endif /* STORM_HAVE_HYPRO */

test/functional/transformer/EndComponentEliminatorTest.cpp

@@ -34,6 +34,9 @@ TEST(NeutralECRemover, SimpleModelTest) {
     storm::storage::SparseMatrix<double> matrix;
     ASSERT_NO_THROW(matrix = builder.build());
     
+    storm::storage::BitVector subsystem(5, true);
+    subsystem.set(2, false);
+    
     storm::storage::BitVector possibleEcRows(12, true);
     possibleEcRows.set(3, false);
     possibleEcRows.set(6, false);
@@ -44,8 +47,7 @@ TEST(NeutralECRemover, SimpleModelTest) {
     storm::storage::BitVector allowEmptyRows(5, true);
     allowEmptyRows.set(1, false);
     allowEmptyRows.set(4, false);
-    storm::storage::BitVector subsystem(5, true);
-    allowEmptyRows.set(2, false);
+    
     
     auto res = storm::transformer::EndComponentEliminator<double>::transform(matrix, subsystem, possibleEcRows, allowEmptyRows);