Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparsePcaaQuery.h
Go to the documentation of this file.
1#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAQUERY_H_
2#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAQUERY_H_
3
8
9namespace storm {
10
11class Environment;
12
13namespace modelchecker {
14namespace multiobjective {
15
16/*
17 * This class represents a query for the Pareto curve approximation algorithm (Pcaa).
18 * It implements the necessary computations for the different query types.
19 */
20template<class SparseModelType, typename GeometryValueType>
22 public:
23 // Typedefs for simple geometric objects
24 typedef std::vector<GeometryValueType> Point;
25 typedef std::vector<GeometryValueType> WeightVector;
26
27 virtual ~SparsePcaaQuery();
28
29 /*
30 * Invokes the computation and retrieves the result
31 */
32 virtual std::unique_ptr<CheckResult> check(Environment const& env, bool produceScheduler) = 0;
33
34 /*
35 * Exports the current approximations and the currently processed points into respective .csv files located at the given directory.
36 * The polytopes are represented as the set of vertices.
37 * Note that the approximations will be intersected with a (sufficiently large) hyperrectangle in order to ensure that the polytopes are bounded
38 * This only works for 2 dimensional queries.
39 */
40 void exportPlotOfCurrentApproximation(Environment const& env) const;
41
42 protected:
43 /*
44 * Represents the information obtained in a single iteration of the algorithm
45 */
50 std::optional<storm::storage::Scheduler<typename SparseModelType::ValueType>> scheduler;
51 };
52
53 /*
54 * Creates a new query for the Pareto curve approximation algorithm (Pcaa)
55 * @param preprocessorResult the result from preprocessing
56 */
58
59 /*
60 * Returns a weight vector w that separates the under approximation from the given point p, i.e.,
61 * For each x in the under approximation, it holds that w*x <= w*p
62 *
63 * @param pointToBeSeparated the point that is to be seperated
64 */
65 WeightVector findSeparatingVector(Point const& pointToBeSeparated);
66
67 /*
68 * Refines the current result w.r.t. the given direction vector.
69 */
70 void performRefinementStep(Environment const& env, WeightVector&& direction, bool produceScheduler);
71
72 /*
73 * Updates the overapproximation after a refinement step has been performed
74 *
75 * @note The last entry of this->refinementSteps should be the newest step whose information is not yet included in the approximation.
76 */
78
79 /*
80 * Updates the underapproximation after a refinement step has been performed
81 *
82 * @note The last entry of this->refinementSteps should be the newest step whose information is not yet included in the approximation.
83 */
85
86 /*
87 * Returns true iff the maximum number of refinement steps (as possibly specified in the settings) has been reached
88 */
89 bool maxStepsPerformed(Environment const& env) const;
90
91 SparseModelType const& originalModel;
93
94 std::vector<Objective<typename SparseModelType::ValueType>> objectives;
95
96 // The corresponding weight vector checker
97 std::unique_ptr<PcaaWeightVectorChecker<SparseModelType>> weightVectorChecker;
98
99 // The results in each iteration of the algorithm
100 std::vector<RefinementStep> refinementSteps;
101 // Overapproximation of the set of achievable values
102 std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> overApproximation;
103 // Underapproximation of the set of achievable values
104 std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> underApproximation;
105
106 // stores for each objective whether it still makes sense to check for this objective individually (i.e., with weight vector given by w_{i}>0 iff i=objIndex
107 // )
109};
110
111} // namespace multiobjective
112} // namespace modelchecker
113} // namespace storm
114
115#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAQUERY_H_ */
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
void performRefinementStep(Environment const &env, WeightVector &&direction, bool produceScheduler)
std::shared_ptr< storm::storage::geometry::Polytope< GeometryValueType > > underApproximation
void exportPlotOfCurrentApproximation(Environment const &env) const
storm::logic::MultiObjectiveFormula const & originalFormula
std::vector< Objective< typename SparseModelType::ValueType > > objectives
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
LabParser.cpp.
std::optional< storm::storage::Scheduler< typename SparseModelType::ValueType > > scheduler