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 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 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; }