Browse Source

ModelCheckerHelper: Added utility function that copies model checking information from one helper to another.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
7795ce5f35
  1. 6
      src/storm/modelchecker/helper/ModelCheckerHelper.h
  2. 31
      src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h

6
src/storm/modelchecker/helper/ModelCheckerHelper.h

@ -14,12 +14,14 @@ namespace storm {
/*! /*!
* Helper class for solving a model checking query. * 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). * @tparam DdType The used library for Dds (or None in case of a sparse representation).
*/ */
template <typename ValueType, storm::dd::DdType DdType = storm::dd::DdType::None>
template <typename VT, storm::dd::DdType DdType = storm::dd::DdType::None>
class ModelCheckerHelper { class ModelCheckerHelper {
public: public:
typedef VT ValueType;
ModelCheckerHelper() = default; ModelCheckerHelper() = default;
~ModelCheckerHelper() = default; ~ModelCheckerHelper() = default;

31
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 <typename TargetHelperType, typename SourceHelperType>
void setInformationFromOtherHelperNondeterministic(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()));
}
// Optimization direction
if (sourceHelperType.isOptimizationDirectionSet()) {
targetHelper.setOptimizationDirection(sourceHelperType.getOptimizationDirection());
}
// Scheduler Production
targetHelper.setProduceScheduler(sourceHelperType.isProduceSchedulerSet());
}
}
}
}
Loading…
Cancel
Save