Change vector to set, add error message if more than two successors for one state, add documentation

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<Node *>(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<Node *>({above});
-            newNode->below = std::vector<Node *>({below});
-            remove(&(below->above), above);
-            remove(&(above->below), below);
-            (below->above).push_back(newNode);
-            above->below.push_back(newNode);
+            newNode->above = std::set<Node *>({above});
+            newNode->below = std::set<Node *>({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<Node *> *nodes, Node *node) {
-            auto index = std::find(nodes->begin(), nodes->end(), node);
-            if (index != nodes->end()) {
-                nodes->erase(index);
-            }
-        };
-
         void Lattice::setStates(std::vector<uint_fast64_t> states, Node *node) {
             for (auto itr = states.begin(); itr < states.end(); ++itr) {
                 node->states.set(*itr);

src/storm-pars/analysis/Lattice.h

@@ -26,8 +26,8 @@ namespace storm {
                 public:
                     struct Node {
                         storm::storage::BitVector states;
-                        std::vector<Node *> above;
-                        std::vector<Node *> below;
+                        std::set<Node *> above;
+                        std::set<Node *> 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<Node *> *nodes, Node *node);
-
                     void setStates(std::vector<uint_fast64_t>  states, Node *node);
 
                 };