1#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAQUERY_H_
2#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAQUERY_H_
13namespace modelchecker {
14namespace multiobjective {
20template<
class SparseModelType,
typename GeometryValueType>
24 typedef std::vector<GeometryValueType>
Point;
32 virtual std::unique_ptr<CheckResult>
check(
Environment const& env,
bool produceScheduler) = 0;
50 std::optional<storm::storage::Scheduler<typename SparseModelType::ValueType>>
scheduler;
94 std::vector<Objective<typename SparseModelType::ValueType>>
objectives;
SparseModelType const & originalModel
std::vector< RefinementStep > refinementSteps
void updateUnderApproximation()
std::shared_ptr< storm::storage::geometry::Polytope< GeometryValueType > > overApproximation
WeightVector findSeparatingVector(Point const &pointToBeSeparated)
virtual std::unique_ptr< CheckResult > check(Environment const &env, bool produceScheduler)=0
std::unique_ptr< PcaaWeightVectorChecker< SparseModelType > > weightVectorChecker
bool maxStepsPerformed(Environment const &env) const
virtual ~SparsePcaaQuery()
storm::storage::BitVector diracWeightVectorsToBeChecked
std::vector< GeometryValueType > WeightVector
void performRefinementStep(Environment const &env, WeightVector &&direction, bool produceScheduler)
std::shared_ptr< storm::storage::geometry::Polytope< GeometryValueType > > underApproximation
void updateOverApproximation()
void exportPlotOfCurrentApproximation(Environment const &env) const
storm::logic::MultiObjectiveFormula const & originalFormula
std::vector< Objective< typename SparseModelType::ValueType > > objectives
std::vector< GeometryValueType > Point
A bit vector that is internally represented as a vector of 64-bit values.
std::optional< storm::storage::Scheduler< typename SparseModelType::ValueType > > scheduler
WeightVector weightVector