diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index a62d2763f..42a4802cb 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -75,20 +75,41 @@ namespace storm { /*! * Retrieves the pointer to a Node at which the state occurs. - * Behaviour unknown when state does not exists at any Node in the Lattice. * * @param state The number of the state. * - * @return The pointer to the node of the state, nullptr if the node does not exist + * @return The pointer to the node of the state, nullptr if the node does not exist. */ Node *getNode(uint_fast64_t state); + /*! + * Retrieves the top node of the lattice. + * + * @return The top node. + */ Node* getTop(); + /*! + * Retrieves the bottom node of the lattice. + * + * @return The bottom node. + */ Node* getBottom(); + /*! + * Returns the vector with the nodes of the lattice. + * Each index in the vector refers to a state. + * When the state is not yet added at a node, it will contain the nullptr. + * + * @return The vector with nodes of the lattice. + */ std::vector getNodes(); + /*! + * Returns a BitVector in which all added states are set. + * + * @return The BitVector with all added states. + */ storm::storage::BitVector getAddedStates(); /*! @@ -105,6 +126,9 @@ namespace storm { */ void toDotFile(std::ostream &out); + /*! + * Constants for comparison of nodes/states + */ static const int UNKNOWN = -1; static const int BELOW = 2; static const int ABOVE = 1; @@ -126,13 +150,6 @@ namespace storm { uint_fast64_t numberOfStates; - /** - * Check if node1 lies above node2 - * @param node1 - * @param node2 - * @param seenNodes - * @return - */ bool above(Node * node1, Node * node2, std::set* seenNodes); int compare(Node* node1, Node* node2);