infinite horizon helper now store information

about shielding tasks and whether to compute all choice values

src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp

@@ -4,85 +4,95 @@
 namespace storm {
     namespace modelchecker {
         namespace helper {
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::SingleValueModelCheckerHelper() : _produceScheduler(false) {
                 // Intentionally left empty
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::setOptimizationDirection(storm::solver::OptimizationDirection const& direction) {
                 _optimizationDirection = direction;
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::clearOptimizationDirection() {
                 _optimizationDirection = boost::none;
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::isOptimizationDirectionSet() const {
                 return _optimizationDirection.is_initialized();
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             storm::solver::OptimizationDirection const& SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::getOptimizationDirection() const {
                 STORM_LOG_ASSERT(isOptimizationDirectionSet(), "Requested optimization direction but none was set.");
                 return _optimizationDirection.get();
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::minimize() const {
                 return storm::solver::minimize(getOptimizationDirection());
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::maximize() const {
                 return storm::solver::maximize(getOptimizationDirection());
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             boost::optional<storm::solver::OptimizationDirection> SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::getOptionalOptimizationDirection() const {
                 return _optimizationDirection;
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& threshold) {
                 _valueThreshold = std::make_pair(comparisonType, threshold);
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::clearValueThreshold() {
                 _valueThreshold = boost::none;
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::isValueThresholdSet() const {
                 return _valueThreshold.is_initialized();
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             storm::logic::ComparisonType const& SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::getValueThresholdComparisonType() const {
                 STORM_LOG_ASSERT(isValueThresholdSet(), "Value Threshold comparison type was requested but not set before.");
                 return _valueThreshold->first;
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             ValueType const& SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::getValueThresholdValue() const {
                 STORM_LOG_ASSERT(isValueThresholdSet(), "Value Threshold comparison type was requested but not set before.");
                 return _valueThreshold->second;
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::setProduceScheduler(bool value) {
                 _produceScheduler = value;
             }
-            
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::isProduceSchedulerSet() const {
                 return _produceScheduler;
             }
 
+            template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
+            void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::setProduceChoiceValues(bool value) {
+                _produceChoiceValues = value;
+            }
+
+            template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
+            bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::isProduceChoiceValuesSet() const {
+                return _produceChoiceValues;
+            }
+
             template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
             void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::setQualitative(bool value) {
                 _isQualitativeSet = value;
@@ -92,17 +102,17 @@ namespace storm {
             bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::isQualitativeSet() const {
                 return _isQualitativeSet;
             }
- 
+
             template class SingleValueModelCheckerHelper<double, storm::models::ModelRepresentation::Sparse>;
             template class SingleValueModelCheckerHelper<storm::RationalNumber, storm::models::ModelRepresentation::Sparse>;
             template class SingleValueModelCheckerHelper<storm::RationalFunction, storm::models::ModelRepresentation::Sparse>;
-            
+
             template class SingleValueModelCheckerHelper<double, storm::models::ModelRepresentation::DdSylvan>;
             template class SingleValueModelCheckerHelper<storm::RationalNumber, storm::models::ModelRepresentation::DdSylvan>;
             template class SingleValueModelCheckerHelper<storm::RationalFunction, storm::models::ModelRepresentation::DdSylvan>;
-            
+
             template class SingleValueModelCheckerHelper<double, storm::models::ModelRepresentation::DdCudd>;
-            
+
         }
     }
-}
+}

src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h

@@ -8,7 +8,7 @@
 namespace storm {
     namespace modelchecker {
         namespace helper {
-            
+
             /*!
              * Helper for model checking queries where we are interested in (optimizing) a single value per state.
              * @tparam ValueType The type of a value
@@ -19,47 +19,47 @@ namespace storm {
             public:
 
                 SingleValueModelCheckerHelper();
-                
+
                 /*!
                  * Sets the optimization direction, i.e., whether we want to minimize or maximize the value for each state
                  * Has no effect for models without nondeterminism.
                  * Has to be set if there is nondeterminism in the model.
                  */
                 void setOptimizationDirection(storm::solver::OptimizationDirection const& direction);
-                
+
                 /*!
                  * Clears the optimization direction if it was set before.
                  */
                 void clearOptimizationDirection();
-                
+
                 /*!
                  * @return true if there is an optimization direction set
                  */
                 bool isOptimizationDirectionSet() const;
-                
+
                 /*!
                  * @pre an optimization direction has to be set before calling this.
                  * @return the optimization direction.
                  */
                 storm::solver::OptimizationDirection const& getOptimizationDirection() const;
-                
+
                 /*!
                  * @pre an optimization direction has to be set before calling this.
                  * @return true iff the optimization goal is to minimize the value for each state
                  */
                 bool minimize() const;
-                
+
                 /*!
                  * @pre an optimization direction has to be set before calling this.
                  * @return true iff the optimization goal is to maximize the value for each state
                  */
                 bool maximize() const;
-                
+
                 /*!
                  * @return The optimization direction (if it was set)
                  */
                 boost::optional<storm::solver::OptimizationDirection> getOptionalOptimizationDirection() const;
-                
+
                 /*!
                  * Sets a goal threshold for the value at each state. If such a threshold is set, it is assumed that we are only interested
                  * in the satisfaction of the threshold. Setting this allows the helper to compute values only up to the precision
@@ -68,39 +68,49 @@ namespace storm {
                  * @param thresholdValue The value used on the right hand side of the comparison relation.
                  */
                 void setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& thresholdValue);
-                
+
                 /*!
                  * Clears the valueThreshold if it was set before.
                  */
                 void clearValueThreshold();
-                
+
                 /*!
                  * @return true, if a value threshold has been set.
                  */
                 bool isValueThresholdSet() const;
-                
+
                 /*!
                  * @pre A value threshold has to be set before calling this.
                  * @return The relation used when comparing computed values (left hand side) with the specified threshold value (right hand side).
                  */
                 storm::logic::ComparisonType const& getValueThresholdComparisonType() const;
-                
+
                 /*!
                  * @pre A value threshold has to be set before calling this.
                  * @return The value used on the right hand side of the comparison relation.
                  */
                 ValueType const& getValueThresholdValue() const;
-                
+
                 /*!
                  * Sets whether an optimal scheduler shall be constructed during the computation
                  */
                 void setProduceScheduler(bool value);
-                
+
                 /*!
                  * @return whether an optimal scheduler shall be constructed during the computation
                  */
                 bool isProduceSchedulerSet() const;
 
+                /*!
+                 * Sets whether all choice values shall be computed
+                 */
+                void setProduceChoiceValues(bool value);
+
+                /*!
+                 * @return whether all choice values shall be computed
+                 */
+                bool isProduceChoiceValuesSet() const;
+
                 /*!
                 * Sets whether the property needs to be checked qualitatively
                 */
@@ -110,13 +120,14 @@ namespace storm {
                  * @return whether the property needs to be checked qualitatively
                  */
                 bool isQualitativeSet() const;
-                
+
             private:
                 boost::optional<storm::solver::OptimizationDirection> _optimizationDirection;
                 boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> _valueThreshold;
                 bool _produceScheduler;
+                bool _produceChoiceValues;
                 bool _isQualitativeSet;
             };
         }
     }
-}
+}

src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h

@@ -8,16 +8,16 @@
 
 namespace storm {
     class Environment;
-    
+
     namespace models {
         namespace sparse {
             template <typename VT> class StandardRewardModel;
         }
     }
-    
+
     namespace modelchecker {
         namespace helper {
-        
+
             /*!
              * Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system.
              * @tparam ValueType the type a value can have
@@ -27,22 +27,22 @@ namespace storm {
             class SparseInfiniteHorizonHelper : public SingleValueModelCheckerHelper<ValueType, storm::models::ModelRepresentation::Sparse> {
 
             public:
-                
+
                 /*!
                  * The type of a component in which the system resides in the long run (BSCC for deterministic models, MEC for nondeterministic models)
                  */
                 using LongRunComponentType = typename std::conditional<Nondeterministic, storm::storage::MaximalEndComponent, storm::storage::StronglyConnectedComponent>::type;
-                
+
                 /*!
                  * Function mapping from indices to values
                  */
                 typedef std::function<ValueType(uint64_t)> ValueGetter;
-                
+
                 /*!
                  * Initializes the helper for a discrete time (i.e. DTMC, MDP)
                  */
                 SparseInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
-                
+
                 /*!
                  * Initializes the helper for continuous time (i.e. MA)
                  */
@@ -52,33 +52,33 @@ namespace storm {
                  * Initializes the helper for continuous time (i.e. CTMC)
                  */
                 SparseInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates);
-                
+
                 /*!
                  * Provides backward transitions that can be used during the computation.
                  * Providing them is optional. If they are not provided, they will be computed internally
                  * Be aware that this class does not take ownership, i.e. the caller has to make sure that the reference to the backwardstransitions remains valid.
                  */
                 void provideBackwardTransitions(storm::storage::SparseMatrix<ValueType> const& backwardsTransitions);
-    
+
                 /*!
                  * Provides the decomposition into long run components (BSCCs/MECs) that can be used during the computation.
                  * Providing the decomposition is optional. If it is not provided, they will be computed internally.
                  * Be aware that this class does not take ownership, i.e. the caller has to make sure that the reference to the decomposition remains valid.
                  */
                 void provideLongRunComponentDecomposition(storm::storage::Decomposition<LongRunComponentType> const& decomposition);
-                
+
                 /*!
                  * Computes the long run average probabilities, i.e., the fraction of the time we are in a psiState
                  * @return a value for each state
                  */
                 std::vector<ValueType> computeLongRunAverageProbabilities(Environment const& env, storm::storage::BitVector const& psiStates);
-                
+
                 /*!
                  * Computes the long run average rewards, i.e., the average reward collected per time unit
                  * @return a value for each state
                  */
                 std::vector<ValueType> computeLongRunAverageRewards(Environment const& env, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel);
-                
+
                 /*!
                  * Computes the long run average value given the provided state and action-based rewards.
                  * @param stateValues a vector containing a value for every state
@@ -86,7 +86,7 @@ namespace storm {
                  * @return a value for each state
                  */
                 std::vector<ValueType> computeLongRunAverageValues(Environment const& env, std::vector<ValueType> const* stateValues = nullptr, std::vector<ValueType> const* actionValues = nullptr);
-                
+
                 /*!
                  * Computes the long run average value given the provided state and action based rewards
                  * @param stateValuesGetter a function returning a value for a given state index
@@ -102,39 +102,40 @@ namespace storm {
                  * @post if scheduler production is enabled and Nondeterministic is true, getProducedOptimalChoices() contains choices for the states of the given component which yield the returned LRA value. Choices for states outside of the component are not affected.
                  */
                 virtual ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter,  ValueGetter const& actionValuesGetter, LongRunComponentType const& component) = 0;
-                
+
             protected:
-                
+
                 /*!
                  * @return true iff this is a computation on a continuous time model (i.e. CTMC, MA)
                  */
                 bool isContinuousTime() const;
-                
+
                 /*!
                  * @post _longRunComponentDecomposition points to a decomposition of the long run components (MECs, BSCCs)
                  */
                 virtual void createDecomposition() = 0;
-                
+
                 /*!
                  * @pre if scheduler production is enabled and Nondeterministic is true, a choice for each state within a component must be set such that the choices yield optimal values w.r.t. the individual components.
                  * @return Lra values for each state
                  * @post if scheduler production is enabled and Nondeterministic is true, getProducedOptimalChoices() contains choices for all input model states which yield the returned LRA values.
                  */
                 virtual std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues) = 0;
-            
+
                 storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
                 storm::storage::BitVector const* _markovianStates;
                 std::vector<ValueType> const* _exitRates;
-                
+
                 storm::storage::SparseMatrix<ValueType> const* _backwardTransitions;
                 storm::storage::Decomposition<LongRunComponentType> const* _longRunComponentDecomposition;
                 std::unique_ptr<storm::storage::SparseMatrix<ValueType>> _computedBackwardTransitions;
                 std::unique_ptr<storm::storage::Decomposition<LongRunComponentType>> _computedLongRunComponentDecomposition;
-                
+
                 boost::optional<std::vector<uint64_t>> _producedOptimalChoices;
+                boost::optional<std::vector<ValueType>> _choiceValues;
             };
 
-        
+
         }
     }
-}
+}

src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp

@@ -22,31 +22,31 @@
 namespace storm {
     namespace modelchecker {
         namespace helper {
-        
+
             template <typename ValueType>
             SparseNondeterministicInfiniteHorizonHelper<ValueType>::SparseNondeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix) : SparseInfiniteHorizonHelper<ValueType, true>(transitionMatrix) {
                 // Intentionally left empty.
             }
-            
+
             template <typename ValueType>
             SparseNondeterministicInfiniteHorizonHelper<ValueType>::SparseNondeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& markovianStates, std::vector<ValueType> const& exitRates) : SparseInfiniteHorizonHelper<ValueType, true>(transitionMatrix, markovianStates, exitRates) {
                 // Intentionally left empty.
             }
-            
+
             template <typename ValueType>
             std::vector<uint64_t> const& SparseNondeterministicInfiniteHorizonHelper<ValueType>::getProducedOptimalChoices() const {
                 STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
                 STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?");
                 return this->_producedOptimalChoices.get();
             }
-            
+
             template <typename ValueType>
             std::vector<uint64_t>& SparseNondeterministicInfiniteHorizonHelper<ValueType>::getProducedOptimalChoices() {
                 STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
                 STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?");
                 return this->_producedOptimalChoices.get();
             }
-            
+
             template <typename ValueType>
             storm::storage::Scheduler<ValueType> SparseNondeterministicInfiniteHorizonHelper<ValueType>::extractScheduler() const {
                 auto const& optimalChoices = getProducedOptimalChoices();
@@ -56,7 +56,14 @@ namespace storm {
                 }
                 return scheduler;
             }
-            
+
+            template <typename ValueType>
+            std::vector<ValueType> SparseNondeterministicInfiniteHorizonHelper<ValueType>::getChoiceValues() const {
+                STORM_LOG_ASSERT(this->isProduceChoiceValuesSet(), "Trying to get the computed choice values although this was not requested.");
+                STORM_LOG_ASSERT(this->_choiceValues.is_initialized(), "Trying to get the computed choice values but none were available. Was there a computation call before?");
+                return this->_choiceValues.get();
+            }
+
             template <typename ValueType>
             void SparseNondeterministicInfiniteHorizonHelper<ValueType>::createDecomposition() {
                 if (this->_longRunComponentDecomposition == nullptr) {
@@ -73,7 +80,7 @@ namespace storm {
             template <typename ValueType>
             ValueType SparseNondeterministicInfiniteHorizonHelper<ValueType>::computeLraForComponent(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& component) {
                 // For models with potential nondeterminisim, we compute the LRA for a maximal end component (MEC)
-                
+
                 // Allocate memory for the nondeterministic choices.
                 if (this->isProduceSchedulerSet()) {
                     if (!this->_producedOptimalChoices.is_initialized()) {
@@ -81,12 +88,19 @@ namespace storm {
                     }
                     this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
                 }
-                
+                // Allocate memory for the choice values.
+                if (this->isProduceSchedulerSet()) {
+                    if (!this->_choiceValues.is_initialized()) {
+                        this->_choiceValues.emplace();
+                    }
+                    this->_choiceValues->resize(this->_transitionMatrix.getRowCount());
+                }
+
                 auto trivialResult = this->computeLraForTrivialMec(env, stateRewardsGetter, actionRewardsGetter, component);
                 if (trivialResult.first) {
                     return trivialResult.second;
                 }
-                
+
                 // Solve nontrivial MEC with the method specified in the settings
                 storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod();
                 if ((storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact()) && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
@@ -105,10 +119,10 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
                 }
             }
-            
+
             template <typename ValueType>
             std::pair<bool, ValueType> SparseNondeterministicInfiniteHorizonHelper<ValueType>::computeLraForTrivialMec(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& component) {
-                
+
                 // If the component only consists of a single state, we compute the LRA value directly
                 if (component.size() == 1) {
                     auto const& element = *component.begin();
@@ -145,8 +159,8 @@ namespace storm {
                 }
                 return {false, storm::utility::zero<ValueType>()};
             }
-            
-    
+
+
             template <typename ValueType>
             ValueType SparseNondeterministicInfiniteHorizonHelper<ValueType>::computeLraForMecVi(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& mec) {
 
@@ -156,7 +170,11 @@ namespace storm {
                 if (this->isProduceSchedulerSet()) {
                     optimalChoices = &this->_producedOptimalChoices.get();
                 }
-                
+                std::vector<ValueType>* choiceValues = nullptr;
+                if (this->isProduceChoiceValuesSet()) {
+                    choiceValues = &this->_choiceValues.get();
+                }
+
                 // Now create a helper and perform the algorithm
                 if (this->isContinuousTime()) {
                     // We assume a Markov Automaton (with deterministic timed states and nondeterministic instant states)
@@ -187,12 +205,12 @@ namespace storm {
                 }
                 storm::expressions::Variable k = solver->addUnboundedContinuousVariable("k", storm::utility::one<ValueType>());
                 solver->update();
-                
+
                 // Add constraints.
                 for (auto const& stateChoicesPair : mec) {
                     uint_fast64_t state = stateChoicesPair.first;
                     bool stateIsMarkovian = this->_markovianStates && this->_markovianStates->get(state);
-                    
+
                     // Now create a suitable constraint for each choice
                     // x_s  {≤, ≥}  -k/rate(s) + sum_s' P(s,act,s') * x_s' + (value(s)/rate(s) + value(s,act))
                     for (auto choice : stateChoicesPair.second) {
@@ -231,12 +249,12 @@ namespace storm {
                         solver->addConstraint("s" + std::to_string(state) + "," + std::to_string(choice), constraint);
                     }
                 }
-                
+
                 solver->optimize();
                 STORM_LOG_THROW(!this->isProduceSchedulerSet(), storm::exceptions::NotImplementedException, "Scheduler extraction is not yet implemented for LP based LRA method.");
                 return solver->getContinuousValue(k);
             }
-            
+
             /*!
              * Auxiliary function that adds the entries of the Ssp Matrix for a single choice (i.e., row)
              * Transitions that lead to a Component state will be redirected to a new auxiliary state (there is one aux. state for each component).
@@ -244,10 +262,10 @@ namespace storm {
              */
             template <typename ValueType>
             void addSspMatrixChoice(uint64_t const& inputMatrixChoice, storm::storage::SparseMatrix<ValueType> const& inputTransitionMatrix, std::vector<uint64_t> const& inputToSspStateMap, uint64_t const& numberOfNonComponentStates, uint64_t const& currentSspChoice, storm::storage::SparseMatrixBuilder<ValueType>& sspMatrixBuilder) {
-            
+
                 // As there could be multiple transitions to the same MEC, we accumulate them in this map before adding them to the matrix builder.
                 std::map<uint64_t, ValueType> auxiliaryStateToProbabilityMap;
-                
+
                 for (auto const& transition : inputTransitionMatrix.getRow(inputMatrixChoice)) {
                     if (!storm::utility::isZero(transition.getValue())) {
                         auto const& sspTransitionTarget = inputToSspStateMap[transition.getColumn()];
@@ -268,18 +286,18 @@ namespace storm {
                         }
                     }
                 }
-                
+
                 // Now insert all (cumulative) probability values that target a component.
                 for (auto const& componentToProbEntry : auxiliaryStateToProbabilityMap) {
                     sspMatrixBuilder.addNextValue(currentSspChoice, componentToProbEntry.first, componentToProbEntry.second);
                 }
             }
-            
+
             template <typename ValueType>
             std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> SparseNondeterministicInfiniteHorizonHelper<ValueType>::buildSspMatrixVector(std::vector<ValueType> const& mecLraValues, std::vector<uint64_t> const& inputToSspStateMap, storm::storage::BitVector const& statesNotInComponent, uint64_t numberOfNonComponentStates, std::vector<std::pair<uint64_t, uint64_t>>* sspComponentExitChoicesToOriginalMap) {
-                
+
                 auto const& choiceIndices = this->_transitionMatrix.getRowGroupIndices();
-                
+
                 std::vector<ValueType> rhs;
                 uint64_t numberOfSspStates = numberOfNonComponentStates + this->_longRunComponentDecomposition->size();
                 storm::storage::SparseMatrixBuilder<ValueType> sspMatrixBuilder(0, numberOfSspStates , 0, true, true, numberOfSspStates);
@@ -323,7 +341,7 @@ namespace storm {
                 }
                 return std::make_pair(sspMatrixBuilder.build(currentSspChoice, numberOfSspStates, numberOfSspStates), std::move(rhs));
             }
-            
+
             template <typename ValueType>
             void SparseNondeterministicInfiniteHorizonHelper<ValueType>::constructOptimalChoices(std::vector<uint64_t> const& sspChoices, storm::storage::SparseMatrix<ValueType> const& sspMatrix, std::vector<uint64_t> const& inputToSspStateMap, storm::storage::BitVector const& statesNotInComponent, uint64_t numberOfNonComponentStates, std::vector<std::pair<uint64_t, uint64_t>> const& sspComponentExitChoicesToOriginalMap) {
                 // We first take care of non-mec states
@@ -398,11 +416,11 @@ namespace storm {
             template <typename ValueType>
             std::vector<ValueType> SparseNondeterministicInfiniteHorizonHelper<ValueType>::buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& componentLraValues) {
                 STORM_LOG_ASSERT(this->_longRunComponentDecomposition != nullptr, "Decomposition not computed, yet.");
-                
+
                 // For fast transition rewriting, we build a mapping from the input state indices to the state indices of a new transition matrix
                 // which redirects all transitions leading to a former component state to a new auxiliary state.
                 // There will be one auxiliary state for each component. These states will be appended to the end of the matrix.
-                
+
                 // First gather the states that are part of a component
                 // and create a mapping from states that lie in a component to the corresponding component index.
                 storm::storage::BitVector statesInComponents(this->_transitionMatrix.getRowGroupCount());
@@ -427,14 +445,14 @@ namespace storm {
                 for (auto mecState : statesInComponents) {
                     inputToSspStateMap[mecState] += numberOfNonComponentStates;
                 }
-                
+
                 // For scheduler extraction, we will need to create a mapping between choices at the auxiliary states and the
                 // corresponding choices in the original model.
                 std::vector<std::pair<uint_fast64_t, uint_fast64_t>> sspComponentExitChoicesToOriginalMap;
-                
+
                 // The next step is to create the SSP matrix and the right-hand side of the SSP.
                 auto sspMatrixVector = buildSspMatrixVector(componentLraValues, inputToSspStateMap, statesNotInComponent, numberOfNonComponentStates, this->isProduceSchedulerSet() ? &sspComponentExitChoicesToOriginalMap : nullptr);
-                
+
                 // Set-up a solver
                 storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
                 storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, true, this->getOptimizationDirection(), false, this->isProduceSchedulerSet());
@@ -448,7 +466,7 @@ namespace storm {
                 solver->setLowerBound(*lowerUpperBounds.first);
                 solver->setUpperBound(*lowerUpperBounds.second);
                 solver->setRequirementsChecked();
-                
+
                 // Solve the equation system
                 std::vector<ValueType> x(sspMatrixVector.first.getRowGroupCount());
                 solver->solveEquations(env, this->getOptimizationDirection(), x, sspMatrixVector.second);
@@ -460,7 +478,7 @@ namespace storm {
                 } else {
                     STORM_LOG_ERROR_COND(!this->isProduceSchedulerSet(), "Requested to produce a scheduler, but no scheduler was generated.");
                 }
-                
+
                 // Prepare result vector.
                 // For efficiency reasons, we re-use the memory of our rhs for this!
                 std::vector<ValueType> result = std::move(sspMatrixVector.second);
@@ -469,10 +487,10 @@ namespace storm {
                 storm::utility::vector::selectVectorValues(result, inputToSspStateMap, x);
                 return result;
             }
-            
+
             template class SparseNondeterministicInfiniteHorizonHelper<double>;
             template class SparseNondeterministicInfiniteHorizonHelper<storm::RationalNumber>;
-            
+
         }
     }
-}
+}

src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h

@@ -3,14 +3,14 @@
 
 
 namespace storm {
-    
+
     namespace storage {
         template <typename VT> class Scheduler;
     }
-    
+
     namespace modelchecker {
         namespace helper {
-        
+
             /*!
              * Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system.
              * @tparam ValueType the type a value can have
@@ -23,35 +23,40 @@ namespace storm {
                  * Function mapping from indices to values
                  */
                 typedef typename SparseInfiniteHorizonHelper<ValueType, true>::ValueGetter ValueGetter;
-                
+
                 /*!
                  * Initializes the helper for a discrete time model (i.e. MDP)
                  */
                 SparseNondeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
-                
+
                 /*!
                  * Initializes the helper for a continuous time model (i.e. MA)
                  */
                 SparseNondeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& markovianStates, std::vector<ValueType> const& exitRates);
-                
+
                 /*!
                  * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
                  * @return the produced scheduler of the most recent call.
                  */
                 std::vector<uint64_t> const& getProducedOptimalChoices() const;
-                
+
                 /*!
                  * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
                  * @return the produced scheduler of the most recent call.
                  */
                 std::vector<uint64_t>& getProducedOptimalChoices();
-                
+
                 /*!
                  * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
                  * @return a new scheduler containing optimal choices for each state that yield the long run average values of the most recent call.
                  */
                 storm::storage::Scheduler<ValueType> extractScheduler() const;
 
+                /*!
+                 * @return the computed choice values for the states.
+                 */
+                std::vector<ValueType> getChoiceValues() const;
+
                 /*!
                  * @param stateValuesGetter a function returning a value for a given state index
                  * @param actionValuesGetter a function returning a value for a given (global) choice index
@@ -59,43 +64,43 @@ namespace storm {
                  * @post if scheduler production is enabled and Nondeterministic is true, getProducedOptimalChoices() contains choices for the states of the given component which yield the returned LRA value. Choices for states outside of the component are not affected.
                  */
                 virtual ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter,  ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& component) override;
-                
+
             protected:
-                
+
                 virtual void createDecomposition() override;
-                
+
                 std::pair<bool, ValueType> computeLraForTrivialMec(Environment const& env, ValueGetter const& stateValuesGetter,  ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& mec);
-                
+
                 /*!
                  * As computeLraForMec but uses value iteration as a solution method (independent of what is set in env)
                  */
                 ValueType computeLraForMecVi(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& mec);
-                
+
                 /*!
                  * As computeLraForMec but uses linear programming as a solution method (independent of what is set in env)
                  * @see Guck et al.: Modelling and Analysis of Markov Reward Automata (ATVA'14), https://doi.org/10.1007/978-3-319-11936-6_13
                  */
                 ValueType computeLraForMecLp(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent  const& mec);
-                
+
                 std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> buildSspMatrixVector(std::vector<ValueType> const& mecLraValues, std::vector<uint64_t> const& inputToSspStateMap, storm::storage::BitVector const& statesNotInComponent, uint64_t numberOfNonComponentStates, std::vector<std::pair<uint64_t, uint64_t>>* sspComponentExitChoicesToOriginalMap);
-                
+
                 /*!
                  * @pre a choice for each state within a component must be set such that the choices yield optimal values w.r.t. the individual components.
                  * Translates optimal choices for MECS and SSP to the original model.
                  * @post getProducedOptimalChoices() contains choices for all input model states which yield the returned LRA values.
                  */
                 void constructOptimalChoices(std::vector<uint64_t> const& sspChoices, storm::storage::SparseMatrix<ValueType> const& sspMatrix, std::vector<uint64_t> const& inputToSspStateMap, storm::storage::BitVector const& statesNotInComponent, uint64_t numberOfNonComponentStates, std::vector<std::pair<uint64_t, uint64_t>> const& sspComponentExitChoicesToOriginalMap);
-                
+
                 /*!
                  * @pre if scheduler production is enabled a choice for each state within a component must be set such that the choices yield optimal values w.r.t. the individual components.
                  * @return Lra values for each state
                  * @post if scheduler production is enabled getProducedOptimalChoices() contains choices for all input model states which yield the returned LRA values.
                  */
                 virtual std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues) override;
-            
+
             };
 
-        
+
         }
     }
-}
+}

src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h

@@ -5,7 +5,7 @@
 namespace storm {
     namespace modelchecker {
         namespace helper {
-            
+
             /*!
              * Forwards relevant information stored in the given CheckTask to the given helper
              */
@@ -26,10 +26,13 @@ namespace storm {
                 // Scheduler Production
 			    helper.setProduceScheduler(checkTask.isProduceSchedulersSet());
 
+                // Shield Synthesis
+			    helper.setProduceChoiceValues(checkTask.isShieldingTask());
+
                 // Qualitative flag
                 helper.setQualitative(checkTask.isQualitativeSet());
             }
-            
+
             /*!
              * Forwards relevant information stored in the given CheckTask to the given helper
              */
@@ -50,4 +53,4 @@ namespace storm {
             }
         }
     }
-}
+}

src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp

@@ -50,7 +50,7 @@ namespace storm {
                             _multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues);
                             auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices();
                             rowGroupIndices.erase(rowGroupIndices.begin());
-                            _multiplier->reduce(env, dir, constrainedChoiceValues, rowGroupIndices, xNew());
+                            _multiplier->reduce(env, dir, rowGroupIndices, constrainedChoiceValues, xNew(), nullptr, &_statesOfCoalition);
                             break;
                         }
                         performIterationStep(env, dir);
@@ -125,6 +125,16 @@ namespace storm {
                     return _produceScheduler;
                 }
 
+                template <typename ValueType>
+                void GameViHelper<ValueType>::setShieldingTask(bool value) {
+                    _shieldingTask = value;
+                }
+
+                template <typename ValueType>
+                bool GameViHelper<ValueType>::isShieldingTask() const {
+                    return _shieldingTask;
+                }
+
                 template <typename ValueType>
                 void GameViHelper<ValueType>::updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix) {
                     _transitionMatrix = newTransitionMatrix;

src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h

@@ -38,6 +38,16 @@ namespace storm {
                      */
                     bool isProduceSchedulerSet() const;
 
+                    /*!
+                     * Sets whether an optimal scheduler shall be constructed during the computation
+                     */
+                    void setShieldingTask(bool value);
+
+                    /*!
+                     * @return whether an optimal scheduler shall be constructed during the computation
+                     */
+                    bool isShieldingTask() const;
+
                     /*!
                      * Changes the transitionMatrix to the given one.
                      */
@@ -93,6 +103,7 @@ namespace storm {
                     std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
 
                     bool _produceScheduler = false;
+                    bool _shieldingTask = false;
                     boost::optional<std::vector<uint64_t>> _producedOptimalChoices;
                 };
             }