towards proper side constraints for parametetric systems

src/storm/adapters/CarlAdapter.h

@@ -9,6 +9,7 @@
 #include <carl/core/Relation.h>
 #include <carl/core/SimpleConstraint.h>
 #include <carl/util/stringparser.h>
+#include <carl/formula/Formula.h>
 
 namespace carl {
     // Define hash values for all polynomials and rational function.

src/storm/analysis/GraphConditions.cpp

@@ -0,0 +1,63 @@
+
+#include "GraphConditions.h"
+#include "storm/utility/constants.h"
+#include "storm/exceptions/NotImplementedException.h"
+
+namespace storm {
+    namespace analysis {
+        template <typename ValueType>
+        ConstraintCollector<ValueType>::ConstraintCollector(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
+            process(dtmc);
+        }
+
+        template <typename ValueType>
+        std::unordered_set<typename ConstraintType<ValueType>::val> const& ConstraintCollector<ValueType>::getWellformedConstraints() const {
+            return this->wellformedConstraintSet;
+        }
+
+        template <typename ValueType>
+        std::unordered_set<typename ConstraintType<ValueType>::val> const& ConstraintCollector<ValueType>::getGraphPreservingConstraints() const {
+            return this->graphPreservingConstraintSet;
+        }
+
+        template <typename ValueType>
+        void ConstraintCollector<ValueType>::process(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
+            for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) {
+                ValueType sum = storm::utility::zero<ValueType>();
+                for (auto const& transition : dtmc.getRows(state)) {
+                    sum += transition.getValue();
+                    if (!storm::utility::isConstant(transition.getValue())) {
+                        if (transition.getValue().denominator().isConstant()) {
+                            if (transition.getValue().denominatorAsNumber() > 0) {
+                                wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::LEQ);
+                                wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ);
+                            } else if (transition.getValue().denominatorAsNumber() < 0) {
+                                wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::GEQ);
+                                wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ);
+                            } else {
+                                assert(false); // Should fail before.
+                            }
+                        } else {
+                            wellformedConstraintSet.emplace(transition.getValue().denominator().polynomial(), storm::CompareRelation::NEQ);
+                            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at edges not yet supported.");
+                        }
+                        graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::NEQ);
+                    }
+                }
+                STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1.");
+                if(!storm::utility::isConstant(sum)) {
+                    wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomial(), storm::CompareRelation::EQ);
+                }
+
+            }
+        }
+
+        template <typename ValueType>
+        void ConstraintCollector<ValueType>::operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
+            process(dtmc);
+        }
+
+
+        template class ConstraintCollector<storm::RationalFunction>;
+    }
+}

src/storm/analysis/GraphConditions.h

@@ -0,0 +1,75 @@
+#pragma once
+
+#include <type_traits>
+#include <unordered_set>
+#include "storm/adapters/CarlAdapter.h"
+#include "storm/models/sparse/Dtmc.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;
+
+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);
+
+};
+
+
+    }
+}

src/storm/cli/entrypoints.h

@@ -1,10 +1,10 @@
-#ifndef STORM_ENTRYPOINTS_H_H
-#define STORM_ENTRYPOINTS_H_H
+#pragma once
 
 #include <type_traits>
 
 #include "storm/utility/storm.h"
 
+#include "storm/analysis/GraphConditions.h"
 #include "storm/storage/SymbolicModelDescription.h"
 #include "storm/utility/DirectEncodingExporter.h"
 #include "storm/utility/Stopwatch.h"
@@ -112,7 +112,7 @@ namespace storm {
                 }
 
                 if (storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultToFile()) {
-                    exportParametricResultToFile(result->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()], storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector(*(model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>())), storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultPath());
+                    exportParametricResultToFile(result->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()], storm::analysis::ConstraintCollector<storm::RationalFunction>(*(model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>())), storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultPath());
                 }
             }
         }
@@ -469,5 +469,3 @@ namespace storm {
 
     }
 }
-
-#endif //STORM_ENTRYPOINTS_H_H

src/storm/models/sparse/Dtmc.cpp

@@ -25,47 +25,7 @@ namespace storm {
                 STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
             }
             
