From 27ca10a668907212fe4185a0e5de05d15ecc2531 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 24 Aug 2020 22:25:08 +0200 Subject: [PATCH] (stateformula) SymbolicQualitativeCheckResult: add getReachableStates() and getStates() accessors, like SymbolicQuantitativeCheckResult --- .../results/SymbolicQualitativeCheckResult.cpp | 10 ++++++++++ .../results/SymbolicQualitativeCheckResult.h | 2 ++ 2 files changed, 12 insertions(+) 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;