From 23edcc1a75dda2d7057178870c219401e40a3cb4 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Tue, 18 Sep 2018 17:38:20 +0200
Subject: [PATCH] Refactor AssumptionChecker

---
 src/storm-pars/analysis/AssumptionChecker.cpp | 82 +++++++++----------
 1 file changed, 41 insertions(+), 41 deletions(-)

diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp
index c3014d3a9..1ed16f149 100644
--- a/src/storm-pars/analysis/AssumptionChecker.cpp
+++ b/src/storm-pars/analysis/AssumptionChecker.cpp
@@ -88,54 +88,54 @@ namespace storm {
                                 storm::exceptions::NotSupportedException,
                                 "Only Greater Or Equal assumptions supported");
 
-                auto val1 = std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName());
-                auto val2 = std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName());
-                auto row1 = matrix.getRow(val1);
-                auto row2 = matrix.getRow(val2);
-                if (row1.getNumberOfEntries() != 2 && row2.getNumberOfEntries() != 2) {
-                    assert (false);
-                }
-
-                auto succ11 = row1.begin();
-                auto succ12 = (++row1.begin());
-                auto succ21 = row2.begin();
-                auto succ22 = (++row2.begin());
+                auto row1 = matrix.getRow(std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()));
+                auto row2 = matrix.getRow(std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()));
 
-                if (succ12->getColumn() == succ21->getColumn() && succ11->getColumn() == succ22->getColumn()) {
-                    auto temp = succ12;
-                    succ12 = succ11;
-                    succ11 = temp;
-                }
+                // Only implemented for two successors
+                if (row1.getNumberOfEntries() == 2 && row2.getNumberOfEntries() == 2) {
+                    auto succ1State1 = row1.begin();
+                    auto succ2State1 = (++row1.begin());
+                    auto succ1State2 = row2.begin();
+                    auto succ2State2 = (++row2.begin());
 
-                if (succ11->getColumn() == succ21->getColumn() && succ12->getColumn() == succ22->getColumn()) {
-                    ValueType prob;
-                    auto comp = lattice->compare(succ11->getColumn(), succ12->getColumn());
-                    if (comp == storm::analysis::Lattice::ABOVE) {
-                        prob = succ11->getValue() - succ21->getValue();
-                    } else if (comp == storm::analysis::Lattice::BELOW) {
-                        prob = succ12->getValue() - succ22->getValue();
+                    if (succ1State1->getColumn() == succ2State2->getColumn()
+                            && succ1State2->getColumn() == succ2State1->getColumn()) {
+                        // swap them
+                        auto temp = succ2State1;
+                        succ2State1 = succ1State1;
+                        succ1State1 = temp;
                     }
-                    auto vars = prob.gatherVariables();
-                    // TODO: Type
-                    std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> substitutions;
-                    for (auto var:vars) {
-                        auto derivative = prob.derivative(var);
-                        assert(derivative.isConstant());
-                        if (derivative.constantPart() >= 0) {
-                            substitutions[var] = 0;
-                        } else if (derivative.constantPart() <= 0) {
-                            substitutions[var] = 1;
+
+                    if (succ1State1->getColumn() == succ1State2->getColumn() && succ2State1->getColumn() == succ2State2->getColumn()) {
+                        ValueType prob;
+                        auto comp = lattice->compare(succ1State1->getColumn(), succ2State1->getColumn());
+                        if (comp == storm::analysis::Lattice::ABOVE) {
+                            prob = succ1State1->getValue() - succ1State2->getValue();
+                        } else if (comp == storm::analysis::Lattice::BELOW) {
+                            prob = succ2State1->getValue() - succ2State2->getValue();
+                        }
+                        auto vars = prob.gatherVariables();
+                        // TODO: Type
+                        std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> substitutions;
+                        for (auto var:vars) {
+                            auto derivative = prob.derivative(var);
+                            assert(derivative.isConstant());
+                            if (derivative.constantPart() >= 0) {
+                                substitutions[var] = 0;
+                            } else if (derivative.constantPart() <= 0) {
+                                substitutions[var] = 1;
+                            }
                         }
+                        result = prob.evaluate(substitutions) >= 0;
+                    }
+
+                    if (result) {
+                        validatedAssumptions.insert(assumption);
+                    } else {
+                        STORM_LOG_DEBUG("Could not validate: " << *assumption << std::endl);
                     }
-                    result = prob.evaluate(substitutions) >= 0;
-                }
-                if (result) {
-                    validatedAssumptions.insert(assumption);
-                } else {
-                    STORM_PRINT("Could not validate: " << *assumption << std::endl);
                 }
             }
-
             return result;
         }