Browse Source

JaniTraverser: Only traverse lower/upper bound expressions of BoundedIntegerVariables, if these bounds exists.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
20d424e289
  1. 8
      src/storm/storage/jani/FunctionEliminator.cpp
  2. 16
      src/storm/storage/jani/traverser/JaniTraverser.cpp

8
src/storm/storage/jani/FunctionEliminator.cpp

@ -334,8 +334,12 @@ namespace storm {
if (variable.hasInitExpression()) {
variable.setInitExpression(functionEliminationVisitor->eliminate(variable.getInitExpression()));
}
variable.setLowerBound(functionEliminationVisitor->eliminate(variable.getLowerBound()));
variable.setUpperBound(functionEliminationVisitor->eliminate(variable.getUpperBound()));
if (variable.hasLowerBound()) {
variable.setLowerBound(functionEliminationVisitor->eliminate(variable.getLowerBound()));
}
if (variable.hasUpperBound()) {
variable.setUpperBound(functionEliminationVisitor->eliminate(variable.getUpperBound()));
}
}
void traverse(UnboundedIntegerVariable& variable, boost::any const& data) override {

16
src/storm/storage/jani/traverser/JaniTraverser.cpp

@ -95,8 +95,12 @@ namespace storm {
if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data);
}
traverse(variable.getLowerBound(), data);
traverse(variable.getUpperBound(), data);
if (variable.hasLowerBound()) {
traverse(variable.getLowerBound(), data);
}
if (variable.hasUpperBound()) {
traverse(variable.getUpperBound(), data);
}
}
void JaniTraverser::traverse(UnboundedIntegerVariable& variable, boost::any const& data) {
@ -276,8 +280,12 @@ namespace storm {
if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data);
}
traverse(variable.getLowerBound(), data);
traverse(variable.getUpperBound(), data);
if (variable.hasLowerBound()) {
traverse(variable.getLowerBound(), data);
}
if (variable.hasUpperBound()) {
traverse(variable.getUpperBound(), data);
}
}
void ConstJaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) {

Loading…
Cancel
Save