diff --git a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp index 1fea0544c..d11d0afe4 100644 --- a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -61,6 +61,16 @@ namespace storm { return this->truthValues; } + template + storm::dd::Bdd const& SymbolicQualitativeCheckResult::getStates() const { + return states; + } + + template + storm::dd::Bdd const& SymbolicQualitativeCheckResult::getReachableStates() const { + return reachableStates; + } + template bool SymbolicQualitativeCheckResult::existsTrue() const { return !this->truthValues.isZero(); diff --git a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.h index 9afa4cd0f..2c2c022f1 100644 --- a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -40,6 +40,8 @@ namespace storm { storm::dd::Bdd const& getTruthValuesVector() const; + storm::dd::Bdd const& getStates() const; + storm::dd::Bdd const& getReachableStates() const; virtual std::ostream& writeToStream(std::ostream& out) const override;