-#ifdef STORM_HAVE_CARL
-            template <typename ValueType, typename RewardModelType>
-            Dtmc<ValueType, RewardModelType>::ConstraintCollector::ConstraintCollector(Dtmc<ValueType> const& dtmc) {
-                process(dtmc);
-            }
-            
-            template <typename ValueType, typename RewardModelType>
-            std::unordered_set<storm::ArithConstraint<ValueType>> const& Dtmc<ValueType, RewardModelType>::ConstraintCollector::getWellformedConstraints() const {
-                return this->wellformedConstraintSet;
-            }
-            
-            template <typename ValueType, typename RewardModelType>
-            std::unordered_set<storm::ArithConstraint<ValueType>> const& Dtmc<ValueType, RewardModelType>::ConstraintCollector::getGraphPreservingConstraints() const {
-                return this->graphPreservingConstraintSet;
-            }
-            
-            template <typename ValueType, typename RewardModelType>
-            void Dtmc<ValueType, RewardModelType>::ConstraintCollector::process(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
-                for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) {
-                    ValueType sum = storm::utility::zero<ValueType>();
-                    for (auto const& transition : dtmc.getRows(state)) {
-                        sum += transition.getValue();
-                        if (!storm::utility::isConstant(transition.getValue())) {
-                            wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ);
-                            wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ);
-                            graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GREATER);
-                        }
-                    }
-                    STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1.");
-                    if(!storm::utility::isConstant(sum)) {
-                        wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ);
-                    }
-                    
-                }
-            }
-            
-            template <typename ValueType, typename RewardModelType>
-            void Dtmc<ValueType, RewardModelType>::ConstraintCollector::operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
-                process(dtmc);
-            }
-#endif
+
             
             template class Dtmc<double>;
             template class Dtmc<float>;

src/storm/models/sparse/Dtmc.h

@@ -1,10 +1,7 @@
 #ifndef STORM_MODELS_SPARSE_DTMC_H_
 #define STORM_MODELS_SPARSE_DTMC_H_
-#include <unordered_set>
 
 #include "storm/models/sparse/DeterministicModel.h"
-#include "storm/utility/OsDetection.h"
-#include "storm/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace models {
@@ -47,56 +44,7 @@ namespace storm {
                 Dtmc(Dtmc<ValueType, RewardModelType>&& dtmc) = default;
                 Dtmc& operator=(Dtmc<ValueType, RewardModelType>&& dtmc) = default;
 
-                
-#ifdef STORM_HAVE_CARL
-                class ConstraintCollector {
-                private:
-                    // A set of constraints that says that the DTMC actually has valid probability distributions in all states.
-                    std::unordered_set<storm::ArithConstraint<ValueType>> 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<storm::ArithConstraint<ValueType>> graphPreservingConstraintSet;
-                    
-                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<storm::ArithConstraint<ValueType>> const&  getWellformedConstraints() const;
-                    
-                    /*!
-                     * Returns the set of graph-preserving constraints.
-                     *
-                     * @return The set of graph-preserving constraints.
-                     */
-                    std::unordered_set<storm::ArithConstraint<ValueType>> 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);
-                    
-                };
-#endif
+
             };
             
         } // namespace sparse

src/storm/utility/storm.h

@@ -93,6 +93,9 @@
 #include "storm/generator/PrismNextStateGenerator.h"
 #include "storm/generator/JaniNextStateGenerator.h"
 
+#include "storm/analysis/GraphConditions.h"
+
+
 // Headers related to exception handling.
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
@@ -580,19 +583,22 @@ namespace storm {
         return result;
     }
     
-    inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
+    inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector<storm::RationalFunction> const& constraintCollector, std::string const& path) {
         std::ofstream filestream;
         storm::utility::openFile(path, filestream);
-        // TODO: add checks.
         filestream << "!Parameters: ";
         std::set<storm::RationalFunctionVariable> vars = result.gatherVariables();
         std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
         filestream << std::endl;
         filestream << "!Result: " << result << std::endl;
         filestream << "!Well-formed Constraints: " << std::endl;
-        std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
+        std::vector<std::string> stringConstraints;
+        std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) ->  std::string { return c.toString();});
+        std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
         filestream << "!Graph-preserving Constraints: " << std::endl;
-        std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
+        stringConstraints.clear();
+        std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) ->  std::string { return c.toString();});
+        std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
         storm::utility::closeFile(filestream);
     }