DeterministicSchedsLpChecker.h

Go to the documentation of this file.

#pragma once
 
#include <optional>
#include <vector>
 
#include "storm/modelchecker/multiobjective/Objective.h"
#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h"
#include "storm/solver/LpSolver.h"
#include "storm/storage/geometry/Polytope.h"
#include "storm/storage/geometry/PolytopeTree.h"
#include "storm/utility/Stopwatch.h"
 
namespace storm {
 
class Environment;
 
namespace modelchecker {
namespace multiobjective {
 
template<typename ModelType, typename GeometryValueType>
class DeterministicSchedsLpChecker {
   public:
    typedef typename ModelType::ValueType ValueType;
    typedef typename std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> Polytope;
    typedef typename std::vector<GeometryValueType> Point;
 
    DeterministicSchedsLpChecker(ModelType const& model, std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper);
 
    void setCurrentWeightVector(Environment const& env, std::vector<GeometryValueType> const& weightVector);
 
    std::optional<std::pair<Point, GeometryValueType>> check(storm::Environment const& env, Polytope overapproximation, Point const& eps = {});
 
    std::pair<std::vector<Point>, std::vector<Polytope>> check(storm::Environment const& env,
                                                               storm::storage::geometry::PolytopeTree<GeometryValueType>& polytopeTree, Point const& eps);
 
    std::string getStatistics(std::string const& prefix = "") const;
 
   private:
    void initialize(Environment const& env);
 
    void initializeLpModel(Environment const& env);
 
    // Builds the induced markov chain of the current model and checks whether the resulting value coincide with the result of the lp solver.
    Point validateCurrentModel(Environment const& env) const;
 
    void checkRecursive(storm::Environment const& env, storm::storage::geometry::PolytopeTree<GeometryValueType>& polytopeTree, Point const& eps,
                        std::vector<Point>& foundPoints, std::vector<Polytope>& infeasableAreas, uint64_t const& depth);
 
    ModelType const& model;
    std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper;
 
    std::unique_ptr<storm::solver::LpSolver<ValueType>> lpModel;
    std::vector<storm::expressions::Expression> choiceVariables;
    std::vector<storm::expressions::Expression> initialStateResults;
    std::vector<storm::expressions::Variable> currentObjectiveVariables;
    std::vector<GeometryValueType> currentWeightVector;
    bool flowEncoding;
 
    storm::utility::Stopwatch swAll;
    storm::utility::Stopwatch swInit;
    storm::utility::Stopwatch swCheckWeightVectors;
    storm::utility::Stopwatch swCheckAreas;
    storm::utility::Stopwatch swValidate;
    uint64_t numLpQueries;
};
 
}  // namespace multiobjective
}  // namespace modelchecker
}  // namespace storm