improvements for preprocessing regarding finite/infinite rewards

Former-commit-id: a57e979bdd

src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h

@@ -34,6 +34,9 @@ namespace storm {
                 // The (discrete) stepBound for the formula (if given by the originalFormula)
                 boost::optional<uint_fast64_t> stepBound;
                 
+                // 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";

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp

@@ -4,6 +4,7 @@
 #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"
@@ -18,10 +19,16 @@ namespace storm {
         namespace helper {
             
             template<typename SparseModelType>
-            typename SparseMultiObjectivePreprocessor<SparseModelType>::PreprocessorData SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, storm::storage::BitVector const& subsystem) {
+            typename SparseMultiObjectivePreprocessor<SparseModelType>::PreprocessorData SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) {
                 
-                auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(originalModel, subsystem);
-                PreprocessorData data(originalModel, std::move(*subsystemBuilderResult.model), std::move(subsystemBuilderResult.newToOldStateIndexMapping));
+                PreprocessorData data(originalFormula, originalModel, SparseModelType(originalModel), storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates()));
+                data.objectivesSolvedInPreprocessing = storm::storage::BitVector(originalFormula.getNumberOfSubformulas(), false);
+                // get a unique name for the labels of states that have to be reached with probability 1 and add the label
+                data.prob1StatesLabel = "prob1";
+                while(data.preprocessedModel.hasLabel(data.prob1StatesLabel)) {
+                    data.prob1StatesLabel = "_" + data.prob1StatesLabel;
+                }
+                data.preprocessedModel.getStateLabeling().addLabel(data.prob1StatesLabel);
                 
                 //Invoke preprocessing on the individual objectives
                 for(auto const& subFormula : originalFormula.getSubFormulas()){
@@ -42,6 +49,10 @@ namespace storm {
                     data.preprocessedModel.removeRewardModel(rewModel);
                 }
                 
+                assertRewardFiniteness(data);
+                
+                data.objectives = storm::utility::vector::filterVector(data.objectives, ~data.objectivesSolvedInPreprocessing);
+                
                 //Set the query type. In case of a numerical query, also set the index of the objective to be optimized.
                 storm::storage::BitVector objectivesWithoutThreshold(data.objectives.size());
                 for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
@@ -107,14 +118,22 @@ namespace storm {
             
             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);
+                    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);
+                    preprocessFormula(formula.getSubformula().asGloballyFormula(), data, currentObjective, isProb0Formula, isProb1Formula);
                 } else if(formula.getSubformula().isEventuallyFormula()){
-                    preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective);
+                    preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, isProb0Formula, isProb1Formula);
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
                 }
@@ -125,8 +144,12 @@ namespace storm {
                 // 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();
+                
                 if(formula.getSubformula().isEventuallyFormula()){
-                    preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, formula.getOptionalRewardModelName());
+                    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()) {
@@ -137,7 +160,7 @@ namespace storm {
             }
             
             template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula) {
                 CheckTask<storm::logic::Formula> phiTask(formula.getLeftSubformula());
                 CheckTask<storm::logic::Formula> psiTask(formula.getRightSubformula());
                 storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.preprocessedModel);
@@ -146,20 +169,46 @@ namespace storm {
                 storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
                 
                 auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(data.preprocessedModel, ~phiStates | psiStates);
-                data.preprocessedModel = std::move(*duplicatorResult.model);
-                // duplicatorResult.newToOldStateIndexMapping now reffers to the indices of the model we had before preprocessing this formula.
-                // This might not be the actual original model.
-                for(auto & originalModelStateIndex : duplicatorResult.newToOldStateIndexMapping){
-                    originalModelStateIndex = data.newToOldStateIndexMapping[originalModelStateIndex];
-                }
-                data.newToOldStateIndexMapping = std::move(duplicatorResult.newToOldStateIndexMapping);
+                updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping);
                 
