From 728dc9e8a43bc41ac2a05f31b1b7790e6b956291 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 7 Sep 2018 09:29:47 +0200 Subject: [PATCH] Fix TODO --- src/storm-pars/analysis/Lattice.cpp | 122 ++++++++++++++-------------- src/storm-pars/analysis/Lattice.h | 7 +- 2 files changed, 64 insertions(+), 65 deletions(-) diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index c9b05dc0a..1846b816e 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -3,6 +3,7 @@ // #include +#include #include "Lattice.h" namespace storm { namespace analysis { @@ -100,36 +101,37 @@ namespace storm { addBetween(state, top, bottom); } - void Lattice::addRelation(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node *between, - storm::analysis::Lattice::Node *below) { - above->below.insert(between); - between->above.insert(above); - between->below.insert(below); - below->above.insert(between); - } - void Lattice::addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below) { - above->below.insert(below); - below->above.insert(above); + if (above != below) { + above->below.insert(below); + below->above.insert(above); + } } int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { Node *node1 = getNode(state1); Node *node2 = getNode(state2); - // TODO: Wat als above(node1, node2) en above(node2, node1), dan moeten ze samengevoegd? + return compare(node1, node2); + } + + int Lattice::compare(Node* node1, Node* node2) { if (node1 != nullptr && node2 != nullptr) { if (node1 == node2) { return SAME; } - std::set* seen1 = new std::set({}); - if (above(node1, node2, seen1)) { + bool isAbove = above(node1, node2, new std::set({})); + bool isBelow = above(node2, node1, new std::set({})); + if (isAbove && isBelow) { + return SAME; + } + + if (isAbove) { return ABOVE; } - std::set* seen2 = new std::set({}); - if (above(node2, node1, seen2)) { + if (isBelow) { return BELOW; } } @@ -137,6 +139,7 @@ namespace storm { return UNKNOWN; } + Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) { return nodes.at(stateNumber); } @@ -153,7 +156,6 @@ namespace storm { return nodes; } - storm::storage::BitVector Lattice::getAddedStates() { return addedStates; } @@ -178,21 +180,21 @@ namespace storm { out << " Address: " << node << "\n"; out << " Above: {"; - for (auto itr2 = node->above.begin(); itr2 != node->above.end(); ++itr2) { - Node *above = *itr2; - index = above->states.getNextSetIndex(0); - out << "{"; - while (index < numberOfStates) { - out << index; - index = above->states.getNextSetIndex(index + 1); - if (index < numberOfStates) { - out << ", "; - } + for (auto itr2 = node->above.begin(); itr2 != node->above.end(); ++itr2) { + Node *above = *itr2; + index = above->states.getNextSetIndex(0); + out << "{"; + while (index < numberOfStates) { + out << index; + index = above->states.getNextSetIndex(index + 1); + if (index < numberOfStates) { + out << ", "; } - - out << "}"; } - out << "}" << "\n"; + + out << "}"; + } + out << "}" << "\n"; out << " Below: {"; @@ -216,45 +218,43 @@ namespace storm { } void Lattice::toDotFile(std::ostream &out) { - // TODO: op de een of andere manier ontstaan er nodes die nergens eindigen/beginnen - out << "digraph \"Lattice\" {" << std::endl; - - // print all nodes - std::vector printed; - out << "\t" << "node [shape=ellipse]" << std::endl; - for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { - - if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) { - out << "\t\"" << (*itr) << "\" [label = \""; - uint_fast64_t index = (*itr)->states.getNextSetIndex(0); - while (index < numberOfStates) { - out << index; - index = (*itr)->states.getNextSetIndex(index + 1); - if (index < numberOfStates) { - out << ", "; + out << "digraph \"Lattice\" {" << std::endl; + + // print all nodes + std::vector printed; + out << "\t" << "node [shape=ellipse]" << std::endl; + for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { + + if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) { + out << "\t\"" << (*itr) << "\" [label = \""; + uint_fast64_t index = (*itr)->states.getNextSetIndex(0); + while (index < numberOfStates) { + out << index; + index = (*itr)->states.getNextSetIndex(index + 1); + if (index < numberOfStates) { + out << ", "; + } } - } - out << "\"]" << std::endl; - printed.push_back(*itr); + out << "\"]" << std::endl; + printed.push_back(*itr); + } } - } - // print arcs - printed.clear(); - for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { - if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) { - auto below = (*itr)->below; - for (auto itr2 = below.begin(); itr2 != below.end(); ++itr2) { - out << "\t\"" << (*itr) << "\" -> \"" << (*itr2) << "\";" << std::endl; + // print arcs + printed.clear(); + for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { + if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) { + auto below = (*itr)->below; + for (auto itr2 = below.begin(); itr2 != below.end(); ++itr2) { + out << "\t\"" << (*itr) << "\" -> \"" << (*itr2) << "\";" << std::endl; + } + printed.push_back(*itr); } - printed.push_back(*itr); } - } - - out << "}" << std::endl; - } + out << "}" << std::endl; + } bool Lattice::above(Node *node1, Node *node2, std::set* seenNodes) { bool result = !node1->below.empty() && std::find(node1->below.begin(), node1->below.end(), node2) != node1->below.end(); diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 806c1b6e7..a62d2763f 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -55,13 +55,10 @@ namespace storm { void add(uint_fast64_t state); /*! - * Adds a new relation to the lattice + * Adds a new relation between two nodes to the lattice * @param above The node closest to the top Node of the Lattice. - * @param between The node between above and below. * @param below The node closest to the bottom Node of the Lattice. */ - void addRelation(Node* above, Node* between, Node* below); - void addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below); /*! @@ -137,6 +134,8 @@ namespace storm { * @return */ bool above(Node * node1, Node * node2, std::set* seenNodes); + + int compare(Node* node1, Node* node2); }; } }