Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
HybridQuantitativeCheckResult.h
Go to the documentation of this file.
1#ifndef STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_
2#define STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_
3
9
10namespace storm {
11namespace modelchecker {
12template<storm::dd::DdType Type, typename ValueType = double>
14 public:
16 HybridQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& symbolicStates,
17 storm::dd::Add<Type, ValueType> const& symbolicValues, storm::dd::Bdd<Type> const& explicitStates, storm::dd::Odd const& odd,
18 std::vector<ValueType> const& explicitValues);
19
24
25 virtual std::unique_ptr<CheckResult> clone() const override;
26
27 virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override;
28
29 std::unique_ptr<CheckResult> toExplicitQuantitativeCheckResult() const;
30
31 virtual bool isHybrid() const override;
32 virtual bool isResultForAllStates() const override;
33
34 virtual bool isHybridQuantitativeCheckResult() const override;
35
37
39
41
42 storm::dd::Odd const& getOdd() const;
43
44 std::vector<ValueType> const& getExplicitValueVector() const;
45
46 virtual std::ostream& writeToStream(std::ostream& out) const override;
47
48 virtual void filter(QualitativeCheckResult const& filter) override;
49
50 virtual ValueType getMin() const override;
51
52 virtual ValueType getMax() const override;
53
54 virtual ValueType sum() const override;
55
56 virtual ValueType average() const override;
57
58 virtual void oneMinus() override;
59
60 private:
61 // The set of all reachable states.
62 storm::dd::Bdd<Type> reachableStates;
63
64 // The set of all states whose result is stored symbolically.
65 storm::dd::Bdd<Type> symbolicStates;
66
67 // The symbolic value vector.
69
70 // The set of all states whose result is stored explicitly.
71 storm::dd::Bdd<Type> explicitStates;
72
73 // The ODD that enables translation of the explicit values to a symbolic format.
75
76 // The explicit value vector.
77 std::vector<ValueType> explicitValues;
78};
79} // namespace modelchecker
80} // namespace storm
81
82#endif /* STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ */
virtual std::ostream & writeToStream(std::ostream &out) const override
HybridQuantitativeCheckResult & operator=(HybridQuantitativeCheckResult &&other)=default
std::vector< ValueType > const & getExplicitValueVector() const
std::unique_ptr< CheckResult > toExplicitQuantitativeCheckResult() const
HybridQuantitativeCheckResult(HybridQuantitativeCheckResult &&other)=default
virtual std::unique_ptr< CheckResult > compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const &bound) const override
virtual void filter(QualitativeCheckResult const &filter) override
Filters the current result wrt.
virtual std::unique_ptr< CheckResult > clone() const override
storm::dd::Add< Type, ValueType > const & getSymbolicValueVector() const
HybridQuantitativeCheckResult & operator=(HybridQuantitativeCheckResult const &other)=default
HybridQuantitativeCheckResult(HybridQuantitativeCheckResult const &other)=default
LabParser.cpp.