parametric simplifier for mdps

src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h

@@ -0,0 +1,37 @@
+#pragma once
+
+#include "storm/logic/Formulas.h"
+#include "storm/modelchecker/CheckTask.h"
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm/utility/parametric.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace parametric {
+            template <typename SparseModelType, typename ConstantType>
+            
+            
+            /*!
+             * Class to efficiently check a formula on a parametric model on different parameter instantiations
+             */
+            class SparseInstantiationModelChecker {
+            public:
+                SparseInstantiationModelChecker(SparseModelType const& parametricModel);
+                
+                virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) = 0;
+                
+                virtual void specifyFormula(CheckTask<storm::logic::Formula, ValueType> const& checkTask) = 0;
+                
+                virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
+
+            private:
+                
+                SparseModelType const& parametricModel;
+                
+            };
+        }
+    }
+}
+
+
+#endif //STORM_SPARSEINSTANTIATIONMODELCHECKER_H

src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp

@@ -0,0 +1,5 @@
+//
+// Created by Tim Quatmann on 23/02/2017.
+//
+
+#include "SparseInstantiationModelChecker.h"

src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h

@@ -0,0 +1,16 @@
+//
+// Created by Tim Quatmann on 23/02/2017.
+//
+
+#ifndef STORM_SPARSEINSTANTIATIONMODELCHECKER_H
+#define STORM_SPARSEINSTANTIATIONMODELCHECKER_H
+
+
+
+class SparseInstantiationModelChecker {
+
+};
+
+
+
+#endif //STORM_SPARSEINSTANTIATIONMODELCHECKER_H

src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp

@@ -31,6 +31,9 @@
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/logic/FragmentSpecification.h"
 
+#include "storm/transformer/SparseParametricMdpSimplifier.h"
+
+
 namespace storm {
     namespace modelchecker {
         namespace region {
@@ -83,6 +86,17 @@ namespace storm {
                     //The result is already known. Nothing else to do here
                     return;
                 }
+                                
+                storm::transformer::SparseParametricMdpSimplifier<ParametricSparseModelType> simplifier(*this->getModel());
+                if(!simplifier.simplify(*this->getSpecifiedFormula())) {
+                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplification was not possible");
+                }
+                simpleModel = simplifier.getSimplifiedModel();
+                STORM_LOG_THROW(simplifier.getSimplifiedFormula()->isOperatorFormula(), storm::exceptions::UnexpectedException, "Expected that the simplified formula is an Operator formula");
+                simpleFormula =  std::dynamic_pointer_cast<storm::logic::OperatorFormula const>(simplifier.getSimplifiedFormula());
+                
+                /*
+                
                 STORM_LOG_DEBUG("Elimination of deterministic states with constant outgoing transitions is happening now.");
                 // Determine the set of states that is reachable from the initial state without jumping over a target state.
                 storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel()->getTransitionMatrix(), this->getModel()->getInitialStates(), maybeStates, targetStates);
@@ -199,6 +213,7 @@ namespace storm {
                 std::shared_ptr<storm::logic::AtomicLabelFormula> targetFormulaPtr(new storm::logic::AtomicLabelFormula("target"));
                 std::shared_ptr<storm::logic::EventuallyFormula> eventuallyFormula(new storm::logic::EventuallyFormula(targetFormulaPtr));
                 simpleFormula = std::shared_ptr<storm::logic::OperatorFormula const>(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound())));
+                 */
             }
 
             template<typename ParametricSparseModelType, typename ConstantType>

src/storm/storage/MaximalEndComponentDecomposition.cpp

@@ -196,6 +196,9 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
         template class MaximalEndComponentDecomposition<storm::RationalNumber>;
         template MaximalEndComponentDecomposition<storm::RationalNumber>::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model);
+
+        template class MaximalEndComponentDecomposition<storm::RationalFunction>;
+        template MaximalEndComponentDecomposition<storm::RationalFunction>::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model);
 #endif
     }
 }

