PcaaWeightVectorChecker.h

Go to the documentation of this file.

#pragma once
 
#include <vector>
 
#include "storm/modelchecker/multiobjective/Objective.h"
#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/storage/Scheduler.h"
 
namespace storm {
 
class Environment;
 
namespace modelchecker {
namespace multiobjective {
 
template<typename ModelType>
class PcaaWeightVectorChecker {
   public:
    typedef typename ModelType::ValueType ValueType;
 
    /*
     * Creates a weight vector checker.
     *
     * @param objectives The (preprocessed) objectives
     *
     */
 
    PcaaWeightVectorChecker(std::vector<Objective<ValueType>> const& objectives);
 
    virtual ~PcaaWeightVectorChecker() = default;
 
    virtual void check(Environment const& env, std::vector<ValueType> weightVector) = 0;
 
    virtual std::vector<ValueType> getAchievablePoint() const = 0;
 
    virtual ValueType getOptimalWeightedSum() const = 0;
 
    virtual storm::storage::Scheduler<ValueType> computeScheduler() const;
 
    void setWeightedPrecision(ValueType const& value);
 
    ValueType const& getWeightedPrecision() const;
 
    virtual bool smallPrecisionsAreChallenging() const;
 
   protected:
    boost::optional<ValueType> computeWeightedResultBound(bool lower, std::vector<ValueType> const& weightVector,
                                                          storm::storage::BitVector const& objectiveFilter) const;
 
    // The (preprocessed) objectives
    std::vector<Objective<ValueType>> objectives;
 
   private:
    // The precision of this weight vector checker.
    std::optional<ValueType> weightedPrecision;
};
 
template<typename ModelType>
std::unique_ptr<PcaaWeightVectorChecker<ModelType>> createWeightVectorChecker(
    preprocessing::SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult);
 
}  // namespace multiobjective
}  // namespace modelchecker
}  // namespace storm