SparseMultiObjectiveRewardAnalysis.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <string>
 
#include "storm/logic/Formulas.h"
#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
 
namespace storm {
 
namespace modelchecker {
namespace multiobjective {
namespace preprocessing {
 
enum class RewardFinitenessType {
    AllFinite,           // The expected reward is finite for all objectives and all schedulers
    ExistsParetoFinite,  // There is a Pareto optimal scheduler yielding finite rewards for all objectives
    Infinite             // All Pareto optimal schedulers yield infinite reward for at least one objective
};
 
/*
 * This class performs some analysis task regarding the occurring expected reward objectives
 */
template<class SparseModelType>
class SparseMultiObjectiveRewardAnalysis {
   public:
    typedef typename SparseModelType::ValueType ValueType;
    typedef typename SparseModelType::RewardModelType RewardModelType;
 
    struct ReturnType {
        RewardFinitenessType rewardFinitenessType;
 
        // The states of the preprocessed model for which...
        storm::storage::BitVector totalReward0EStates;  // ... there is a scheduler such that all expected total reward objectives have value zero
        storm::storage::BitVector reward0AStates;       // ... all schedulers induce value 0 for all reward-based objectives
        boost::optional<storm::storage::BitVector>
            totalRewardLessInfinityEStates;  // ... there is a scheduler yielding finite reward for all expected total reward objectives
    };
 
    static ReturnType analyze(
        storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
 
    static void computeUpperResultBound(SparseModelType const& model, storm::modelchecker::multiobjective::Objective<ValueType>& objective,
                                        storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
 
   private:
    static void setReward0States(
        ReturnType& result,
        storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult,
        storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
 
    static void checkRewardFiniteness(
        ReturnType& result,
        storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult,
        storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
};
 
}  // namespace preprocessing
}  // namespace multiobjective
}  // namespace modelchecker
}  // namespace storm