diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 5b5140431..87b95a78c 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -6,74 +6,72 @@ #include "storm/models/sparse/Dtmc.h" #include -#include - namespace storm { namespace analysis { - -template -struct ConstraintType { - typedef storm::ArithConstraint val; -}; - -template -struct ConstraintType::value>::type> { - typedef carl::Formula val; -}; - -/** - * Class to collect constraints on parametric Markov chains. - */ -template -class ConstraintCollector { -private: - // A set of constraints that says that the DTMC actually has valid probability distributions in all states. - std::unordered_set::val> wellformedConstraintSet; - - // A set of constraints that makes sure that the underlying graph of the model does not change depending - // on the parameter values. - std::unordered_set::val> graphPreservingConstraintSet; - - void wellformedRequiresNonNegativeEntries(std::vector const&); -public: - /*! - * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for - * retrieval after the construction. - * - * @param dtmc The DTMC for which to create the constraints. - */ - ConstraintCollector(storm::models::sparse::Dtmc const& dtmc); - - /*! - * Returns the set of wellformed-ness constraints. - * - * @return The set of wellformed-ness constraints. - */ - std::unordered_set::val> const& getWellformedConstraints() const; - - /*! - * Returns the set of graph-preserving constraints. - * - * @return The set of graph-preserving constraints. - */ - std::unordered_set::val> const& getGraphPreservingConstraints() const; - - /*! - * Constructs the constraints for the given DTMC. - * - * @param dtmc The DTMC for which to create the constraints. - */ - void process(storm::models::sparse::Dtmc const& dtmc); - - /*! - * Constructs the constraints for the given DTMC by calling the process method. - * - * @param dtmc The DTMC for which to create the constraints. - */ - void operator()(storm::models::sparse::Dtmc const& dtmc); - -}; - - + + template + struct ConstraintType { + typedef storm::ArithConstraint val; + }; + + template + struct ConstraintType::value>::type> { + typedef carl::Formula val; + }; + + /** + * Class to collect constraints on parametric Markov chains. + */ + template + class ConstraintCollector { + private: + // A set of constraints that says that the DTMC actually has valid probability distributions in all states. + std::unordered_set::val> wellformedConstraintSet; + + // A set of constraints that makes sure that the underlying graph of the model does not change depending + // on the parameter values. + std::unordered_set::val> graphPreservingConstraintSet; + + void wellformedRequiresNonNegativeEntries(std::vector const&); + public: + /*! + * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for + * retrieval after the construction. + * + * @param dtmc The DTMC for which to create the constraints. + */ + ConstraintCollector(storm::models::sparse::Dtmc const& dtmc); + + /*! + * Returns the set of wellformed-ness constraints. + * + * @return The set of wellformed-ness constraints. + */ + std::unordered_set::val> const& getWellformedConstraints() const; + + /*! + * Returns the set of graph-preserving constraints. + * + * @return The set of graph-preserving constraints. + */ + std::unordered_set::val> const& getGraphPreservingConstraints() const; + + /*! + * Constructs the constraints for the given DTMC. + * + * @param dtmc The DTMC for which to create the constraints. + */ + void process(storm::models::sparse::Dtmc const& dtmc); + + /*! + * Constructs the constraints for the given DTMC by calling the process method. + * + * @param dtmc The DTMC for which to create the constraints. + */ + void operator()(storm::models::sparse::Dtmc const& dtmc); + + }; + + } }