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> const& weightVector) = 0;
 
    virtual std::vector<ValueType> getUnderApproximationOfInitialStateResults() const = 0;
    virtual std::vector<ValueType> getOverApproximationOfInitialStateResults() const = 0;
 
    void setWeightedPrecision(ValueType const& value);
 
    ValueType const& getWeightedPrecision() const;
 
    virtual storm::storage::Scheduler<ValueType> computeScheduler() 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;
    // The precision of this weight vector checker.
    ValueType weightedPrecision;
};
 
template<typename ModelType>
class WeightVectorCheckerFactory {
   public:
    template<typename VT = typename ModelType::ValueType,
             typename std::enable_if<std::is_same<ModelType, storm::models::sparse::Mdp<VT>>::value, int>::type = 0>
    static std::unique_ptr<PcaaWeightVectorChecker<ModelType>> create(
        preprocessing::SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult);
 
    template<typename VT = typename ModelType::ValueType,
             typename std::enable_if<std::is_same<ModelType, storm::models::sparse::MarkovAutomaton<VT>>::value, int>::type = 0>
    static std::unique_ptr<PcaaWeightVectorChecker<ModelType>> create(
        preprocessing::SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult);
};
 
}  // namespace multiobjective
}  // namespace modelchecker
}  // namespace storm