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