diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index e05c83344..19b1f627e 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -51,6 +51,31 @@ namespace storm { ExplicitQuantitativeCheckResult::ExplicitQuantitativeCheckResult(boost::variant&& values, boost::optional>> scheduler) : values(std::move(values)), scheduler(scheduler) { // Intentionally left empty. } + + template + ExplicitQuantitativeCheckResult::ExplicitQuantitativeCheckResult(ExplicitQualitativeCheckResult const& other) { + if (other.isResultForAllStates()) { + storm::storage::BitVector const& bvValues = other.getTruthValuesVector(); + + vector_type newVector; + newVector.reserve(bvValues.size()); + for (std::size_t i = 0, n = bvValues.size(); i < n; i++) { + newVector.push_back(bvValues.get(i) ? storm::utility::one() : storm::utility::zero()); + } + + values = newVector; + } else { + ExplicitQualitativeCheckResult::map_type const& bitMap = other.getTruthValuesMap(); + + map_type newMap; + for (auto const& e : bitMap) { + newMap[e.first] = e.second ? storm::utility::one() : storm::utility::zero(); + } + + values = newMap; + } + } + template std::unique_ptr ExplicitQuantitativeCheckResult::clone() const { diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h index e6fe5a178..4fe38b0f0 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -16,6 +16,9 @@ namespace storm { namespace modelchecker { + // fwd + class ExplicitQualitativeCheckResult; + template class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult { public: @@ -37,6 +40,8 @@ namespace storm { ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult&& other) = default; ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult&& other) = default; #endif + explicit ExplicitQuantitativeCheckResult(ExplicitQualitativeCheckResult const& other); + virtual ~ExplicitQuantitativeCheckResult() = default; virtual std::unique_ptr clone() const override; diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index ef778a7f7..37d79ffea 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -22,6 +22,12 @@ namespace storm { // Intentionally left empty. } + + template + SymbolicQuantitativeCheckResult::SymbolicQuantitativeCheckResult(SymbolicQualitativeCheckResult const& other) : reachableStates(other.getReachableStates()), states(other.getStates()), values(other.getTruthValuesVector().template toAdd()) { + // Intentionally left empty. + } + template std::unique_ptr SymbolicQuantitativeCheckResult::clone() const { return std::make_unique>(this->reachableStates, this->states, this->values); diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h index d1d5fa3ba..61c041d5f 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -8,6 +8,10 @@ namespace storm { namespace modelchecker { + // fwd + template + class SymbolicQualitativeCheckResult; + template class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult { public: @@ -21,6 +25,8 @@ namespace storm { SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult&& other) = default; SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult&& other) = default; #endif + + SymbolicQuantitativeCheckResult(SymbolicQualitativeCheckResult const& other); virtual std::unique_ptr clone() const override;