GraphConditions for any model type

src/storm/analysis/GraphConditions.cpp

@@ -1,4 +1,6 @@
 
+#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/Ctmc.h"
 #include "GraphConditions.h"
 #include "storm/utility/constants.h"
 #include "storm/exceptions/NotImplementedException.h"
@@ -9,8 +11,8 @@ namespace storm {
 
 
         template <typename ValueType>
-        ConstraintCollector<ValueType>::ConstraintCollector(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
-            process(dtmc);
+        ConstraintCollector<ValueType>::ConstraintCollector(storm::models::sparse::Model<ValueType> const& model) {
+            process(model);
         }
 
         template <typename ValueType>
@@ -50,10 +52,13 @@ namespace storm {
         }
 
         template <typename ValueType>
-        void ConstraintCollector<ValueType>::process(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
-            for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) {
+        void ConstraintCollector<ValueType>::process(storm::models::sparse::Model<ValueType> const& model) {
+            for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) {
                 ValueType sum = storm::utility::zero<ValueType>();
-                for (auto const& transition : dtmc.getRows(state)) {
+
+                for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
+                    auto const& transition = *transitionIt;
+                    std::cout << transition.getValue() << std::endl;
                     sum += transition.getValue();
                     if (!storm::utility::isConstant(transition.getValue())) {
                         auto const& transitionVars = transition.getValue().gatherVariables();
@@ -90,9 +95,17 @@ namespace storm {
                     // Assert: sum == 1
                     wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
                 }
+            }
 
+            if (model.getType() == storm::models::ModelType::Ctmc) {
+                auto const& exitRateVector = static_cast<storm::models::sparse::Ctmc<ValueType> const&>(model).getExitRateVector();
+                wellformedRequiresNonNegativeEntries(exitRateVector);
+            } else if (model.getType() == storm::models::ModelType::MarkovAutomaton) {
+                auto const& exitRateVector = static_cast<storm::models::sparse::MarkovAutomaton<ValueType> const&>(model).getExitRates();
+                wellformedRequiresNonNegativeEntries(exitRateVector);
             }
-            for(auto const& rewModelEntry : dtmc.getRewardModels()) {
+
+            for(auto const& rewModelEntry : model.getRewardModels()) {
                 if (rewModelEntry.second.hasStateRewards()) {
                     wellformedRequiresNonNegativeEntries(rewModelEntry.second.getStateRewardVector());
                 }
@@ -117,13 +130,13 @@ namespace storm {
                         }
                     }
                 }
-
             }
+
         }
 
         template <typename ValueType>
-        void ConstraintCollector<ValueType>::operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
-            process(dtmc);
+        void ConstraintCollector<ValueType>::operator()(storm::models::sparse::Model<ValueType> const& model) {
+            process(model);
         }
 
         template class ConstraintCollector<storm::RationalFunction>;

src/storm/analysis/GraphConditions.h

@@ -38,12 +38,12 @@ namespace storm {
             void wellformedRequiresNonNegativeEntries(std::vector<ValueType> const&);
         public:
             /*!
-             * Constructs a constraint collector for the given DTMC. The constraints are built and ready for
+             * Constructs a constraint collector for the given Model. The constraints are built and ready for
              * retrieval after the construction.
              *
-             * @param dtmc The DTMC for which to create the constraints.
+             * @param model The Model for which to create the constraints.
              */
-            ConstraintCollector(storm::models::sparse::Dtmc<ValueType> const& dtmc);
+            ConstraintCollector(storm::models::sparse::Model<ValueType> const& model);
             
             /*!
              * Returns the set of wellformed-ness constraints.
@@ -66,18 +66,18 @@ namespace storm {
             std::set<storm::RationalFunctionVariable> const& getVariables() const;
             
             /*!
-             * Constructs the constraints for the given DTMC.
+             * Constructs the constraints for the given Model.
              *
-             * @param dtmc The DTMC for which to create the constraints.
+             * @param model The DTMC for which to create the constraints.
              */
-            void process(storm::models::sparse::Dtmc<ValueType> const& dtmc);
+            void process(storm::models::sparse::Model<ValueType> const& model);
             
             /*!
-             * Constructs the constraints for the given DTMC by calling the process method.
+             * Constructs the constraints for the given Model by calling the process method.
              *
-             * @param dtmc The DTMC for which to create the constraints.
+             * @param model The Model for which to create the constraints.
              */
-            void operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc);
+            void operator()(storm::models::sparse::Model<ValueType> const& model);
             
         };