src/storm/transformer/SparseParametricDtmcSimplifier.cpp

@@ -30,7 +30,7 @@ namespace storm {
             }
             storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
-            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->originalModel.getBackwardTransitions(), phiStates, psiStates);
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->originalModel, phiStates, psiStates);
             // Only consider the maybestates that are reachable from one initial state without hopping over a target (i.e., prob1) state
             storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & ~statesWithProbability01.first, ~statesWithProbability01.first, statesWithProbability01.second);
             storm::storage::BitVector maybeStates = reachableGreater0States & ~statesWithProbability01.second;
@@ -111,7 +111,6 @@ namespace storm {
             // Only consider the states that are reachable from an initial state without hopping over a target state
             storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & statesWithProb1, statesWithProb1, targetStates);
             storm::storage::BitVector maybeStates = reachableStates & ~targetStates;
-            targetStates = targetStates & reachableStates;
             
             // obtain the resulting subsystem
             std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
@@ -126,7 +125,7 @@ namespace storm {
             this->simplifiedFormula = std::make_shared<storm::logic::RewardOperatorFormula const>(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation);
             
             // Eliminate all states for which all outgoing transitions are constant
-            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel);
+            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front());
                 
             return true;
         }

src/storm/transformer/SparseParametricMdpSimplifier.cpp

