DeterministicSchedsObjectiveHelper.h

Go to the documentation of this file.

#pragma once
 
#include <map>
#include <optional>
 
#include "storm/modelchecker/multiobjective/Objective.h"
#include "storm/storage/BitVector.h"
 
namespace storm {
 
namespace storage {
template<typename ValueType>
class MaximalEndComponentDecomposition;
}
 
class Environment;
 
namespace modelchecker::multiobjective {
 
template<typename ModelType>
class DeterministicSchedsObjectiveHelper {
   public:
    typedef typename ModelType::ValueType ValueType;
    DeterministicSchedsObjectiveHelper(ModelType const& model, Objective<ValueType> const& objective);
 
    bool hasConstantInitialStateValue() const;
 
    ValueType getConstantInitialStateValue() const;
 
    storm::storage::BitVector const& getMaybeStates() const;
 
    storm::storage::BitVector const& getRewMinusInfEStates() const;
 
    std::map<uint64_t, ValueType> const& getChoiceRewards() const;
 
    storm::storage::BitVector const& getRelevantZeroRewardChoices() const;
 
    ValueType const& getUpperValueBoundAtState(uint64_t state) const;
    ValueType const& getLowerValueBoundAtState(uint64_t state) const;
 
    enum class InfinityCase { AlwaysFinite, HasPositiveInfinite, HasNegativeInfinite };
 
    InfinityCase const& getInfinityCase() const;
 
    bool minimizing() const;
 
    void computeLowerUpperBounds(Environment const& env) const;
 
    bool isTotalRewardObjective() const;
 
    bool hasThreshold() const;
 
    ValueType getThreshold() const;
 
    ValueType evaluateScheduler(Environment const& env, storm::storage::BitVector const& selectedChoices) const;
 
   private:
    void initialize();
 
    storm::storage::BitVector maybeStates;         // S_?^j
    storm::storage::BitVector rewMinusInfEStates;  // S_{-infty}^j
    std::optional<ValueType> constantInitialStateValue;
    storm::storage::BitVector relevantZeroRewardChoices;
    std::map<uint64_t, ValueType> choiceRewards;
    InfinityCase infinityCase;
 
    // Computed on demand:
    mutable std::optional<std::vector<ValueType>> lowerResultBounds;
    mutable std::optional<std::vector<ValueType>> upperResultBounds;
 
    ModelType const& model;
    Objective<ValueType> const& objective;
};
}  // namespace modelchecker::multiobjective
}  // namespace storm