Browse Source
Counterexamples:making minimal label set generator aware of unbounded integer variables
tempestpy_adaptions
Tim Quatmann
4 years ago
No known key found for this signature in database
GPG Key ID: 6EDE19592731EEC3
1 changed files with
2 additions and
4 deletions
-
src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
|
|
|
@ -423,13 +423,11 @@ namespace storm { |
|
|
|
|
|
|
|
// Then add the constraints for bounds of the integer variables. |
|
|
|
for (auto const& integerVariable : program.getGlobalIntegerVariables()) { |
|
|
|
localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression()); |
|
|
|
localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression()); |
|
|
|
localSolver->add(integerVariable.getRangeExpression()); |
|
|
|
} |
|
|
|
for (auto const& module : program.getModules()) { |
|
|
|
for (auto const& integerVariable : module.getIntegerVariables()) { |
|
|
|
localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression()); |
|
|
|
localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression()); |
|
|
|
localSolver->add(integerVariable.getRangeExpression()); |
|
|
|
} |
|
|
|
} |
|
|
|
} else { |
|
|
|
|
