|
@ -8,6 +8,17 @@ |
|
|
namespace storm { |
|
|
namespace storm { |
|
|
namespace analysis { |
|
|
namespace analysis { |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
template <typename ValueType, typename Enable=void> |
|
|
|
|
|
struct ConstraintType { |
|
|
|
|
|
typedef void* val; |
|
|
|
|
|
}; |
|
|
|
|
|
|
|
|
|
|
|
template<typename ValueType> |
|
|
|
|
|
struct ConstraintType<ValueType, typename std::enable_if<std::is_same<storm::RationalFunction, ValueType>::value>::type> { |
|
|
|
|
|
typedef storm::RationalFunctionConstraint val; |
|
|
|
|
|
}; |
|
|
|
|
|
|
|
|
/** |
|
|
/** |
|
|
* Class to collect constraints on parametric Markov chains. |
|
|
* Class to collect constraints on parametric Markov chains. |
|
|
*/ |
|
|
*/ |
|
@ -15,11 +26,11 @@ namespace storm { |
|
|
class ConstraintCollector { |
|
|
class ConstraintCollector { |
|
|
private: |
|
|
private: |
|
|
// A set of constraints that says that the DTMC actually has valid probability distributions in all states. |
|
|
// A set of constraints that says that the DTMC actually has valid probability distributions in all states. |
|
|
std::unordered_set<typename storm::ConstraintType<ValueType>::val> wellformedConstraintSet; |
|
|
|
|
|
|
|
|
std::unordered_set<typename ConstraintType<ValueType>::val> wellformedConstraintSet; |
|
|
|
|
|
|
|
|
// A set of constraints that makes sure that the underlying graph of the model does not change depending |
|
|
// A set of constraints that makes sure that the underlying graph of the model does not change depending |
|
|
// on the parameter values. |
|
|
// on the parameter values. |
|
|
std::unordered_set<typename storm::ConstraintType<ValueType>::val> graphPreservingConstraintSet; |
|
|
|
|
|
|
|
|
std::unordered_set<typename ConstraintType<ValueType>::val> graphPreservingConstraintSet; |
|
|
|
|
|
|
|
|
// A set of variables |
|
|
// A set of variables |
|
|
std::set<storm::RationalFunctionVariable> variableSet; |
|
|
std::set<storm::RationalFunctionVariable> variableSet; |
|
|