Refactor AssumptionChecker

src/storm-pars/analysis/AssumptionChecker.cpp

@@ -88,32 +88,31 @@ 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 row1 = matrix.getRow(std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()));
+                auto row2 = matrix.getRow(std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()));
 
-                auto succ11 = row1.begin();
-                auto succ12 = (++row1.begin());
-                auto succ21 = row2.begin();
-                auto succ22 = (++row2.begin());
+                // 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 (succ12->getColumn() == succ21->getColumn() && succ11->getColumn() == succ22->getColumn()) {
-                    auto temp = succ12;
-                    succ12 = succ11;
-                    succ11 = temp;
+                    if (succ1State1->getColumn() == succ2State2->getColumn()
+                            && succ1State2->getColumn() == succ2State1->getColumn()) {
+                        // swap them
+                        auto temp = succ2State1;
+                        succ2State1 = succ1State1;
+                        succ1State1 = temp;
                     }
 
-                if (succ11->getColumn() == succ21->getColumn() && succ12->getColumn() == succ22->getColumn()) {
+                    if (succ1State1->getColumn() == succ1State2->getColumn() && succ2State1->getColumn() == succ2State2->getColumn()) {
                         ValueType prob;
-                    auto comp = lattice->compare(succ11->getColumn(), succ12->getColumn());
+                        auto comp = lattice->compare(succ1State1->getColumn(), succ2State1->getColumn());
                         if (comp == storm::analysis::Lattice::ABOVE) {
-                        prob = succ11->getValue() - succ21->getValue();
+                            prob = succ1State1->getValue() - succ1State2->getValue();
                         } else if (comp == storm::analysis::Lattice::BELOW) {
-                        prob = succ12->getValue() - succ22->getValue();
+                            prob = succ2State1->getValue() - succ2State2->getValue();
                         }
                         auto vars = prob.gatherVariables();
                         // TODO: Type
@@ -129,13 +128,14 @@ namespace storm {
                         }
                         result = prob.evaluate(substitutions) >= 0;
                     }
+
                     if (result) {
                         validatedAssumptions.insert(assumption);
                     } else {
-                    STORM_PRINT("Could not validate: " << *assumption << std::endl);
+                        STORM_LOG_DEBUG("Could not validate: " << *assumption << std::endl);
+                    }
                 }
             }
-
             return result;
         }