Browse Source

New utility function for exchanging informations between deterministic helpers.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
f8d4fd8862
  1. 15
      src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h

15
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 <typename TargetHelperType, typename SourceHelperType>
void setInformationFromOtherHelperDeterministic(TargetHelperType& targetHelper, SourceHelperType const& sourceHelperType, std::function<typename TargetHelperType::StateSet(typename SourceHelperType::StateSet const&)> 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<typename TargetHelperType::ValueType>(sourceHelperType.getValueThresholdValue()));
}
}
}
}
}
Loading…
Cancel
Save