-                // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from the firstCopy to a psiState
                 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) {
+                        subsystemStates = storm::utility::graph::performProb0E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, newPsiStates);
+                        subsystemStates |= duplicatorResult.secondCopy;
+                        noIncomingTransitionFromFirstCopyStates = newPsiStates;
+                    } else {
+                        for(auto psiState : newPsiStates) {
+                            data.preprocessedModel.getStateLabeling().addLabelToState(data.prob1StatesLabel, psiState);
+                        }
+                        subsystemStates = storm::utility::graph::performProb1E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, newPsiStates);
+                        subsystemStates |= duplicatorResult.secondCopy;
+                        noIncomingTransitionFromFirstCopyStates = duplicatorResult.secondCopy & (~newPsiStates);
+                    }
+                    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;
+                                }
+                            }
+                        }
+                    }
+                    subsystemStates = storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getInitialStates(), subsystemStates, storm::storage::BitVector(subsystemStates.size(), false));
+                    auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, subsystemStates, consideredActions);
+                    updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping);
+                    data.objectivesSolvedInPreprocessing.set(data.objectives.size());
+                } 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) {
@@ -171,35 +220,32 @@ namespace storm {
                     }
                     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) {
                 STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with a discrete time bound but got " << formula << ".");
                 currentObjective.stepBound = formula.getDiscreteTimeBound();
-                    preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective);
+                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) {
+            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
+                // The transformation factor has already been set correctly.
                 currentObjective.toOriginalValueTransformationOffset = storm::utility::one<ValueType>();
-                if(currentObjective.threshold) {
-                    // Strict thresholds become non-strict and vice versa
-                    currentObjective.thresholdIsStrict = !currentObjective.thresholdIsStrict;
-                }
                 auto negatedSubformula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer());
-                preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), data, currentObjective);
+                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, boost::optional<std::string> const& optionalRewardModelName) {
+            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);
+                    preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data, currentObjective, isProb0Formula, isProb1Formula);
                     return;
                 }
                 STORM_LOG_THROW(formula.isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability Probabilities nor reachability rewards");
@@ -208,16 +254,21 @@ namespace storm {
                 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();
-                
-                STORM_LOG_WARN("There is no check for reward finiteness yet"); //TODO
                 auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(data.preprocessedModel, targetStates);
-                data.preprocessedModel = std::move(*duplicatorResult.model);
-                // duplicatorResult.newToOldStateIndexMapping now reffers to the indices of the model we had before preprocessing this formula.
-                // This might not be the actual original model.
-                for(auto & originalModelStateIndex : duplicatorResult.newToOldStateIndexMapping){
-                    originalModelStateIndex = data.newToOldStateIndexMapping[originalModelStateIndex];
+                updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping);
+                
+                // 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 is not defined for these states.
+                // We also need to enforce that the second copy will be reached eventually with prob 1.
+                for(auto targetState : duplicatorResult.gateStates) {
+                    data.preprocessedModel.getStateLabeling().addLabelToState(data.prob1StatesLabel, targetState);
+                }
+                storm::storage::BitVector subsystemStates = storm::utility::graph::performProb1E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, duplicatorResult.gateStates);
+                subsystemStates |= duplicatorResult.secondCopy;
+                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);
                 }
-                data.newToOldStateIndexMapping = std::move(duplicatorResult.newToOldStateIndexMapping);
                 
                 // Add a reward model that gives zero reward to the states of the second copy.
                 std::vector<ValueType> objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix());
@@ -246,12 +297,119 @@ namespace storm {
             template<typename SparseModelType>
             void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::TotalRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
                 std::vector<ValueType> objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix());
