SparsePcaaQuery.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <optional>
#include <variant>
#include <vector>
 
#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/storage/geometry/Polytope.h"
 
namespace storm {
 
class Environment;
 
namespace modelchecker::multiobjective {
 
/*
 * This class represents a query for the Pareto curve approximation algorithm (Pcaa).
 * It implements the necessary computations for the different query types.
 * @See Section 3.4 of https://doi.org/10.18154/RWTH-2023-09669
 */
template<class SparseModelType, typename GeometryValueType>
class SparsePcaaQuery {
   public:
    using Point = std::vector<GeometryValueType>;
    using WeightVector = std::vector<GeometryValueType>;
    using Polytope = storm::storage::geometry::Polytope<GeometryValueType>;
    using Halfspace = storm::storage::geometry::Halfspace<GeometryValueType>;
    using PolytopePtr = std::shared_ptr<Polytope>;
    using PreprocessorResult = preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>;
    using ModelValueType = typename SparseModelType::ValueType;
 
    SparsePcaaQuery(PreprocessorResult& preprocessorResult);
 
    std::unique_ptr<CheckResult> check(Environment const& env, bool produceScheduler);
 
   private:
    struct RefinementStep {
        WeightVector weightVector;
        Point achievablePoint;
        GeometryValueType optimalWeightedSum;
        std::optional<storm::storage::Scheduler<ModelValueType>> scheduler;
    };
 
    struct WeightedSumOptimizationInput {
        WeightVector weightVector;
        GeometryValueType epsilonWso;
    };
    using AnswerOrWeights = std::variant<std::unique_ptr<CheckResult>, WeightedSumOptimizationInput>;
    AnswerOrWeights tryAnswerOrNextWeights(Environment const& env, std::vector<RefinementStep> const& refinementSteps, PolytopePtr overApproximation,
                                           bool produceScheduler);
    AnswerOrWeights tryAnswerOrNextWeightsAchievability(Environment const& env, std::optional<uint64_t> const optObjIndex,
                                                        std::vector<GeometryValueType> const& thresholds, std::vector<RefinementStep> const& refinementSteps,
                                                        PolytopePtr overApproximation, bool produceScheduler);
    AnswerOrWeights tryAnswerOrNextWeightsPareto(Environment const& env, std::vector<RefinementStep> const& refinementSteps, PolytopePtr overApproximation,
                                                 bool produceScheduler);
 
    GeometryValueType getEpsilonWso(Environment const& env, std::optional<GeometryValueType> approxDistance = std::nullopt);
 
    void exportPlotOfCurrentApproximation(Environment const& env, std::vector<RefinementStep> const& refinementSteps, PolytopePtr overApproximation) const;
 
    uint64_t const initialStateOfOriginalModel;  // needed to prepare the CheckResult.
    std::vector<Objective<ModelValueType>> objectives;
 
    // The corresponding weight vector checker
    std::unique_ptr<PcaaWeightVectorChecker<SparseModelType>> weightVectorChecker;
};
 
}  // namespace modelchecker::multiobjective
}  // namespace storm