@@ -0,0 +1,240 @@
+#include "storm/transformer/SparseParametricMdpSimplifier.h"
+
+#include "storm/adapters/CarlAdapter.h"
+
+#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/models/sparse/Mdp.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/transformer/GoalStateMerger.h"
+#include "storm/transformer/EndComponentEliminator.h"
+#include "storm/utility/graph.h"
+#include "storm/utility/vector.h"
+
+#include <storm/exceptions/NotSupportedException.h>
+#include <storm/exceptions/UnexpectedException.h>
+
+namespace storm {
+    namespace transformer {
+
+        template<typename SparseModelType>
+        SparseParametricMdpSimplifier<SparseModelType>::SparseParametricMdpSimplifier(SparseModelType const& model) : SparseParametricModelSimplifier<SparseModelType>(model) {
+            // intentionally left empty
+        }
+        
+        template<typename SparseModelType>
+        bool SparseParametricMdpSimplifier<SparseModelType>::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) {
+            bool minimizing = formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType);
+            
+            // Get the prob0, prob1 and the maybeStates
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->originalModel);
+            if(!propositionalChecker.canHandle(formula.getSubformula().asUntilFormula().getLeftSubformula()) || !propositionalChecker.canHandle(formula.getSubformula().asUntilFormula().getRightSubformula())) {
+                STORM_LOG_DEBUG("Can not simplify when Until-formula has non-propositional subformula(s). Formula: " << formula);
+                return false;
+            }
+            storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = minimizing ?
+                                                                                                      storm::utility::graph::performProb01Min(this->originalModel, phiStates, psiStates) :
+                                                                                                      storm::utility::graph::performProb01Max(this->originalModel, phiStates, psiStates);
+                                                                                                      
+            // Only consider the maybestates that are reachable from one initial state without hopping over a target (i.e., prob1) state
+            storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & ~statesWithProbability01.first, ~statesWithProbability01.first, statesWithProbability01.second);
+            storm::storage::BitVector maybeStates = reachableGreater0States & ~statesWithProbability01.second;
+            
+            // obtain the resulting subsystem
+            storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
+            this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first);
+            this->simplifiedModel->getStateLabeling().addLabel("target", statesWithProbability01.second);
+            this->simplifiedModel->getStateLabeling().addLabel("sink", statesWithProbability01.first);
+            
+            // obtain the simplified formula for the simplified model
+            auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> ("target");
+            auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula const>(labelFormula, storm::logic::FormulaContext::Probability);
+            this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(eventuallyFormula, formula.getOperatorInformation());
+            
+            // Eliminate all states for which all outgoing transitions are constant
+            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel);
+                        
+            // Eliminate the end components that do not contain a target or a sink state (only required if the probability is maximized)
+            if(!minimizing) {
+                this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink"));
+            }
+            
+            return true;
+        }
+        
+        template<typename SparseModelType>
+        bool SparseParametricMdpSimplifier<SparseModelType>::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) {
+            STORM_LOG_THROW(!formula.getSubformula().asBoundedUntilFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported.");
+            STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().hasUpperBound(), storm::exceptions::UnexpectedException, "Expected a bounded until formula with an upper bound.");
+            STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().isStepBounded(), storm::exceptions::UnexpectedException, "Expected a bounded until formula with step bounds.");
+                        
+            bool minimizing = formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType);
+            uint_fast64_t upperStepBound = formula.getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt();
+            if (formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict()) {
+                STORM_LOG_THROW(upperStepBound > 0, storm::exceptions::UnexpectedException, "Expected a strict upper bound that is greater than zero.");
+                --upperStepBound;
+            }
+            
+            // Get the prob0, target, and the maybeStates
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->originalModel);
+            if(!propositionalChecker.canHandle(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula()) || !propositionalChecker.canHandle(formula.getSubformula().asBoundedUntilFormula().getRightSubformula())) {
+                STORM_LOG_DEBUG("Can not simplify when Until-formula has non-propositional subformula(s). Formula: " << formula);
+                return false;
+            }
+            storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            storm::storage::BitVector probGreater0States = minimizing ?
+                                                           storm::utility::graph::performProbGreater0A(this->originalModel.getTransitionMatrix(), this->originalModel.getTransitionMatrix().getRowGroupIndices(), this->originalModel.getBackwardTransitions(), phiStates, psiStates, true, upperStepBound) :
+                                                           storm::utility::graph::performProbGreater0E(this->originalModel.getBackwardTransitions(), phiStates, psiStates, true, upperStepBound);
+            storm::storage::BitVector prob0States = ~probGreater0States;
+            
+            // Only consider the maybestates that are reachable from one initial probGreater0 state within the given amount of steps and without hopping over a target state
+            storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & probGreater0States, probGreater0States, psiStates, true, upperStepBound);
+            storm::storage::BitVector maybeStates = reachableGreater0States & ~psiStates;
+            
+            // obtain the resulting subsystem
+            storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
+            this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
+            this->simplifiedModel->getStateLabeling().addLabel("target", psiStates);
+            this->simplifiedModel->getStateLabeling().addLabel("sink", prob0States);
+            
+            // obtain the simplified formula for the simplified model
+            auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> ("target");
+            auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula const>(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps);
+            this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(boundedUntilFormula, formula.getOperatorInformation());
+            
+            return true;
+        }
+        
+        template<typename SparseModelType>
+        bool SparseParametricMdpSimplifier<SparseModelType>::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) {
+            typename SparseModelType::RewardModelType const& originalRewardModel = formula.hasRewardModelName() ? this->originalModel.getRewardModel(formula.getRewardModelName()) : this->originalModel.getUniqueRewardModel();
+            
+            bool minimizing = formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType);
+
+            // Get the prob1 and the maybeStates
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->originalModel);
+            if(!propositionalChecker.canHandle(formula.getSubformula().asEventuallyFormula().getSubformula())) {
+                STORM_LOG_DEBUG("Can not simplify when reachability reward formula has non-propositional subformula(s). Formula: " << formula);
+                return false;
+            }
+            storm::storage::BitVector targetStates = std::move(propositionalChecker.check(formula.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            // The set of target states can be extended by the states that reach target with probability 1 without collecting any reward
+            // TODO for the call of Prob1E we could restrict the analysis to actions with zero reward instead of states with zero reward
+            targetStates = minimizing ?
+                           storm::utility::graph::performProb1E(this->originalModel, this->originalModel.getBackwardTransitions(), originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), targetStates) :
+                           storm::utility::graph::performProb1A(this->originalModel, this->originalModel.getBackwardTransitions(), originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), targetStates);
+            storm::storage::BitVector statesWithProb1 = minimizing ?
+                                     storm::utility::graph::performProb1E(this->originalModel, this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), targetStates) :
+                                     storm::utility::graph::performProb1A(this->originalModel, this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), targetStates);
+            storm::storage::BitVector infinityStates = ~statesWithProb1;
+            // Only consider the states that are reachable from an initial state without hopping over a target state
+            storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & statesWithProb1, statesWithProb1, targetStates);
+            storm::storage::BitVector maybeStates = reachableStates & ~targetStates;
+            
+            // obtain the resulting subsystem
+            std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
+            storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
+            this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector);
+            this->simplifiedModel->getStateLabeling().addLabel("target", targetStates);
+            this->simplifiedModel->getStateLabeling().addLabel("sink", infinityStates);
+            
+            // obtain the simplified formula for the simplified model
+            auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> ("target");
+            auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula const>(labelFormula, storm::logic::FormulaContext::Reward);
+            this->simplifiedFormula = std::make_shared<storm::logic::RewardOperatorFormula const>(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation);
+            
+            // Eliminate all states for which all outgoing transitions are constant
+            this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front());
+            
+            // Eliminate the end components in which no reward is collected (only required if rewards are minimized)
+            this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink"), rewardModelNameAsVector.front());
+            return true;
+        }
+        
+        template<typename SparseModelType>
+        bool SparseParametricMdpSimplifier<SparseModelType>::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) {
+            STORM_LOG_THROW(formula.getSubformula().asCumulativeRewardFormula().isStepBounded(), storm::exceptions::UnexpectedException, "Expected a cumulative reward formula with step bounds.");
+                        
+            typename SparseModelType::RewardModelType const& originalRewardModel = formula.hasRewardModelName() ? this->originalModel.getRewardModel(formula.getRewardModelName()) : this->originalModel.getUniqueRewardModel();
+
+            bool minimizing = formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType);
+            uint_fast64_t stepBound = formula.getSubformula().asCumulativeRewardFormula().getBound().evaluateAsInt();
+            if (formula.getSubformula().asCumulativeRewardFormula().isBoundStrict()) {
+                STORM_LOG_THROW(stepBound > 0, storm::exceptions::UnexpectedException, "Expected a strict upper bound that is greater than zero.");
+                --stepBound;
+            }
+            
+            // Get the states with non-zero reward
+            storm::storage::BitVector maybeStates = minimizing ?
+                                                    storm::utility::graph::performProbGreater0A(this->originalModel.getTransitionMatrix(), this->originalModel.getTransitionMatrix().getRowGroupIndices(), this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), ~originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), true, stepBound) :
+                                                    storm::utility::graph::performProbGreater0E(this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), ~originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), true, stepBound);
+            storm::storage::BitVector zeroRewardStates = ~maybeStates;
+            storm::storage::BitVector noStates(this->originalModel.getNumberOfStates(), false);
+            
+            // obtain the resulting subsystem
+            std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
+            storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
+            this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector);
+            
+            // obtain the simplified formula for the simplified model
+            this->simplifiedFormula = formula.asSharedPointer();
+            
+            return true;
+        }
+        
+        template<typename SparseModelType>
+        std::shared_ptr<SparseModelType> SparseParametricMdpSimplifier<SparseModelType>::eliminateNeutralEndComponents(SparseModelType const& model, storm::storage::BitVector const& ignoredStates, boost::optional<std::string> const& rewardModelName) {
+            
+            // Get the actions that can be part of an EC
+            storm::storage::BitVector possibleECActions(model.getNumberOfChoices(), true);
+            for (auto const& state : ignoredStates) {
+                for(uint_fast64_t actionIndex = model.getTransitionMatrix().getRowGroupIndices()[state]; actionIndex < model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++actionIndex) {
+                    possibleECActions.set(actionIndex, false);
+                }
+            }
+            
+            // Get the action-based reward values and unselect non-zero reward actions
+            std::vector<typename SparseModelType::ValueType> actionRewards;
+            if(rewardModelName) {
+                actionRewards = model.getRewardModel(*rewardModelName).getTotalRewardVector(model.getTransitionMatrix());
+                uint_fast64_t actionIndex = 0;
+                for (auto const& actionReward : actionRewards) {
+                    if(!storm::utility::isZero(actionReward)) {
+                        possibleECActions.set(actionIndex, false);
+                    }
+                    ++actionIndex;
+                }
+            }
+            
+            // Invoke EC Elimination
+            auto ecEliminatorResult = storm::transformer::EndComponentEliminator<typename SparseModelType::ValueType>::transform(model.getTransitionMatrix(), storm::storage::BitVector(model.getNumberOfStates(), true), possibleECActions, storm::storage::BitVector(model.getNumberOfStates(), false));
+            
+            // obtain the reward model for the resulting system
+            std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels;
+            if(rewardModelName) {
+                std::vector<typename SparseModelType::ValueType> newActionRewards(ecEliminatorResult.matrix.getRowCount());
+                storm::utility::vector::selectVectorValues(newActionRewards, ecEliminatorResult.newToOldRowMapping, actionRewards);
+                rewardModels.insert(std::make_pair(*rewardModelName, typename SparseModelType::RewardModelType(boost::none, std::move(actionRewards))));
+            }
+            
+            // the new labeling
+            storm::models::sparse::StateLabeling labeling(ecEliminatorResult.matrix.getRowGroupCount());
+            for (auto const& label : model.getStateLabeling().getLabels()) {
+                auto const& origStatesWithLabel = model.getStates(label);
+                storm::storage::BitVector newStatesWithLabel(ecEliminatorResult.matrix.getRowGroupCount(), false);
+                for (auto const& origState : origStatesWithLabel) {
+                    newStatesWithLabel.set(ecEliminatorResult.oldToNewStateMapping[origState], true);
+                }
+                labeling.addLabel(label, std::move(newStatesWithLabel));
+            }
+            
+            return std::make_shared<SparseModelType>(std::move(ecEliminatorResult.matrix), std::move(labeling), std::move(rewardModels));
+        }
+
+
+        template class SparseParametricMdpSimplifier<storm::models::sparse::Mdp<storm::RationalFunction>>;
+    }
+}

