From 8fbc8d56c0f91b50e59cb0faafa7ad7fe0f6c384 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 6 Feb 2019 23:01:22 +0100
Subject: [PATCH] graph preservation properties correctly computed for CTMCs

---
 src/storm-pars-cli/storm-pars.cpp      |  5 ++
 src/storm/analysis/GraphConditions.cpp | 75 +++++++++++++++++---------
 2 files changed, 54 insertions(+), 26 deletions(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index b001381b7..6b3763321 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -375,6 +375,11 @@ namespace storm {
                                                     boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
                                                     storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
                                                 }
+                                                else if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Ctmc)) {
+                                                    auto ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
+                                                    boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
+                                                    storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*ctmc), parametricSettings.exportResultPath());
+                                                }
                                             });
             } else {
                 STORM_LOG_TRACE("Sampling the model at given points.");
diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp
index c11fccb0b..8fa6c194a 100644
--- a/src/storm/analysis/GraphConditions.cpp
+++ b/src/storm/analysis/GraphConditions.cpp
@@ -56,47 +56,70 @@ namespace storm {
 
         template <typename ValueType>
         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 transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
-                    auto const& transition = *transitionIt;
-                    sum += transition.getValue();
-                    if (!storm::utility::isConstant(transition.getValue())) {
-                        auto const& transitionVars = transition.getValue().gatherVariables();
-                        variableSet.insert(transitionVars.begin(), transitionVars.end());
-                        // Assert: 0 <= transition <= 1
+
+            if (model.getType() != storm::models::ModelType::Ctmc) {
+
+                for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) {
+                    ValueType sum = storm::utility::zero<ValueType>();
+
+                    for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
+                        auto const& transition = *transitionIt;
+                        sum += transition.getValue();
+                        if (!storm::utility::isConstant(transition.getValue())) {
+                            auto const& transitionVars = transition.getValue().gatherVariables();
+                            variableSet.insert(transitionVars.begin(), transitionVars.end());
+                            // Assert: 0 <= transition <= 1
+                            if (transition.getValue().denominator().isConstant()) {
+                                assert(transition.getValue().denominator().constantPart() != 0);
+                                if (transition.getValue().denominator().constantPart() > 0) {
+                                    // Assert: nom <= denom
+                                    wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ);
+                                    // Assert: nom >= 0
+                                    wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
+                                } else if (transition.getValue().denominator().constantPart() < 0) {
+                                    // Assert nom >= denom
+                                    wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ);
+                                    // Assert: nom <= 0
+                                    wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
+                                } else {
+                                    STORM_LOG_ASSERT(false, "Denominator must not equal 0.");
+                                }
+                            } else {
+                                // Assert: denom != 0
+                                wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
+                                 // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0
+                                wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
+                                 // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0
+                            }
+                            // Assert: transition > 0
+                            graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), 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)) {
+                        // Assert: sum == 1
+                        wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
+                    }
+                }
+            } else {
+                for (auto const& transition : model.getTransitionMatrix()) {
+                    if(!transition.getValue().isConstant()) {
                         if (transition.getValue().denominator().isConstant()) {
                             assert(transition.getValue().denominator().constantPart() != 0);
                             if (transition.getValue().denominator().constantPart() > 0) {
-                                // Assert: nom <= denom
-                                wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ);
-                                // Assert: nom >= 0
                                 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
                             } else if (transition.getValue().denominator().constantPart() < 0) {
-                                // Assert nom >= denom
-                                wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ);
-                                // Assert: nom <= 0
                                 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
                             } else {
-                                STORM_LOG_ASSERT(false, "Denominator must not equal 0.");
+                                assert(false); // Should fail before.
                             }
                         } else {
-                            // Assert: denom != 0
                             wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
-                             // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0
                             wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
-                             // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0
                         }
-                        // Assert: transition > 0
                         graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), 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)) {
-                    // Assert: sum == 1
-                    wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
-                }
             }
 
             if (model.getType() == storm::models::ModelType::Ctmc) {