diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 87db8a666..dbf2c0964 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -82,7 +82,8 @@ namespace storm { void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) { assert(!addedStates[state]); - assert(compare(above, below) == ABOVE); + auto res = compare(above, below); + assert(res == ABOVE || res == UNKNOWN); Node *newNode = new Node(); newNode->states = storm::storage::BitVector(numberOfStates); newNode->states.set(state); diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index a26713fa7..7765dc8ed 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -94,7 +94,10 @@ namespace storm { auto row = matrix.getRow(i); for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { - stateMap[i].set(rowItr->getColumn(), true); + // ignore self-loops when there are more transitions + if (i != rowItr->getColumn() || row.getNumberOfEntries() == 1) { + stateMap[i].set(rowItr->getColumn(), true); + } } } @@ -154,7 +157,10 @@ namespace storm { // Check if current state has not been added yet, and all successors have bool check = !seenStates[stateNumber]; for (auto succIndex = successors.getNextSetIndex(0); check && succIndex != numberOfStates; succIndex = successors.getNextSetIndex(++succIndex)) { - check &= seenStates[succIndex]; + if (succIndex != stateNumber) { + check &= seenStates[succIndex]; + } + // if the stateNumber equals succIndex we have a self-loop } if (check && successors.getNumberOfSetBits() == 1) {