src/storm/transformer/SparseParametricMdpSimplifier.h

@@ -0,0 +1,41 @@
+#pragma once
+
+
+#include "storm/transformer/SparseParametricModelSimplifier.h"
+
+namespace storm {
+    namespace transformer {
+
+        /*!
+         * This class performs different steps to simplify the given (parametric) model.
+         * Checking the obtained simplified formula on the simplified model yields the same result as checking the original formula on the original model (wrt. to the initial states of the two models)
+         * End Components of nondeterministic models are removed whenever this is valid for the corresponding formula. This allows us to apply, e.g., value iteration that does not start from the 0,...,0 vector.
+         */
+        template<typename SparseModelType>
+        class SparseParametricMdpSimplifier : public SparseParametricModelSimplifier<SparseModelType> {
+        public:
+            SparseParametricMdpSimplifier(SparseModelType const& model);
+            
+        protected:
+            
+            // Perform the simplification for the corresponding formula type
+            virtual bool simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) override;
+            virtual bool simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) override;
+            virtual bool simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) override;
+            virtual bool simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) override;
+            
+                        
+            /*!
+             * Eliminates all end components of the model satisfying
+             * * ignoredStates is false for all states of the EC
+             * * (if rewardModelName is given) there is no reward collected while staying inside the EC.
+             *
+             * Eliminating an EC means that it is replaced by a single state whose incoming and outgoing tansitions correspond to the incoming and outgoing transitions of the EC
+             *
+             * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given)
+             */
+            static std::shared_ptr<SparseModelType> eliminateNeutralEndComponents(SparseModelType const& model, storm::storage::BitVector const& ignoredStates, boost::optional<std::string> const& rewardModelName = boost::none);
+            
+        };
+    }
+}