+                storm::storage::BitVector positiveRewards = storm::utility::vector::filterGreaterZero(objectiveRewards);
+                storm::storage::BitVector nonNegativeRewards = positiveRewards | storm::utility::vector::filterZero(objectiveRewards);
+                STORM_LOG_THROW(nonNegativeRewards.full() || positiveRewards.empty(), storm::exceptions::InvalidPropertyException, "The reward model for the formula " << formula << " has positive and negative rewards which is not supported.");
                 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>::assertRewardFiniteness(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 = assertNegativeRewardFiniteness(data);
+                } else {
+                    actionsWithNegativeReward = storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), false);
+                }
+                if(positiveRewardsOccur) {
+                    assertPositiveRewardFiniteness(data, actionsWithNegativeReward);
+                }
+            }
+            
+            template<typename SparseModelType>
+            storm::storage::BitVector SparseMultiObjectivePreprocessor<SparseModelType>::assertNegativeRewardFiniteness(PreprocessorData& data) {
+
+                storm::storage::BitVector actionsWithNonNegativeReward(data.preprocessedModel.getTransitionMatrix().getRowCount(), true);
+                for(auto& obj : data.objectives) {
+                    if (!obj.rewardFinitenessChecked && !obj.rewardsArePositive) {
+                        obj.rewardFinitenessChecked = true;
+                        actionsWithNonNegativeReward &= storm::utility::vector::filterZero(data.preprocessedModel.getRewardModel(obj.rewardModelName).getStateActionRewardVector());
+                    }
+                }
+                
+                storm::storage::BitVector statesWithNegativeRewardForAllChoices(data.preprocessedModel.getNumberOfStates(), true);
+                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
+                    statesWithNegativeRewardForAllChoices.set(state, actionsWithNonNegativeReward.getNextSetIndex(data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]) >= data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]);
+                }
+                
+                storm::storage::BitVector submatrixRows = actionsWithNonNegativeReward;
+                //enable one row for the statesWithRewardForAllChoices so that the rowgroups will not be deleted when taking the submatrix
+                for(auto state : statesWithNegativeRewardForAllChoices) {
+                    submatrixRows.set(data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], true);
+                }
+                storm::storage::BitVector allStates(data.preprocessedModel.getNumberOfStates(), true);
+                storm::storage::SparseMatrix<ValueType> transitionsWithNonNegativeReward = data.preprocessedModel.getTransitionMatrix().getSubmatrix(false, submatrixRows, allStates, true);
+                STORM_LOG_ASSERT(data.preprocessedModel.getTransitionMatrix().getRowGroupCount() == transitionsWithNonNegativeReward.getRowGroupCount(), "Row group count mismatch.");
+                
+                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);
+                
+                auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true));
+                data.preprocessedModel = std::move(*subsystemBuilderResult.model);
+                // subsystemBuilderResult.newToOldStateIndexMapping now reffers to the indices of the model we had before building the subsystem
+                for(auto & originalModelStateIndex : subsystemBuilderResult.newToOldStateIndexMapping){
+                    originalModelStateIndex = data.newToOldStateIndexMapping[originalModelStateIndex];
+                }
+                data.newToOldStateIndexMapping = std::move(subsystemBuilderResult.newToOldStateIndexMapping);
+                return (~actionsWithNonNegativeReward) % subsystemBuilderResult.subsystemActions;
+            }
+            
+            template<typename SparseModelType>
+            void SparseMultiObjectivePreprocessor<SparseModelType>::assertPositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward) {
+                
+                auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getBackwardTransitions());
+                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).getStateActionRewardVector());
+                        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) {
+                                STORM_LOG_DEBUG("Found end component that contains positive rewards for current objective " << *obj.originalFormula << ".");
+                                data.objectivesSolvedInPreprocessing.set(objIndex);
+                                break;
+                            }
+                        }
+                    }
+                }
+            }
+            
+            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 class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<double>>;
 
             

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h

@@ -1,14 +1,14 @@
 #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 {
             
             /*
@@ -26,10 +26,8 @@ namespace storm {
                  * 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.
-                 * @param subsystem the states of the original model which should be considered. Choices that have a transition leading outside of the subsystem will be
-                 *                  removed. Hence, every state in the subsystem has to have one choice that stays inside the subsystem.
                  */
-                static PreprocessorData preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel,  storm::storage::BitVector const& subsystem);
+                static PreprocessorData preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel);
                 
             private:
                 
@@ -37,19 +35,54 @@ namespace storm {
                  * 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::UntilFormula 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);
