Browse Source

Fixed TerminalStatesGetter with multi-bounded formulae.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
871efc0d8c
No known key found for this signature in database GPG Key ID: 6EDE19592731EEC3
  1. 2
      src/storm/builder/TerminalStatesGetter.cpp

2
src/storm/builder/TerminalStatesGetter.cpp

@ -26,7 +26,7 @@ namespace storm {
} else if (left.isAtomicLabelFormula()) { } else if (left.isAtomicLabelFormula()) {
terminalLabelCallback(left.asAtomicLabelFormula().getLabel(), false); terminalLabelCallback(left.asAtomicLabelFormula().getLabel(), false);
} }
} else if (formula.isBoundedUntilFormula()) {
} else if (formula.isBoundedUntilFormula() && !formula.asBoundedUntilFormula().hasMultiDimensionalSubformulas()) {
storm::logic::BoundedUntilFormula const& boundedUntil = formula.asBoundedUntilFormula(); storm::logic::BoundedUntilFormula const& boundedUntil = formula.asBoundedUntilFormula();
bool hasLowerBound = false; bool hasLowerBound = false;
for (uint64_t i = 0; i < boundedUntil.getDimension(); ++i) { for (uint64_t i = 0; i < boundedUntil.getDimension(); ++i) {

Loading…
Cancel
Save