Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SymbolicQualitativeCheckResult.h
Go to the documentation of this file.
1#ifndef STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_
2#define STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_
3
7
8namespace storm {
9namespace modelchecker {
10template<storm::dd::DdType Type>
12 public:
14 SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& truthValues);
15 SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& states, storm::dd::Bdd<Type> const& truthValues);
16
21
22 virtual std::unique_ptr<CheckResult> clone() const override;
23
24 virtual bool isSymbolic() const override;
25 virtual bool isResultForAllStates() const override;
26
27 virtual bool isSymbolicQualitativeCheckResult() const override;
28
29 virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) override;
30 virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override;
31 virtual void complement() override;
32
33 virtual bool existsTrue() const override;
34 virtual bool forallTrue() const override;
35 virtual uint64_t count() const override;
36
38 storm::dd::Bdd<Type> const& getStates() const;
40
41 virtual std::ostream& writeToStream(std::ostream& out) const override;
42
43 virtual void filter(QualitativeCheckResult const& filter) override;
44
45 private:
46 // The set of all reachable states.
47 storm::dd::Bdd<Type> reachableStates;
48
49 // The set of states for which this check result contains values.
51
52 // The values of the qualitative check result.
53 storm::dd::Bdd<Type> truthValues;
54};
55} // namespace modelchecker
56} // namespace storm
57
58#endif /* STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ */
SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult const &other)=default
virtual void filter(QualitativeCheckResult const &filter) override
Filters the current result wrt.
virtual std::unique_ptr< CheckResult > clone() const override
SymbolicQualitativeCheckResult & operator=(SymbolicQualitativeCheckResult const &other)=default
virtual QualitativeCheckResult & operator&=(QualitativeCheckResult const &other) override
virtual QualitativeCheckResult & operator|=(QualitativeCheckResult const &other) override
SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult &&other)=default
virtual std::ostream & writeToStream(std::ostream &out) const override
SymbolicQualitativeCheckResult & operator=(SymbolicQualitativeCheckResult &&other)=default
LabParser.cpp.