Browse Source

Fix adding same state twice to Order

tempestpy_adaptions
Jip Spel 5 years ago
parent
commit
32e3661bd2
  1. 11
      src/storm-pars/analysis/OrderExtender.cpp

11
src/storm-pars/analysis/OrderExtender.cpp

@ -196,8 +196,19 @@ namespace storm {
order->addBetween(max, order->getTop(), order->getNode(min)); order->addBetween(max, order->getTop(), order->getNode(min));
} }
assert (order->compare(max, min) == Order::ABOVE); assert (order->compare(max, min) == Order::ABOVE);
if (order->contains(state)) {
if (order->compare(max, state) == Order::UNKNOWN) {
order->addRelation(max, state);
}
if (order->compare(state, min) == Order::UNKNOWN) {
order->addRelation(state, min);
}
} else {
order->addBetween(state, max, min); order->addBetween(state, max, min);
} }
assert (order->compare(max, state) == Order::ABOVE);
assert (order->compare(state, min) == Order::ABOVE);
}
} }
} }
} }

Loading…
Cancel
Save