-                static void preprocessFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none);
+                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 assertRewardFiniteness(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 assertNegativeRewardFiniteness(PreprocessorData& data);
+                
+                /*!
+                 * Checks reward finiteness for the positive rewards
+                 */
+                static void assertPositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward);
+                
+                /*!
+                 * 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);
+                
             };
             
         }

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h

@@ -6,7 +6,9 @@
 #include <iomanip>
 #include <boost/optional.hpp>
 
+#include "src/logic/Formulas.h"
 #include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h"
+#include "src/storage/BitVector.h"
 
 namespace storm {
     namespace modelchecker {
@@ -17,9 +19,13 @@ namespace storm {
                 
                 enum class QueryType { Achievability, Numerical, Pareto };
                 
+                storm::logic::MultiObjectiveFormula const& originalFormula;
+                storm::storage::BitVector objectivesSolvedInPreprocessing;
+                
                 SparseModelType const& originalModel;
                 SparseModelType preprocessedModel;
                 std::vector<uint_fast64_t> newToOldStateIndexMapping;
+                std::string prob1StatesLabel;
                 
                 QueryType queryType;
                 std::vector<SparseMultiObjectiveObjectiveInformation<typename SparseModelType::ValueType>> objectives;
@@ -27,7 +33,7 @@ namespace storm {
                 
                 bool produceSchedulers;
                 
-                SparseMultiObjectivePreprocessorData(SparseModelType const& originalModel, SparseModelType&& preprocessedModel, std::vector<uint_fast64_t>&& newToOldStateIndexMapping) : originalModel(originalModel), preprocessedModel(preprocessedModel), newToOldStateIndexMapping(newToOldStateIndexMapping), produceSchedulers(false) {
+                SparseMultiObjectivePreprocessorData(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, SparseModelType&& preprocessedModel, std::vector<uint_fast64_t>&& newToOldStateIndexMapping) : originalFormula(originalFormula), originalModel(originalModel), preprocessedModel(preprocessedModel), newToOldStateIndexMapping(newToOldStateIndexMapping), produceSchedulers(false) {
                     //Intentionally left empty
                 }
                 
@@ -36,6 +42,18 @@ namespace storm {
                     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;
+                    out << std::endl;
+                    if(!objectivesSolvedInPreprocessing.empty()) {
+                        out << "Objectives solved while preprocessing: " << std::endl;
+                        out << "--------------------------------------------------------------" << std::endl;
+                        for(auto const& subFIndex : objectivesSolvedInPreprocessing) {
+                            out<< "\t" << subFIndex << ": \t" << originalFormula.getSubformula(subFIndex) << std::endl;
+                        }
+                        out << std::endl;
+                    }
                     out << "Objectives:" << std::endl;
                     out << "--------------------------------------------------------------" << std::endl;
                     for (auto const& obj : objectives) {

src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp

@@ -20,7 +20,9 @@ namespace storm {
 
             template <class SparseModelType>
             SparseMultiObjectiveWeightVectorChecker<SparseModelType>::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), checkHasBeenCalled(false) , objectiveResults(data.objectives.size()){
-                //Intentionally left empty
+                
+                // 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>

src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h

@@ -72,6 +72,11 @@ namespace storm {
                 // stores the considered information of the multi-objective model checking problem
                 PreprocessorData const& data;
                 
+                // 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;
                 

src/transformer/SubsystemBuilder.h

@@ -31,23 +31,24 @@ namespace storm {
             struct SubsystemBuilderReturnType {
                 // The resulting model
                 std::shared_ptr<SparseModelType> model;
-                // Gives for each state in the resulting model the corresponding state in the original model and vice versa.
-                // If a state does not exist in the other model, an invalid index is given.
+                // Gives for each state in the resulting model the corresponding state in the original model.
                 std::vector<uint_fast64_t> newToOldStateIndexMapping;
-                std::vector<uint_fast64_t> oldToNewStateIndexMapping;
                 // marks the actions of the original model that are still available in the subsystem
                 storm::storage::BitVector subsystemActions;
             };
             
             /*
              * Removes all states that are not part of the subsystem
-             * all actions (i.e. rows) that lead outside of the subsystem are erased. Note that this might introduce deadlock states.
+             * all actions (i.e. rows) that lead outside of the subsystem are erased.
+             * An exception is thrown if this introduces a deadlock state.
              * 
              * @param originalModel The model to be duplicated
              * @param subsystem The states that will be kept
+             * @param consideredActions The actions that are considered to be part of the subsystem. The remaining ones will be ignored.
              */
