From f94d45483e13d019a562efaa9f3a579c9949cefc Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 19 Aug 2020 16:06:09 +0200 Subject: [PATCH] Use the new model representation enum in the model checking helpers. --- .../helper/ModelCheckerHelper.cpp | 34 ++++----- .../modelchecker/helper/ModelCheckerHelper.h | 8 +- .../helper/SingleValueModelCheckerHelper.cpp | 74 +++++++++---------- .../helper/SingleValueModelCheckerHelper.h | 6 +- .../HybridInfiniteHorizonHelper.h | 2 +- .../SparseInfiniteHorizonHelper.h | 2 +- 6 files changed, 63 insertions(+), 63 deletions(-) diff --git a/src/storm/modelchecker/helper/ModelCheckerHelper.cpp b/src/storm/modelchecker/helper/ModelCheckerHelper.cpp index f2c7e12f4..716ffdec8 100644 --- a/src/storm/modelchecker/helper/ModelCheckerHelper.cpp +++ b/src/storm/modelchecker/helper/ModelCheckerHelper.cpp @@ -6,41 +6,41 @@ namespace storm { namespace modelchecker { namespace helper { - template - void ModelCheckerHelper::setRelevantStates(StateSet const& relevantStates) { + template + void ModelCheckerHelper::setRelevantStates(StateSet const& relevantStates) { _relevantStates = relevantStates; } - template - void ModelCheckerHelper::clearRelevantStates() { + template + void ModelCheckerHelper::clearRelevantStates() { _relevantStates = boost::none; } - template - bool ModelCheckerHelper::hasRelevantStates() const { + template + bool ModelCheckerHelper::hasRelevantStates() const { return _relevantStates.is_initialized(); } - template - boost::optional::StateSet> const& ModelCheckerHelper::getOptionalRelevantStates() const { + template + boost::optional::StateSet> const& ModelCheckerHelper::getOptionalRelevantStates() const { return _relevantStates; } - template - typename ModelCheckerHelper::StateSet const& ModelCheckerHelper::getRelevantStates() const { + template + typename ModelCheckerHelper::StateSet const& ModelCheckerHelper::getRelevantStates() const { STORM_LOG_ASSERT(hasRelevantStates(), "Retrieving relevant states although none have been set."); return _relevantStates.get(); } - template class ModelCheckerHelper; - template class ModelCheckerHelper; - template class ModelCheckerHelper; + template class ModelCheckerHelper; + template class ModelCheckerHelper; + template class ModelCheckerHelper; - template class ModelCheckerHelper; - template class ModelCheckerHelper; - template class ModelCheckerHelper; + template class ModelCheckerHelper; + template class ModelCheckerHelper; + template class ModelCheckerHelper; - template class ModelCheckerHelper; + template class ModelCheckerHelper; } } diff --git a/src/storm/modelchecker/helper/ModelCheckerHelper.h b/src/storm/modelchecker/helper/ModelCheckerHelper.h index bdf708d07..05e87ea11 100644 --- a/src/storm/modelchecker/helper/ModelCheckerHelper.h +++ b/src/storm/modelchecker/helper/ModelCheckerHelper.h @@ -3,7 +3,7 @@ #include #include -#include "storm/storage/dd/DdType.h" +#include "storm/models/ModelRepresentation.h" #include "storm/storage/dd/Bdd.h" #include "storm/storage/BitVector.h" @@ -15,9 +15,9 @@ namespace storm { /*! * Helper class for solving a model checking query. * @tparam VT The value type of a single value. - * @tparam DdType The used library for Dds (or None in case of a sparse representation). + * @tparam ModelRepresentation The used kind of model representation */ - template + template class ModelCheckerHelper { public: typedef VT ValueType; @@ -28,7 +28,7 @@ namespace storm { /*! * Identifies a subset of the model states */ - using StateSet = typename std::conditional>::type; + using StateSet = typename std::conditional::ddType>>::type; /*! * Sets relevant states. diff --git a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp index 0487cb673..796b696f8 100644 --- a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp +++ b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp @@ -5,93 +5,93 @@ namespace storm { namespace modelchecker { namespace helper { - template - SingleValueModelCheckerHelper::SingleValueModelCheckerHelper() : _produceScheduler(false) { + template + SingleValueModelCheckerHelper::SingleValueModelCheckerHelper() : _produceScheduler(false) { // Intentionally left empty } - template - void SingleValueModelCheckerHelper::setOptimizationDirection(storm::solver::OptimizationDirection const& direction) { + template + void SingleValueModelCheckerHelper::setOptimizationDirection(storm::solver::OptimizationDirection const& direction) { _optimizationDirection = direction; } - template - void SingleValueModelCheckerHelper::clearOptimizationDirection() { + template + void SingleValueModelCheckerHelper::clearOptimizationDirection() { _optimizationDirection = boost::none; } - template - bool SingleValueModelCheckerHelper::isOptimizationDirectionSet() const { + template + bool SingleValueModelCheckerHelper::isOptimizationDirectionSet() const { return _optimizationDirection.is_initialized(); } - template - storm::solver::OptimizationDirection const& SingleValueModelCheckerHelper::getOptimizationDirection() const { + template + storm::solver::OptimizationDirection const& SingleValueModelCheckerHelper::getOptimizationDirection() const { STORM_LOG_ASSERT(isOptimizationDirectionSet(), "Requested optimization direction but none was set."); return _optimizationDirection.get(); } - template - bool SingleValueModelCheckerHelper::minimize() const { + template + bool SingleValueModelCheckerHelper::minimize() const { return storm::solver::minimize(getOptimizationDirection()); } - template - bool SingleValueModelCheckerHelper::maximize() const { + template + bool SingleValueModelCheckerHelper::maximize() const { return storm::solver::maximize(getOptimizationDirection()); } - template - boost::optional SingleValueModelCheckerHelper::getOptionalOptimizationDirection() const { + template + boost::optional SingleValueModelCheckerHelper::getOptionalOptimizationDirection() const { return _optimizationDirection; } - template - void SingleValueModelCheckerHelper::setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& threshold) { + template + void SingleValueModelCheckerHelper::setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& threshold) { _valueThreshold = std::make_pair(comparisonType, threshold); } - template - void SingleValueModelCheckerHelper::clearValueThreshold() { + template + void SingleValueModelCheckerHelper::clearValueThreshold() { _valueThreshold = boost::none; } - template - bool SingleValueModelCheckerHelper::isValueThresholdSet() const { + template + bool SingleValueModelCheckerHelper::isValueThresholdSet() const { return _valueThreshold.is_initialized(); } - template - storm::logic::ComparisonType const& SingleValueModelCheckerHelper::getValueThresholdComparisonType() const { + template + storm::logic::ComparisonType const& SingleValueModelCheckerHelper::getValueThresholdComparisonType() const { STORM_LOG_ASSERT(isValueThresholdSet(), "Value Threshold comparison type was requested but not set before."); return _valueThreshold->first; } - template - ValueType const& SingleValueModelCheckerHelper::getValueThresholdValue() const { + template + ValueType const& SingleValueModelCheckerHelper::getValueThresholdValue() const { STORM_LOG_ASSERT(isValueThresholdSet(), "Value Threshold comparison type was requested but not set before."); return _valueThreshold->second; } - template - void SingleValueModelCheckerHelper::setProduceScheduler(bool value) { + template + void SingleValueModelCheckerHelper::setProduceScheduler(bool value) { _produceScheduler = value; } - template - bool SingleValueModelCheckerHelper::isProduceSchedulerSet() const { + template + bool SingleValueModelCheckerHelper::isProduceSchedulerSet() const { return _produceScheduler; } - template class SingleValueModelCheckerHelper; - template class SingleValueModelCheckerHelper; - template class SingleValueModelCheckerHelper; + template class SingleValueModelCheckerHelper; + template class SingleValueModelCheckerHelper; + template class SingleValueModelCheckerHelper; - template class SingleValueModelCheckerHelper; - template class SingleValueModelCheckerHelper; - template class SingleValueModelCheckerHelper; + template class SingleValueModelCheckerHelper; + template class SingleValueModelCheckerHelper; + template class SingleValueModelCheckerHelper; - template class SingleValueModelCheckerHelper; + template class SingleValueModelCheckerHelper; } } diff --git a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h index 2b7776c3d..2246ef793 100644 --- a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h +++ b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h @@ -12,10 +12,10 @@ namespace storm { /*! * Helper for model checking queries where we are interested in (optimizing) a single value per state. * @tparam ValueType The type of a value - * @tparam DdType The used library for Dds (or None in case of a sparse representation) + * @tparam ModelRepresentation The used kind of model representation */ - template - class SingleValueModelCheckerHelper : public ModelCheckerHelper { + template + class SingleValueModelCheckerHelper : public ModelCheckerHelper { public: SingleValueModelCheckerHelper(); diff --git a/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h index 09035c6f3..92999133d 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h @@ -27,7 +27,7 @@ namespace storm { * Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. */ template - class HybridInfiniteHorizonHelper : public SingleValueModelCheckerHelper { + class HybridInfiniteHorizonHelper : public SingleValueModelCheckerHelper::representation> { public: /*! diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h index b8ebcef0b..6630dd5ad 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h @@ -24,7 +24,7 @@ namespace storm { * @tparam Nondeterministic true if there is nondeterminism in the Model (MDP or MA) */ template - class SparseInfiniteHorizonHelper : public SingleValueModelCheckerHelper { + class SparseInfiniteHorizonHelper : public SingleValueModelCheckerHelper { public: