From a639836f6fb800b61c64a96acbc38b4a5d835382 Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Mon, 24 Aug 2020 22:25:09 +0200
Subject: [PATCH] (stateformula) CheckResults: provide constructor for
 quantitative from qualitative result

---
 .../ExplicitQuantitativeCheckResult.cpp       | 25 +++++++++++++++++++
 .../results/ExplicitQuantitativeCheckResult.h |  5 ++++
 .../SymbolicQuantitativeCheckResult.cpp       |  6 +++++
 .../results/SymbolicQuantitativeCheckResult.h |  6 +++++
 4 files changed, 42 insertions(+)

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<ValueType>::ExplicitQuantitativeCheckResult(boost::variant<vector_type, map_type>&& values, boost::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler) : values(std::move(values)), scheduler(scheduler) {
             // Intentionally left empty.
         }
+
+        template<typename ValueType>
+        ExplicitQuantitativeCheckResult<ValueType>::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<ValueType>() : storm::utility::zero<ValueType>());
+                }
+
+                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<ValueType>() : storm::utility::zero<ValueType>();
+                }
+
+                values = newMap;
+            }
+        }
+
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<ValueType>::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<typename ValueType>
         class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult<ValueType> {
         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<CheckResult> 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<storm::dd::DdType Type, typename ValueType>
+        SymbolicQuantitativeCheckResult<Type, ValueType>::SymbolicQuantitativeCheckResult(SymbolicQualitativeCheckResult<Type> const& other) : reachableStates(other.getReachableStates()), states(other.getStates()), values(other.getTruthValuesVector().template toAdd<ValueType>()) {
+            // Intentionally left empty.
+        }
+
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> SymbolicQuantitativeCheckResult<Type, ValueType>::clone() const {
             return std::make_unique<SymbolicQuantitativeCheckResult<Type, ValueType>>(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<storm::dd::DdType Type>
+        class SymbolicQualitativeCheckResult;
+
         template<storm::dd::DdType Type, typename ValueType = double>
         class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult<ValueType> {
         public:
@@ -21,6 +25,8 @@ namespace storm {
             SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult&& other) = default;
             SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult&& other) = default;
 #endif
+
+            SymbolicQuantitativeCheckResult(SymbolicQualitativeCheckResult<Type> const& other);
             
             virtual std::unique_ptr<CheckResult> clone() const override;