-            static SubsystemBuilderReturnType transform(SparseModelType const& originalModel, storm::storage::BitVector const& subsystem) {
+            static SubsystemBuilderReturnType transform(SparseModelType const& originalModel, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& consideredActions) {
                 STORM_LOG_DEBUG("Invoked subsystem builder on model with " << originalModel.getNumberOfStates() << " states.");
+                STORM_LOG_THROW(!(originalModel.getInitialStates() & subsystem).empty(), storm::exceptions::InvalidArgumentException, "The subsystem would not contain any initial states");
                 SubsystemBuilderReturnType result;
                 
                 uint_fast64_t subsystemStateCount = subsystem.getNumberOfSetBits();
@@ -55,30 +56,32 @@ namespace storm {
                 if(subsystemStateCount == subsystem.size()) {
                     result.model = std::make_shared<SparseModelType>(originalModel);
                     result.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, result.model->getNumberOfStates());
-                    result.oldToNewStateIndexMapping = result.newToOldStateIndexMapping;
                     result.subsystemActions = storm::storage::BitVector(result.model->getTransitionMatrix().getRowCount(), true);
                     return result;
                 }
                 
                 result.newToOldStateIndexMapping.reserve(subsystemStateCount);
-                result.oldToNewStateIndexMapping = std::vector<uint_fast64_t>(subsystem.size(), std::numeric_limits<uint_fast64_t>::max());
                 result.subsystemActions = storm::storage::BitVector(result.model->getTransitionMatrix().getRowCount(), false);
                 for(auto subsysState : subsystem) {
-                    result.oldToNewStateIndexMapping[subsysState] = result.newToOldStateIndexMapping.size();
                     result.newToOldStateIndexMapping.push_back(subsysState);
-                    for(uint_fast64_t row = originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]; row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; ++row) {
+                    bool stateHasOneChoiceLeft = false;
+                    for(uint_fast64_t row = consideredActions.getNextSetIndex(originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]); row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; row = consideredActions.getNextSetIndex(row+1)) {
+                        bool allRowEntriesStayInSubsys = true;
                         result.subsystemActions.set(row, true);
                         for(auto const& entry : originalModel.getTransitionMatrix().getRow(row)) {
                             if(!subsystem.get(entry.getColumn())) {
-                                result.subsystemActions.set(row, false);
+                                allRowEntriesStayInSubsys = false;
                                 break;
                             }
                         }
+                        stateHasOneChoiceLeft |= allRowEntriesStayInSubsys;
+                        result.subsystemActions.set(row, allRowEntriesStayInSubsys);
                     }
+                     STORM_LOG_THROW(stateHasOneChoiceLeft, storm::exceptions::InvalidArgumentException, "The subsystem would contain a deadlock state.");
                 }
                 
                 // Transform the ingedients of the model
-                storm::storage::SparseMatrix<typename SparseModelType::ValueType> matrix = transformMatrix(originalModel.getTransitionMatrix(), result);
+                storm::storage::SparseMatrix<typename SparseModelType::ValueType> matrix = transformMatrix(originalModel.getTransitionMatrix(), subsystem, result.subsystemActions);
                 storm::models::sparse::StateLabeling labeling(matrix.getRowGroupCount());
                 for(auto const& label : originalModel.getStateLabeling().getLabels()){
                     storm::storage::BitVector newBitVectorForLabel = transformStateBitVector(originalModel.getStateLabeling().getStates(label), subsystem);
@@ -86,13 +89,13 @@ namespace storm {
                 }
                 std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels;
                 for(auto const& rewardModel : originalModel.getRewardModels()){
-                    rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, originalModel.getTransitionMatrix().getRowGroupIndices(), subsystem, result)));
+                    rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, subsystem, result.subsystemActions)));
                 }
                 boost::optional<std::vector<storm::models::sparse::LabelSet>> choiceLabeling;
                 if(originalModel.hasChoiceLabeling()){
                     choiceLabeling = transformActionValueVector<storm::models::sparse::LabelSet>(originalModel.getChoiceLabeling(), result.subsystemActions);
                 }
-                result.model = std::make_shared<SparseModelType>(createTransformedModel(originalModel, subsystem, result, matrix, labeling, rewardModels, choiceLabeling));
+                result.model = std::make_shared<SparseModelType>(createTransformedModel(originalModel, subsystem, matrix, labeling, rewardModels, choiceLabeling));
                 STORM_LOG_DEBUG("Subsystem Builder is done. Resulting model has " << result.model->getNumberOfStates() << " states.");
                 return result;
             }
