(stateformula) CheckResults: provide constructor for quantitative from qualitative result

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -52,6 +52,31 @@ namespace storm {
             // 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 {
             return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(this->values, this->scheduler);

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;

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);

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:
@@ -22,6 +26,8 @@ namespace storm {
             SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult&& other) = default;
 #endif
 
+            SymbolicQuantitativeCheckResult(SymbolicQualitativeCheckResult<Type> const& other);
+            
             virtual std::unique_ptr<CheckResult> clone() const override;
 
             virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override;