diff --git a/src/modelchecker/results/CheckResult.h b/src/modelchecker/results/CheckResult.h index 93ff1399f..1de7a33c5 100644 --- a/src/modelchecker/results/CheckResult.h +++ b/src/modelchecker/results/CheckResult.h @@ -21,6 +21,8 @@ namespace storm { // The base class of all check results. class CheckResult { public: + virtual ~CheckResult() = default; + /*! * Filters the current result wrt. to the filter, i.e. only keeps the entries that are selected by the filter. * This means that the filter must be a qualitative result of proper type (symbolic/explicit). diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/modelchecker/results/ExplicitQualitativeCheckResult.h index abce327b4..665675cfd 100644 --- a/src/modelchecker/results/ExplicitQualitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.h @@ -18,6 +18,7 @@ namespace storm { typedef std::map map_type; ExplicitQualitativeCheckResult(); + virtual ~ExplicitQualitativeCheckResult() = default; ExplicitQualitativeCheckResult(map_type const& map); ExplicitQualitativeCheckResult(map_type&& map); ExplicitQualitativeCheckResult(storm::storage::sparse::state_type state, bool value); diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h index 07166d258..542abe059 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -30,6 +30,7 @@ namespace storm { ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult&& other) = default; ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult&& other) = default; #endif + virtual ~ExplicitQuantitativeCheckResult() = default; ValueType& operator[](storm::storage::sparse::state_type state); ValueType const& operator[](storm::storage::sparse::state_type state) const; diff --git a/src/modelchecker/results/QualitativeCheckResult.h b/src/modelchecker/results/QualitativeCheckResult.h index 5904d2b6e..608e2c0d1 100644 --- a/src/modelchecker/results/QualitativeCheckResult.h +++ b/src/modelchecker/results/QualitativeCheckResult.h @@ -7,6 +7,7 @@ namespace storm { namespace modelchecker { class QualitativeCheckResult : public CheckResult { public: + virtual ~QualitativeCheckResult() = default; virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other); virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other); virtual void complement(); diff --git a/src/modelchecker/results/QuantitativeCheckResult.h b/src/modelchecker/results/QuantitativeCheckResult.h index 2dc1afc39..425e7b6ef 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.h +++ b/src/modelchecker/results/QuantitativeCheckResult.h @@ -7,6 +7,9 @@ namespace storm { namespace modelchecker { class QuantitativeCheckResult : public CheckResult { public: + + virtual ~QuantitativeCheckResult() = default; + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const; virtual bool isQuantitative() const override; diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp index 5923b5284..ed3d82fe4 100644 --- a/src/utility/ConstantsComparator.cpp +++ b/src/utility/ConstantsComparator.cpp @@ -12,12 +12,12 @@ namespace storm { namespace utility { template bool ConstantsComparator::isOne(ValueType const& value) const { - return isOne(value); + return storm::utility::isOne(value); } template bool ConstantsComparator::isZero(ValueType const& value) const { - return isZero(value); + return storm::utility::isZero(value); } template @@ -27,7 +27,7 @@ namespace storm { template bool ConstantsComparator::isConstant(ValueType const& value) const { - return isConstant(value); + return storm::utility::isConstant(value); } template