diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 1c4fe63c7..4bc2819ca 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -8,13 +8,12 @@ namespace storm { namespace analysis { Lattice::Lattice(storm::storage::BitVector topStates, storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates) { - top = new Node(); top->states = topStates; bottom = new Node(); bottom->states = bottomStates; - top->below.push_back(bottom); - bottom->above.push_back(top); + top->below.insert(bottom); + bottom->above.insert(top); nodes = std::vector(numberOfStates); for (auto i = topStates.getNextSetIndex(0); i < numberOfStates; i = topStates.getNextSetIndex(i+1)) { @@ -32,12 +31,12 @@ namespace storm { Node *newNode = new Node(); newNode->states = storm::storage::BitVector(numberOfStates); newNode->states.set(state); - newNode->above = std::vector({above}); - newNode->below = std::vector({below}); - remove(&(below->above), above); - remove(&(above->below), below); - (below->above).push_back(newNode); - above->below.push_back(newNode); + newNode->above = std::set({above}); + newNode->below = std::set({below}); + below->above.erase(above); + above->below.erase(below); + (below->above).insert(newNode); + above->below.insert(newNode); nodes.at(state) = newNode; } @@ -107,7 +106,7 @@ namespace storm { } out << "}"; - if (itr2 + 1 != node->above.end()) { + if ((++itr2) != node->above.end()) { out << ", "; } } @@ -127,7 +126,7 @@ namespace storm { } out << "}"; - if (itr2 + 1 != node->below.end()) { + if ((++itr2) != node->below.end()) { out << ", "; } } @@ -184,13 +183,6 @@ namespace storm { return result; } - void Lattice::remove(std::vector *nodes, Node *node) { - auto index = std::find(nodes->begin(), nodes->end(), node); - if (index != nodes->end()) { - nodes->erase(index); - } - }; - void Lattice::setStates(std::vector states, Node *node) { for (auto itr = states.begin(); itr < states.end(); ++itr) { node->states.set(*itr); diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 8324a75d2..643dc16b6 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -26,8 +26,8 @@ namespace storm { public: struct Node { storm::storage::BitVector states; - std::vector above; - std::vector below; + std::set above; + std::set below; }; /*! @@ -83,12 +83,17 @@ namespace storm { Node *getNode(uint_fast64_t state); /*! - * Prints a string representation of the lattice to std::cout. + * Prints a string representation of the lattice to the output stream. * * @param out The stream to output to. */ void toString(std::ostream &out); + /*! + * Prints a dot representation of the lattice to the output stream. + * + * @param out The stream to output to. + */ void toDotFile(std::ostream &out); /*! @@ -136,11 +141,14 @@ namespace storm { state->stateNumber = i; auto row = matrix.getRow(i); - //TODO assert that there are at most two successors + + if ((*(row.begin())).getValue() != ValueType(1)) { + STORM_LOG_THROW((row.begin() + 2) == row.end(), storm::exceptions::NotSupportedException, "Only two outgoing transitions per state allowed"); state->successor1 = (*(row.begin())).getColumn(); state->successor2 = (*(++row.begin())).getColumn(); } else { + state-> successor1 = (*(row.begin())).getColumn(); state-> successor2 = (*(row.begin())).getColumn(); } @@ -169,20 +177,19 @@ namespace storm { uint_fast64_t successor1 = currentState->successor1; uint_fast64_t successor2 = currentState->successor2; int compareResult = lattice->compare(successor1, successor2); + Node* node1 = lattice->getNode(successor1); + Node* node2 = lattice->getNode(successor2); if (compareResult == 1) { // successor 1 is closer to top than successor 2 lattice->addBetween(currentState->stateNumber, lattice->getNode(successor1), lattice->getNode(successor2)); - // Add stateNumber to the set with seen states. } else if (compareResult == 2) { // successor 2 is closer to top than successor 1 lattice->addBetween(currentState->stateNumber, lattice->getNode(successor2), lattice->getNode(successor1)); - // Add stateNumber to the set with seen states. } else if (compareResult == 0) { // the successors are at the same level lattice->addToNode(currentState->stateNumber, lattice->getNode(successor1)); - // Add stateNumber to the set with seen states. } else { // TODO: is this what we want? lattice->add(currentState->stateNumber); @@ -213,8 +220,6 @@ namespace storm { bool above(Node *, Node *); - void remove(std::vector *nodes, Node *node); - void setStates(std::vector states, Node *node); };