From f746386512074e6b3e4095cfd649b46b492335b3 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 2 Jun 2017 20:50:58 +0200
Subject: [PATCH] slightly reverting Matthias last change (include of
 carl::Formula)

---
 src/storm/analysis/GraphConditions.h | 132 +++++++++++++--------------
 1 file changed, 65 insertions(+), 67 deletions(-)

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 <carl/formula/Formula.h>
 
-#include <carl/formula/Formula.h>
-
 namespace storm {
     namespace analysis {
-
-template <typename ValueType, typename Enable=void>
-struct ConstraintType {
-    typedef storm::ArithConstraint<ValueType> val;
-};
-
-template<typename ValueType>
-struct ConstraintType<ValueType, typename std::enable_if<std::is_same<storm::RationalFunction, ValueType>::value>::type> {
-   typedef carl::Formula<typename ValueType::PolyType::PolyType> val;
-};
-
-/**
- * Class to collect constraints on parametric Markov chains.
- */
-template<typename ValueType>
-class ConstraintCollector {
-private:
-    // A set of constraints that says that the DTMC actually has valid probability distributions in all states.
-    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
-    // on the parameter values.
-    std::unordered_set<typename ConstraintType<ValueType>::val> graphPreservingConstraintSet;
-
-    void wellformedRequiresNonNegativeEntries(std::vector<ValueType> 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<ValueType> const& dtmc);
-
-    /*!
-     * Returns the set of wellformed-ness constraints.
-     *
-     * @return The set of wellformed-ness constraints.
-     */
-    std::unordered_set<typename ConstraintType<ValueType>::val> const&  getWellformedConstraints() const;
-
-    /*!
-     * Returns the set of graph-preserving constraints.
-     *
-     * @return The set of graph-preserving constraints.
-     */
-    std::unordered_set<typename ConstraintType<ValueType>::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<ValueType> 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<ValueType> const& dtmc);
-
-};
-
-
+        
+        template <typename ValueType, typename Enable=void>
+        struct ConstraintType {
+            typedef storm::ArithConstraint<ValueType> val;
+        };
+        
+        template<typename ValueType>
+        struct ConstraintType<ValueType, typename std::enable_if<std::is_same<storm::RationalFunction, ValueType>::value>::type> {
+            typedef carl::Formula<typename ValueType::PolyType::PolyType> val;
+        };
+        
+        /**
+         * Class to collect constraints on parametric Markov chains.
+         */
+        template<typename ValueType>
+        class ConstraintCollector {
+        private:
+            // A set of constraints that says that the DTMC actually has valid probability distributions in all states.
+            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
+            // on the parameter values.
+            std::unordered_set<typename ConstraintType<ValueType>::val> graphPreservingConstraintSet;
+            
+            void wellformedRequiresNonNegativeEntries(std::vector<ValueType> 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<ValueType> const& dtmc);
+            
+            /*!
+             * Returns the set of wellformed-ness constraints.
+             *
+             * @return The set of wellformed-ness constraints.
+             */
+            std::unordered_set<typename ConstraintType<ValueType>::val> const&  getWellformedConstraints() const;
+            
+            /*!
+             * Returns the set of graph-preserving constraints.
+             *
+             * @return The set of graph-preserving constraints.
+             */
+            std::unordered_set<typename ConstraintType<ValueType>::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<ValueType> 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<ValueType> const& dtmc);
+            
+        };
+        
+        
     }
 }