diff --git a/src/storm/modelchecker/helper/ModelCheckerHelper.h b/src/storm/modelchecker/helper/ModelCheckerHelper.h index 05169ae17..02ee35531 100644 --- a/src/storm/modelchecker/helper/ModelCheckerHelper.h +++ b/src/storm/modelchecker/helper/ModelCheckerHelper.h @@ -14,12 +14,14 @@ namespace storm { /*! * Helper class for solving a model checking query. - * @tparam ValueType The type of a single value. + * @tparam VT The value type of a single value. * @tparam DdType The used library for Dds (or None in case of a sparse representation). */ - template + template class ModelCheckerHelper { public: + typedef VT ValueType; + ModelCheckerHelper() = default; ~ModelCheckerHelper() = default; diff --git a/src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h b/src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h new file mode 100644 index 000000000..44dcc467c --- /dev/null +++ b/src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h @@ -0,0 +1,31 @@ +#pragma once + +#include "storm/modelchecker/CheckTask.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + /*! + * Forwards relevant information stored in another helper to the given helper + */ + template + void setInformationFromOtherHelperNondeterministic(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())); + } + // Optimization direction + if (sourceHelperType.isOptimizationDirectionSet()) { + targetHelper.setOptimizationDirection(sourceHelperType.getOptimizationDirection()); + } + // Scheduler Production + targetHelper.setProduceScheduler(sourceHelperType.isProduceSchedulerSet()); + } + } + } +} \ No newline at end of file