@@ -100,7 +103,7 @@ namespace storm {
         private:
             template<typename ValueType = typename SparseModelType::ValueType, typename RewardModelType = typename SparseModelType::RewardModelType>
             static typename std::enable_if<std::is_same<RewardModelType, storm::models::sparse::StandardRewardModel<ValueType>>::value, RewardModelType>::type
-            transformRewardModel(RewardModelType const& originalRewardModel, std::vector<uint_fast64_t> const& originalRowGroupIndices, storm::storage::BitVector const& subsystem, SubsystemBuilderReturnType const& result) {
+            transformRewardModel(RewardModelType const& originalRewardModel, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& subsystemActions) {
                 boost::optional<std::vector<ValueType>> stateRewardVector;
                 boost::optional<std::vector<ValueType>> stateActionRewardVector;
                 boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewardMatrix;
@@ -108,40 +111,17 @@ namespace storm {
                     stateRewardVector = transformStateValueVector(originalRewardModel.getStateRewardVector(), subsystem);
                 }
                 if(originalRewardModel.hasStateActionRewards()){
-                    stateActionRewardVector = transformActionValueVector(originalRewardModel.getStateActionRewardVector(), result.subsystemActions);
+                    stateActionRewardVector = transformActionValueVector(originalRewardModel.getStateActionRewardVector(), subsystemActions);
                 }
                 if(originalRewardModel.hasTransitionRewards()){
-                    transitionRewardMatrix = transformMatrix(originalRewardModel.getTransitionRewardMatrix(), result);
+                    transitionRewardMatrix = transformMatrix(originalRewardModel.getTransitionRewardMatrix(), subsystem, subsystemActions);
                 }
                 return RewardModelType(std::move(stateRewardVector), std::move(stateActionRewardVector), std::move(transitionRewardMatrix));
             }
             
             template<typename ValueType = typename SparseModelType::ValueType>
-            static storm::storage::SparseMatrix<ValueType> transformMatrix(storm::storage::SparseMatrix<ValueType> const& originalMatrix, SubsystemBuilderReturnType const& result) {
-                // Build the builder
-                uint_fast64_t const numStates = result.newToOldStateIndexMapping.size();
-                uint_fast64_t const numRows = result.subsystemActions.getNumberOfSetBits();
-                uint_fast64_t numEntries = 0;
-                for(auto row : result.subsystemActions) {
-                    numEntries += originalMatrix.getRow(row).getNumberOfEntries();
-                }
-                storm::storage::SparseMatrixBuilder<ValueType> builder(numRows, numStates, numEntries, true, !originalMatrix.hasTrivialRowGrouping(), originalMatrix.hasTrivialRowGrouping() ? 0 : numStates);
-                
-                // Fill in the data
-                uint_fast64_t newRow = 0;
-                for(uint_fast64_t newState = 0; newState < numStates; ++newState){
-                    if(!originalMatrix.hasTrivialRowGrouping()){
-                        builder.newRowGroup(newRow);
-                    }
-                    uint_fast64_t oldState = result.newToOldStateIndexMapping[newState];
-                    for (uint_fast64_t oldRow = result.subsystemActions.getNextSetIndex(originalMatrix.getRowGroupIndices()[oldState]); oldRow < originalMatrix.getRowGroupIndices()[oldState+1]; oldRow = result.subsystemActions.getNextSetIndex(oldRow+1)){
-                        for(auto const& entry : originalMatrix.getRow(oldRow)){
-                            builder.addNextValue(newRow, result.oldToNewStateIndexMapping[entry.getColumn()], entry.getValue());
-                        }
-                        ++newRow;
-                    }
-                }
-                return builder.build();
+            static storm::storage::SparseMatrix<ValueType> transformMatrix(storm::storage::SparseMatrix<ValueType> const& originalMatrix, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& subsystemActions) {
+                return originalMatrix.getSubmatrix(false, subsystemActions, subsystem);
             }
             
             
@@ -178,7 +158,6 @@ namespace storm {
             MT>::type
             createTransformedModel(MT const& originalModel,
                                    storm::storage::BitVector const& subsystem,
-                                   SubsystemBuilderReturnType const& result,
                                    storm::storage::SparseMatrix<typename MT::ValueType>& matrix,
                                    storm::models::sparse::StateLabeling& stateLabeling,
                                    std::unordered_map<std::string,
@@ -193,7 +172,6 @@ namespace storm {
             MT>::type
             createTransformedModel(MT const& originalModel,
                                    storm::storage::BitVector const& subsystem,
-                                   SubsystemBuilderReturnType const& result,
                                    storm::storage::SparseMatrix<typename MT::ValueType>& matrix,
                                    storm::models::sparse::StateLabeling& stateLabeling,
                                    std::unordered_map<std::string,