implemented single objective queries

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp

@@ -183,8 +183,6 @@ namespace storm {
                     preprocessUntilFormula(formula.getSubformula().asUntilFormula(), opInfo, data);
                 } else if (formula.getSubformula().isBoundedUntilFormula()){
                     preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), opInfo, data);
-                } else if (formula.getSubformula().isMultiObjectiveFormula()){
-                    preprocessMultiObjectiveSubformula(formula.getSubformula().asMultiObjectiveFormula(), opInfo, data);
                 } else if (formula.getSubformula().isGloballyFormula()){
                     preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), opInfo, data);
                 } else if (formula.getSubformula().isEventuallyFormula()){
@@ -271,20 +269,11 @@ namespace storm {
                 
             }
             
-            template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessMultiObjectiveSubformula(storm::logic::MultiObjectiveFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) {
-                // Check whether only bounded until formulas are contained
-                for (auto const& f : formula.getSubformulas()) {
-                    STORM_LOG_THROW(f->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "MultiObjective subformulas are only allowed if they all contain bounded until formulas");
-                }
-                data.objectives.back()->formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(formula.asSharedPointer(), opInfo);
-            }
-            
             template<typename SparseModelType>
             void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) {
                 
                 // Check how to handle this query
-                if (formula.getDimension() != 1 || formula.getTimeBoundReference().isRewardBound()) {
+                if (formula.isMultiDimensional() || formula.getTimeBoundReference().isRewardBound()) {
                     data.objectives.back()->formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(formula.asSharedPointer(), opInfo);
                 } else if (!formula.hasLowerBound() || (!formula.isLowerBoundStrict() && storm::utility::isZero(formula.template getLowerBound<storm::RationalNumber>()))) {
                     std::shared_ptr<storm::logic::Formula const> subformula;

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h

@@ -60,7 +60,6 @@ namespace storm {
                 static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
                 static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, std::shared_ptr<storm::logic::Formula const> subformula = nullptr);
                 static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
-                static void preprocessMultiObjectiveSubformula(storm::logic::MultiObjectiveFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
                 static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
                 static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName = boost::none);
                 static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName = boost::none);

src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp

@@ -17,13 +17,37 @@
 #include "storm/exceptions/UnexpectedException.h"
 #include "storm/exceptions/IllegalArgumentException.h"
 #include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/InvalidPropertyException.h"
 
 namespace storm {
     namespace modelchecker {
         namespace multiobjective {
             
             template<typename ValueType, bool SingleObjectiveMode>
-            MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& allowedBottomStates) : model(model), objectives(objectives), possibleECActions(possibleECActions), allowedBottomStates(allowedBottomStates) {
+            MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives) : model(model), objectives(objectives) {
+                initialize();
+            }
+            
+            template<typename ValueType, bool SingleObjectiveMode>
+            MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::shared_ptr<storm::logic::ProbabilityOperatorFormula const> objectiveFormula) : model(model) {
+                
+                STORM_LOG_THROW(objectiveFormula->hasOptimalityType(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+                if (objectiveFormula->getSubformula().isMultiObjectiveFormula()) {
+                    for (auto const& subFormula : objectiveFormula->getSubformula().asMultiObjectiveFormula().getSubformulas()) {
+                        STORM_LOG_THROW(subFormula->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << *subFormula << ".");
+                    }
+                } else {
+                    STORM_LOG_THROW(objectiveFormula->getSubformula().isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << objectiveFormula->getSubformula() << ".");
+                }
+                
+                // Build an objective from the formula.
+                storm::modelchecker::multiobjective::Objective<ValueType> objective;
+                objective.formula = objectiveFormula;
+                objective.originalFormula = objective.formula;
+                objective.considersComplementaryEvent = false;
+                objective.lowerResultBound = storm::utility::zero<ValueType>();
+                objective.upperResultBound = storm::utility::one<ValueType>();
+                objectives.push_back(std::move(objective));
                 
                 initialize();
             }
@@ -46,29 +70,21 @@ namespace storm {
                 for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
                     auto const& formula = *this->objectives[objIndex].formula;
                     if (formula.isProbabilityOperatorFormula()) {
-                        std::vector<std::shared_ptr<storm::logic::Formula const>> subformulas;
-                        if (formula.getSubformula().isBoundedUntilFormula()) {
-                            subformulas.push_back(formula.getSubformula().asSharedPointer());
-                        } else if (formula.getSubformula().isMultiObjectiveFormula()) {
-                            subformulas = formula.getSubformula().asMultiObjectiveFormula().getSubformulas();
-                        } else {
-                            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unexpected type of subformula for formula " << formula);
-                        }
-                        for (auto const& subformula : subformulas) {
-                            auto const& boundedUntilFormula = subformula->asBoundedUntilFormula();
-                            for (uint64_t dim = 0; dim < boundedUntilFormula.getDimension(); ++dim) {
-                                subObjectives.push_back(std::make_pair(boundedUntilFormula.restrictToDimension(dim), objIndex));
+                        STORM_LOG_THROW(formula.getSubformula().isBoundedUntilFormula(), storm::exceptions::NotSupportedException, "Unexpected type of subformula for formula " << formula);
+                        auto const& subformula = formula.getSubformula().asBoundedUntilFormula();
+                        for (uint64_t dim = 0; dim < subformula.getDimension(); ++dim) {
+                            subObjectives.push_back(std::make_pair(subformula.restrictToDimension(dim), objIndex));
                             std::string memLabel = "dim" + std::to_string(subObjectives.size()) + "_maybe";
                             while (model.getStateLabeling().containsLabel(memLabel)) {
                                 memLabel = "_" + memLabel;
                             }
                             memoryLabels.push_back(memLabel);
-                                if (boundedUntilFormula.getTimeBoundReference(dim).isTimeBound() || boundedUntilFormula.getTimeBoundReference(dim).isStepBound()) {
+                            if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) {
                                 dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.getNumberOfChoices(), 1));
                                 scalingFactors.push_back(storm::utility::one<ValueType>());
                             } else {
-                                    STORM_LOG_ASSERT(boundedUntilFormula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound.");
-                                    std::string const& rewardName = boundedUntilFormula.getTimeBoundReference(dim).getRewardName();
+                                STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound.");
+                                std::string const& rewardName = subformula.getTimeBoundReference(dim).getRewardName();
                                 STORM_LOG_THROW(this->model.hasRewardModel(rewardName), storm::exceptions::IllegalArgumentException, "No reward model with name '" << rewardName << "' found.");
                                 auto const& rewardModel = this->model.getRewardModel(rewardName);
                                 STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported as reward bounds.");
@@ -78,8 +94,6 @@ namespace storm {
                                 scalingFactors.push_back(std::move(discretizedRewardsAndFactor.second));
                             }
                         }
-
-                        }
                     } else if (formula.isRewardOperatorFormula() && formula.getSubformula().isCumulativeRewardFormula()) {
                         subObjectives.push_back(std::make_pair(formula.getSubformula().asSharedPointer(), objIndex));
                         dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.getNumberOfChoices(), 1));
@@ -424,8 +438,7 @@ namespace storm {
             storm::storage::BitVector MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::computeProductInStatesForEpochClass(Epoch const& epoch) {
                 storm::storage::SparseMatrix<ValueType> const& productMatrix = memoryProduct.getProduct().getTransitionMatrix();
                 
-                storm::storage::BitVector result(productMatrix.getRowGroupCount(), false);
-                result.set(*memoryProduct.getProduct().getInitialStates().begin(), true);
+                storm::storage::BitVector result = memoryProduct.getProduct().getInitialStates();
                 // Perform DFS
                 storm::storage::BitVector reachableStates = result;
                 std::vector<uint_fast64_t> stack(reachableStates.begin(), reachableStates.end());
@@ -588,9 +601,23 @@ namespace storm {
             
             template<typename ValueType, bool SingleObjectiveMode>
             typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getInitialStateResult(Epoch const& epoch) {
+                STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states.");
+                STORM_LOG_ASSERT(memoryProduct.getProduct().getInitialStates().getNumberOfSetBits() == 1, "The product has multiple initial states.");
                 return getStateSolution(epoch, *memoryProduct.getProduct().getInitialStates().begin());
             }
 
+            template<typename ValueType, bool SingleObjectiveMode>
+            typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex) {
+                STORM_LOG_ASSERT(model.getInitialStates().get(initialStateIndex), "The given model state is not an initial state.");
+                for (uint64_t memState = 0; memState < memoryProduct.getNumberOfMemoryState(); ++memState) {
+                    uint64_t productState = memoryProduct.getProductState(initialStateIndex, memState);
+                    if (memoryProduct.getProduct().getInitialStates().get(productState)) {
+                        return getStateSolution(epoch, productState);
+                    }
+                }
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not find the initial product state corresponding to the given initial model state.");
+                return getStateSolution(epoch, -1ull);
+            }
             
             template<typename ValueType, bool SingleObjectiveMode>
             storm::storage::MemoryStructure MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::computeMemoryStructure() const {
@@ -854,15 +881,23 @@ namespace storm {
 
             template<typename ValueType, bool SingleObjectiveMode>
             storm::storage::BitVector const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MemoryProduct::convertMemoryState(uint64_t const& memoryState) const {
+                STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to convert a memory state, but the memoryStateMap is not yet initialized.");
                 return memoryStateMap[memoryState];
             }
             
             template<typename ValueType, bool SingleObjectiveMode>
             uint64_t MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MemoryProduct::convertMemoryState(storm::storage::BitVector const& memoryState) const {
+                STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to convert a memory state, but the memoryStateMap is not yet initialized.");
                 auto memStateIt = std::find(memoryStateMap.begin(), memoryStateMap.end(), memoryState);
                 return memStateIt - memoryStateMap.begin();
             }
             
+            template<typename ValueType, bool SingleObjectiveMode>
+            uint64_t MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MemoryProduct::getNumberOfMemoryState() const {
+                STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to retrieve the number of memory states but the memoryStateMap is not yet initialized.");
+                return memoryStateMap.size();
+            }
+            
             template<typename ValueType, bool SingleObjectiveMode>
             uint64_t MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MemoryProduct::getProductStateFromChoice(uint64_t const& productChoice) const {
                 return choiceToStateMap[productChoice];

src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h

@@ -5,12 +5,12 @@
 #include "storm/storage/BitVector.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/modelchecker/multiobjective/Objective.h"
+#include "storm/modelchecker/CheckTask.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/utility/vector.h"
 #include "storm/storage/memorystructure/MemoryStructure.h"
 #include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
 #include "storm/transformer/EndComponentEliminator.h"
-
 #include "storm/utility/Stopwatch.h"
 
 namespace storm {
@@ -40,14 +40,10 @@ namespace storm {
                  *
                  * @param model The (preprocessed) model
                  * @param objectives The (preprocessed) objectives
-                 * @param possibleECActions Overapproximation of the actions that are part of an EC
-                 * @param allowedBottomStates The states which are allowed to become a bottom state under a considered scheduler
                  *
                  */
-                MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model,
-                                                        std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives,
-                                                        storm::storage::BitVector const& possibleECActions,
-                                                        storm::storage::BitVector const& allowedBottomStates);
+                MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives);
+                MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::shared_ptr<storm::logic::ProbabilityOperatorFormula const> objectiveFormula);
                 
                 ~MultiDimensionalRewardUnfolding() {
                     std::cout << "Unfolding statistics: " << std::endl;
@@ -78,7 +74,8 @@ namespace storm {
                 EpochModel& setCurrentEpoch(Epoch const& epoch);
                 
                 void setSolutionForCurrentEpoch(std::vector<SolutionType>& inStateSolutions);
-                SolutionType const& getInitialStateResult(Epoch const& epoch);
+                SolutionType const& getInitialStateResult(Epoch const& epoch); // Assumes that the initial state is unique
+                SolutionType const& getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex);
                 
                 
             private:
@@ -99,6 +96,8 @@ namespace storm {
                     uint64_t convertMemoryState(storm::storage::BitVector const& memoryState) const;
                     storm::storage::BitVector const& convertMemoryState(uint64_t const& memoryState) const;
                     
+                    uint64_t getNumberOfMemoryState() const;
+                    
                     uint64_t getProductStateFromChoice(uint64_t const& productChoice) const;
                 
                 private:
@@ -162,9 +161,7 @@ namespace storm {
                 SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState);
                 
                 storm::models::sparse::Mdp<ValueType> const& model;
-                std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives;
-                storm::storage::BitVector possibleECActions;
-                storm::storage::BitVector allowedBottomStates;
+                std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> objectives;
                 
                 MemoryProduct memoryProduct;
                 

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -43,14 +43,14 @@ namespace storm {
         template<typename SparseMdpModelType>
         bool SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true))) {
+            if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(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 formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true));
+                return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true));
             }
         }
         
@@ -58,15 +58,28 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
             storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            if (pathFormula.isMultiDimensional() || pathFormula.getTimeBoundReference().isRewardBound()) {
+                STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model.");
+                STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking non-trivial bounded until formulas is not optimized w.r.t. qualitative queries");
+                storm::logic::OperatorInformation opInfo(checkTask.getOptimizationDirection());
+                if (checkTask.isBoundSet()) {
+                    opInfo.bound = checkTask.getBound();
+                }
+                auto formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(checkTask.getFormula().asSharedPointer(), opInfo);
+                storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
+                auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNonTrivialBoundedUntilProbabilities(checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory);
+                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            } else {
                 STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
                 STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
                 std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
                 std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
                 ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
                 ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *minMaxLinearEquationSolverFactory, checkTask.getHint());
+                std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeStepBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), *minMaxLinearEquationSolverFactory, checkTask.getHint());
                 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             }
+        }
         
         template<typename SparseMdpModelType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) {

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

@@ -35,7 +35,7 @@ namespace storm {
         namespace helper {
 
             template<typename ValueType>
-            std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
+            std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeStepBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
                 std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
                 
                 // Determine the states that have 0 probability of reaching the target states.
@@ -71,6 +71,56 @@ namespace storm {
                 return result;
             }
 
+            template<typename ValueType>
+            std::map<storm::storage::sparse::state_type, ValueType> SparseMdpPrctlHelper<ValueType>::computeNonTrivialBoundedUntilProbabilities(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+                auto initEpoch = rewardUnfolding.getStartEpoch();
+                auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch);
+                
+                // initialize data that will be needed for each epoch
+                std::vector<ValueType> x, b, epochResult;
+                std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver;
+                for (auto const& epoch : epochOrder) {
+                    // Update some data for the case that the Matrix has changed
+                    auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch);
+                    if (epochModel.epochMatrixChanged) {
+                        x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                        minMaxSolver = minMaxLinearEquationSolverFactory.create(epochModel.epochMatrix);
+                        minMaxSolver->setOptimizationDirection(dir);
+                        minMaxSolver->setCachingEnabled(true);
+                        minMaxSolver->setLowerBound(storm::utility::zero<ValueType>());
+                        minMaxSolver->setUpperBound(storm::utility::one<ValueType>());
+                    }
+                    
+                    // Prepare the right hand side of the equation system
+                    b.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero<ValueType>());
+                    std::vector<ValueType> const& objectiveValues = epochModel.objectiveRewards.front();
+                    for (auto const& choice : epochModel.objectiveRewardFilter.front()) {
+                        b[choice] = objectiveValues[choice];
+                    }
+                    auto stepSolutionIt = epochModel.stepSolutions.begin();
+                    for (auto const& choice : epochModel.stepChoices) {
+                        b[choice] += *stepSolutionIt;
+                        ++stepSolutionIt;
+                    }
+                    assert(stepSolutionIt == epochModel.stepSolutions.end());
+                    
+                    // Solve the minMax equation system
+                    minMaxSolver->solveEquations(x, b);
+                    
+                    // Plug in the result into the reward unfolding
+                    epochResult.resize(epochModel.epochInStates.getNumberOfSetBits());
+                    storm::utility::vector::selectVectorValues(epochResult, epochModel.epochInStates, x);
+                    rewardUnfolding.setSolutionForCurrentEpoch(epochResult);
+                }
+                
+                std::map<storm::storage::sparse::state_type, ValueType> result;
+                for (auto const& initState : initialStates) {
+                    result[initState] = rewardUnfolding.getInitialStateResult(initEpoch, initState);
+                }
+                
+                return  result;
+            }
+
             template<typename ValueType>
             std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
 

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h

@@ -6,6 +6,7 @@
 #include "storm/modelchecker/hints/ModelCheckerHint.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/MaximalEndComponent.h"
+#include "storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h"
 #include "MDPModelCheckingHelperReturnType.h"
 
 #include "storm/utility/solver.h"
@@ -33,7 +34,9 @@ namespace storm {
             template <typename ValueType>
             class SparseMdpPrctlHelper {
             public:
-                static std::vector<ValueType> computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
+                static std::vector<ValueType> computeStepBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
+                
+                static std::map<storm::storage::sparse::state_type, ValueType> computeNonTrivialBoundedUntilProbabilities(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
                 
                 static std::vector<ValueType> computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
 

src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp

@@ -11,6 +11,184 @@
 #include "storm/utility/constants.h"
 #include "storm/api/storm.h"
 
+TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_small) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
+    std::string constantsDef = "N=2";
+    std::string formulasAsString = "Pmax=? [ F{\"r\"}<=1 x=N ] ";
+    formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )]";
+    formulasAsString += "; \n Pmin=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )]";
+
+    // programm, model,  formula
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsDef);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();;
+    std::unique_ptr<storm::modelchecker::CheckResult> result;
+    
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.5), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.125), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+}
+
+TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_large) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
+    std::string constantsDef = "N=10";
+    std::string formulasAsString = "Pmax=? [ F{\"r\"}<=5 x=N ] ";
+    formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}<=5 x=N, F{\"l\"}<=10 x=0 )]";
+
+    // programm, model,  formula
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsDef);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();;
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result;
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
+  
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    storm::RationalNumber expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 5);
+    EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 15);
+    EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+    
+}
+
+
+TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_tiny_ec) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_reward_bounded.nm";
+    std::string constantsDef = "";
+    std::string formulasAsString = "Pmax=? [ F{\"a\"}<=3 x=4 ] "; // 0.2
+    formulasAsString += "; \n Pmin=? [ F{\"a\"}<=3 x=4 ] "; // 0.0
+    formulasAsString += "; \n Pmin=? [ F{\"a\"}<1 x=1 ] "; // 0.0
+    formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )] "; // 0.02
+    formulasAsString += "; \n Pmin=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )] "; // 0.0
+    formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<13 x=5, F{\"c\"}<2/5 x=3 )] "; // 0.02
+    formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=0 x=3, F{\"b\"}<=17 x=4, F{\"c\"}<4/5 x=5 )] "; // 0.02
+
+    // programm, model,  formula
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsDef);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();;
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result;
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
+
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/5");
+    EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
+    EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
+    EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+    
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
+    EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+    
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[4], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
+    EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+    
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[5], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
+    EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+    
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[6], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
+    EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+    
+}
+
+TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_zeroconf_dl) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf_dl_not_unfolded.nm";
+    std::string constantsDef = "N=1000,K=2,reset=true";
+    std::string formulasAsString = "Pmin=? [ F{\"t\"}<50 \"ipfound\" ]";
+    formulasAsString += "; \n Pmax=? [multi(F{\"t\"}<50 \"ipfound\", F{\"r\"}<=0 \"ipfound\")  ]";
+
+    // programm, model,  formula
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsDef);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();;
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result;
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp);
+
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<double>(formulas[0], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_NEAR(0.9989804701, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<double>(formulas[1], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_NEAR(0.984621063, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+
+}
+
+TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_csma) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm";
+    std::string constantsDef = "";
+    std::string formulasAsString = "Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ]";
+
+    // programm, model,  formula
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsDef);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
+    uint_fast64_t const initState = *mdp->getInitialStates().begin();;
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result;
+    
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
+    
+    result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("29487882838281/35184372088832");
+    EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+
+}
+
+
+
+
 #if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE
 
 TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) {