From f8d4fd8862a15529a35adecfcf9d01584b5fa8b7 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 12 Aug 2020 10:42:26 +0200 Subject: [PATCH] New utility function for exchanging informations between deterministic helpers. --- .../utility/SetInformationFromOtherHelper.h | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h b/src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h index 44dcc467c..9ca78aa4d 100644 --- a/src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h +++ b/src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h @@ -26,6 +26,21 @@ namespace storm { // Scheduler Production targetHelper.setProduceScheduler(sourceHelperType.isProduceSchedulerSet()); } + + /*! + * Forwards relevant information stored in another helper to the given helper + */ + template + void setInformationFromOtherHelperDeterministic(TargetHelperType& targetHelper, SourceHelperType const& sourceHelperType, std::function const& stateSetTransformer) { + // Relevancy of initial states. + if (sourceHelperType.hasRelevantStates()) { + targetHelper.setRelevantStates(stateSetTransformer(sourceHelperType.getRelevantStates())); + } + // Value threshold to which the result will be compared + if (sourceHelperType.isValueThresholdSet()) { + targetHelper.setValueThreshold(sourceHelperType.getValueThresholdComparisonType(), storm::utility::convertNumber(sourceHelperType.getValueThresholdValue())); + } + } } } } \ No newline at end of file