DeterministicSchedsParetoExplorer.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <queue>
 
#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h"
#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h"
#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
 
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/solver/SmtSolver.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/geometry/Halfspace.h"
#include "storm/storage/geometry/Polytope.h"
 
namespace storm {
 
class Environment;
 
namespace modelchecker {
namespace multiobjective {

template<class SparseModelType, typename GeometryValueType>
class DeterministicSchedsParetoExplorer {
   public:
    typedef uint64_t PointId;
    typedef typename std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> Polytope;
    typedef typename SparseModelType::ValueType ModelValueType;
 
    class Point {
       public:
        Point(std::vector<GeometryValueType> const& coordinates);
        Point(std::vector<GeometryValueType>&& coordinates);
 
        std::vector<GeometryValueType> const& get() const;
        std::vector<GeometryValueType>& get();
 
        uint64_t dimension() const;
 
        enum class DominanceResult { Incomparable, Dominates, Dominated, Equal };
        DominanceResult getDominance(Point const& other) const;
 
        void setOnFacet(bool value = true);
        bool liesOnFacet() const;
        void setParetoOptimal(bool value = true);
        bool isParetoOptimal() const;
 
        std::string toString(bool convertToDouble = false) const;
 
       private:
        std::vector<GeometryValueType> coordinates;
        bool onFacet;
        bool paretoOptimal;
    };
 
    class Pointset {
       public:
        typedef typename std::map<PointId, Point>::const_iterator iterator_type;
 
        Pointset();

        boost::optional<PointId> addPoint(Environment const& env, Point&& point);

        Point const& getPoint(PointId const& id) const;
 
        iterator_type begin() const;
        iterator_type end() const;

        uint64_t size() const;

        Polytope downwardClosure() const;
 
        void collectPointsInPolytope(std::set<PointId>& collectedPoints, Polytope const& polytope);
 
        void printToStream(std::ostream& out, bool includeIDs = true, bool convertToDouble = false);
 
       private:
        std::map<PointId, Point> points;
        PointId currId;
    };
 
    class Facet {
       public:
        Facet(storm::storage::geometry::Halfspace<GeometryValueType> const& halfspace);
        Facet(storm::storage::geometry::Halfspace<GeometryValueType>&& halfspace);
        storm::storage::geometry::Halfspace<GeometryValueType> const& getHalfspace() const;
        void addPoint(PointId const& pointId, Point const& point);
        std::vector<PointId> const& getPoints() const;
        uint64_t getNumberOfPoints() const;

        Polytope getInducedPolytope(Pointset const& pointset, std::vector<GeometryValueType> const& referenceCoordinates);
 
       private:
        storm::storage::geometry::Halfspace<GeometryValueType> halfspace;
        std::vector<PointId> pointsOnFacet;
    };
 
    DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
 
    virtual std::unique_ptr<CheckResult> check(Environment const& env);
 
    void exportPlotOfCurrentApproximation(Environment const& env);
 
   private:
    void clean();

    void addHalfspaceToOverApproximation(Environment const& env, std::vector<GeometryValueType> const& normalVector, GeometryValueType const& offset);

    void addUnachievableArea(Environment const& env, Polytope const& area);

    void initializeFacets(Environment const& env);

    std::vector<GeometryValueType> getReferenceCoordinates(Environment const& env) const;

    void processFacet(Environment const& env, Facet& f);

    bool optimizeAndSplitFacet(Environment const& env, Facet& f);
 
    Polytope negateMinObjectives(Polytope const& polytope) const;
    void negateMinObjectives(std::vector<GeometryValueType>& vector) const;
 
    Pointset pointset;
    std::queue<Facet> unprocessedFacets;
    Polytope overApproximation;
    std::vector<Polytope> unachievableAreas;
    std::vector<GeometryValueType> eps;
    std::shared_ptr<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>> lpChecker;
    std::unique_ptr<PcaaWeightVectorChecker<SparseModelType>> wvChecker;
    std::vector<DeterministicSchedsObjectiveHelper<SparseModelType>> objectiveHelper;
 
    std::shared_ptr<SparseModelType> const& model;
    uint64_t originalModelInitialState;
    std::vector<Objective<ModelValueType>> const& objectives;
};
 
}  // namespace multiobjective
}  // namespace modelchecker
}  // namespace storm