Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExplicitParetoCurveCheckResult.h
Go to the documentation of this file.
1#pragma once
2
3#include <vector>
4
8
9namespace storm {
10namespace modelchecker {
11template<typename ValueType>
13 public:
18 ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type> const& points,
19 polytope_type const& underApproximation = nullptr, polytope_type const& overApproximation = nullptr);
20 ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type>&& points,
22 ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type>&& points, std::vector<scheduler_type>&& schedulers,
24
30
31 virtual std::unique_ptr<CheckResult> clone() const override;
32
33 virtual bool isExplicitParetoCurveCheckResult() const override;
34 virtual bool isExplicit() const override;
35
36 virtual void filter(QualitativeCheckResult const& filter) override;
37
39
40 virtual bool hasScheduler() const override;
41
42 std::vector<scheduler_type> const& getSchedulers() const;
43 std::vector<scheduler_type>& getSchedulers();
44
45 private:
46 // The state of the checked model to which the result applies
48 // The corresponding strategies to reach each point in the pareto curve
49 std::vector<scheduler_type> schedulers;
50};
51} // namespace modelchecker
52} // namespace storm
ExplicitParetoCurveCheckResult(ExplicitParetoCurveCheckResult const &other)=default
ExplicitParetoCurveCheckResult(ExplicitParetoCurveCheckResult &&other)=default
storm::storage::sparse::state_type const & getState() const
typename ParetoCurveCheckResult< ValueType >::point_type point_type
ExplicitParetoCurveCheckResult & operator=(ExplicitParetoCurveCheckResult const &other)=default
typename ParetoCurveCheckResult< ValueType >::polytope_type polytope_type
virtual void filter(QualitativeCheckResult const &filter) override
Filters the current result wrt.
ExplicitParetoCurveCheckResult & operator=(ExplicitParetoCurveCheckResult &&other)=default
virtual std::unique_ptr< CheckResult > clone() const override
std::vector< scheduler_type > const & getSchedulers() const
std::shared_ptr< storm::storage::geometry::Polytope< ValueType > > polytope_type
This class defines which action is chosen in a particular state of a non-deterministic model.
Definition Scheduler.h:18
LabParser.cpp.