Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExplicitQuantitativeCheckResult.h
Go to the documentation of this file.
1#pragma once
2#include <boost/optional.hpp>
3#include <boost/variant.hpp>
4#include <map>
5#include <optional>
6#include <vector>
7
14
15namespace storm {
16
17namespace modelchecker {
18// Forward declaration
19class ExplicitQualitativeCheckResult;
20
21template<typename ValueType>
23 public:
24 typedef std::vector<ValueType> vector_type;
25 typedef std::map<storm::storage::sparse::state_type, ValueType> map_type;
26
30 ExplicitQuantitativeCheckResult(storm::storage::sparse::state_type const& state, ValueType const& value);
33 ExplicitQuantitativeCheckResult(boost::variant<vector_type, map_type> const& values,
34 boost::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler = boost::none);
35 ExplicitQuantitativeCheckResult(boost::variant<vector_type, map_type>&& values,
36 boost::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler = boost::none);
37
43
45
46 virtual std::unique_ptr<CheckResult> clone() const override;
47
49 ValueType const& operator[](storm::storage::sparse::state_type state) const;
50
51 virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override;
52
53 virtual bool isExplicit() const override;
54 virtual bool isResultForAllStates() const override;
55
56 virtual bool isExplicitQuantitativeCheckResult() const override;
57
58 vector_type const& getValueVector() const;
60 map_type const& getValueMap() const;
61
62 virtual std::ostream& writeToStream(std::ostream& out) const override;
63
64 virtual void filter(QualitativeCheckResult const& filter) override;
65
66 virtual void oneMinus() override;
67
68 virtual ValueType getMin() const override;
69 virtual ValueType getMax() const override;
70 virtual std::pair<ValueType, ValueType> getMinMax() const;
71 virtual ValueType average() const override;
72 virtual ValueType sum() const override;
73
74 virtual bool hasScheduler() const override;
75 void setScheduler(std::unique_ptr<storm::storage::Scheduler<ValueType>>&& scheduler);
78
79 storm::json<ValueType> toJson(std::optional<storm::storage::sparse::StateValuations> const& stateValuations = std::nullopt,
80 std::optional<storm::models::sparse::StateLabeling> const& stateLabels = std::nullopt) const;
81
82 private:
83 // The values of the quantitative check result.
84 boost::variant<vector_type, map_type> values;
85
86 // An optional scheduler that accompanies the values.
87 boost::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler;
88};
89} // namespace modelchecker
90} // namespace storm
virtual std::ostream & writeToStream(std::ostream &out) const override
virtual std::unique_ptr< CheckResult > clone() const override
storm::storage::Scheduler< ValueType > const & getScheduler() const
std::map< storm::storage::sparse::state_type, ValueType > map_type
ValueType & operator[](storm::storage::sparse::state_type state)
ExplicitQuantitativeCheckResult & operator=(ExplicitQuantitativeCheckResult const &other)=default
ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult &&other)=default
storm::json< ValueType > toJson(std::optional< storm::storage::sparse::StateValuations > const &stateValuations=std::nullopt, std::optional< storm::models::sparse::StateLabeling > const &stateLabels=std::nullopt) const
ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult const &other)=default
virtual std::pair< ValueType, ValueType > getMinMax() const
virtual void filter(QualitativeCheckResult const &filter) override
Filters the current result wrt.
void setScheduler(std::unique_ptr< storm::storage::Scheduler< ValueType > > &&scheduler)
ExplicitQuantitativeCheckResult & operator=(ExplicitQuantitativeCheckResult &&other)=default
virtual std::unique_ptr< CheckResult > compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const &bound) const override
This class defines which action is chosen in a particular state of a non-deterministic model.
Definition Scheduler.h:18
LabParser.cpp.
nlohmann::basic_json< std::map, std::vector, std::string, bool, int64_t, uint64_t, ValueType > json
Definition JsonForward.h:10