src/storm/transformer/SparseParametricModelSimplifier.cpp

@@ -1,4 +1,5 @@
 #include <storm/exceptions/InvalidArgumentException.h>
+#include <storm/exceptions/UnexpectedException.h>
 #include "storm/transformer/SparseParametricModelSimplifier.h"
 
 
@@ -74,7 +75,7 @@ namespace storm {
         bool SparseParametricModelSimplifier<SparseModelType>::simplifyForReachabilityProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) {
             // transform to until formula
             auto untilFormula = std::make_shared<storm::logic::UntilFormula const>(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asEventuallyFormula().getSubformula().asSharedPointer());
-            return simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula(untilFormula,formula.getOperatorInformation()));
+            return simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula(untilFormula, formula.getOperatorInformation()));
         }
 
         template<typename SparseModelType>
@@ -99,7 +100,7 @@ namespace storm {
         }
         
         template<typename SparseModelType>
-         std::shared_ptr<SparseModelType> SparseParametricModelSimplifier<SparseModelType>::eliminateConstantDeterministicStates(SparseModelType const& model) {
+         std::shared_ptr<SparseModelType> SparseParametricModelSimplifier<SparseModelType>::eliminateConstantDeterministicStates(SparseModelType const& model, boost::optional<std::string> const& rewardModelName) {
             storm::storage::SparseMatrix<typename SparseModelType::ValueType> const& sparseMatrix = model.getTransitionMatrix();
             
             // Get the states without any label
@@ -109,13 +110,10 @@ namespace storm {
             }
             considerForElimination.complement();
                             
-            // get the state-based reward values (or the 0..0 vector if there are no rewards)
-            std::vector<typename SparseModelType::ValueType> stateValues;
-            if(model.hasUniqueRewardModel()) {
-                 stateValues = model.getUniqueRewardModel().getTotalRewardVector(sparseMatrix);
-            } else {
-                STORM_LOG_THROW(!model.hasRewardModel(), storm::exceptions::InvalidArgumentException, "Invoked state elimination but there are multiple reward models defined");
-                stateValues = std::vector<typename SparseModelType::ValueType>(model.getNumberOfStates(), storm::utility::zero<typename SparseModelType::ValueType>());
+            // get the action-based reward values
+            std::vector<typename SparseModelType::ValueType> actionRewards;
+            if(rewardModelName) {
+                actionRewards = model.getRewardModel(*rewardModelName).getTotalRewardVector(sparseMatrix);
             }
             
             // Find the states that are to be eliminated
@@ -123,7 +121,7 @@ namespace storm {
             storm::storage::BitVector keptStates(sparseMatrix.getRowGroupCount(), true);
             storm::storage::BitVector keptRows(sparseMatrix.getRowCount(), true);
             for (auto state : considerForElimination) {
-                if (sparseMatrix.getRowGroupSize(state) == 1 && storm::utility::isConstant(stateValues[state])) {
+                if (sparseMatrix.getRowGroupSize(state) == 1 && (!rewardModelName.is_initialized() || storm::utility::isConstant(actionRewards[sparseMatrix.getRowGroupIndices()[state]]))) {
                     bool hasOnlyConstEntries = true;
                     for (auto const& entry : sparseMatrix.getRowGroup(state)) {
                         if(!storm::utility::isConstant(entry.getValue())) {
@@ -139,19 +137,40 @@ namespace storm {
                 }
             }
             
+            // only keep the relevant reward values and translate them to state-based rewards
+            std::vector<typename SparseModelType::ValueType> rewardsOfEliminatedStates;
+            if(rewardModelName) {
+                rewardsOfEliminatedStates.reserve(model.getNumberOfStates());
+                for(uint_fast64_t state = 0; state < model.getNumberOfStates(); ++state) {
+                    if(keptStates.get(state)) {
+                        // The current state will not be eliminated. Hence we do not need to consider its reward during elimination
+                        rewardsOfEliminatedStates.push_back(storm::utility::zero<typename SparseModelType::ValueType>());
+                    } else {
+                        // We need to keep track of the reward of this state during elimination
+                        rewardsOfEliminatedStates.push_back(std::move(actionRewards[sparseMatrix.getRowGroupIndices()[state]]));
+                    }
+                }
+            } else {
+                rewardsOfEliminatedStates.resize(model.getNumberOfStates(), storm::utility::zero<typename SparseModelType::ValueType>());
+            }
+            
+            // invoke elimination and obtain resulting transition matrix
             storm::storage::FlexibleSparseMatrix<typename SparseModelType::ValueType> flexibleMatrix(sparseMatrix);
             storm::storage::FlexibleSparseMatrix<typename SparseModelType::ValueType> flexibleBackwardTransitions(sparseMatrix.transpose(true), true);
-            storm::solver::stateelimination::PrioritizedStateEliminator<typename SparseModelType::ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, statesToEliminate, stateValues);
+            storm::solver::stateelimination::PrioritizedStateEliminator<typename SparseModelType::ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, statesToEliminate, rewardsOfEliminatedStates);
             stateEliminator.eliminateAll();
+            storm::storage::SparseMatrix<typename  SparseModelType::ValueType> newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, keptStates);
             
-            stateValues = storm::utility::vector::filterVector(stateValues, keptRows);
-            
+            // obtain the reward model for the resulting system
             std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels;
-            if(model.hasUniqueRewardModel()) {
-                rewardModels.insert(std::make_pair(model.getRewardModels().begin()->first, typename SparseModelType::RewardModelType(boost::none, stateValues)));
+            if(rewardModelName) {
+                actionRewards = storm::utility::vector::filterVector(actionRewards, keptRows);
+                rewardsOfEliminatedStates = storm::utility::vector::filterVector(rewardsOfEliminatedStates, keptStates);
+                storm::utility::vector::addVectorToGroupedVector(actionRewards, rewardsOfEliminatedStates, newTransitionMatrix.getRowGroupIndices());
+                rewardModels.insert(std::make_pair(*rewardModelName, typename SparseModelType::RewardModelType(boost::none, std::move(actionRewards))));
             }
-            
-            return std::make_shared<SparseModelType>(flexibleMatrix.createSparseMatrix(keptRows, keptStates), model.getStateLabeling().getSubLabeling(keptStates), std::move(rewardModels));
+                
+            return std::make_shared<SparseModelType>(std::move(newTransitionMatrix), model.getStateLabeling().getSubLabeling(keptStates), std::move(rewardModels));
         }
 
 

src/storm/transformer/SparseParametricModelSimplifier.h

@@ -53,11 +53,11 @@ namespace storm {
              * * there is only one enabled action (i.e., there is no nondeterministic choice at the state),
              * * all outgoing transitions are constant,
              * * there is no statelabel defined, and
-             * * (if applicable) the reward collected at the state is constant.
+             * * (if rewardModelName is given) the reward collected at the state is constant.
              *
-             * Assumes that there is at most one reward model defined. Otherwise an exception is thrown.
+             * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given)
              */
-            static std::shared_ptr<SparseModelType> eliminateConstantDeterministicStates(SparseModelType const& model);
+            static std::shared_ptr<SparseModelType> eliminateConstantDeterministicStates(SparseModelType const& model, boost::optional<std::string> const& rewardModelName = boost::none);
             
             SparseModelType const& originalModel;
             

src/storm/utility/graph.cpp

@@ -1352,9 +1352,8 @@ namespace storm {
             
             template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
-            
             template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
-            
+
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
             
             
@@ -1366,7 +1365,7 @@ namespace storm {
             template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,  storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
             
-            
+            template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;