From c0aa6eefa38f97f99899e76b47f83ecad8270214 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Wed, 15 May 2019 12:02:21 +0200 Subject: [PATCH] Clean up Lattice --- src/storm-pars/analysis/AssumptionChecker.cpp | 17 +- src/storm-pars/analysis/AssumptionChecker.h | 4 - src/storm-pars/analysis/Lattice.cpp | 62 +----- src/storm-pars/analysis/Lattice.h | 82 ++++--- .../analysis/LatticeExtenderTest.cpp | 15 +- src/test/storm-pars/analysis/LatticeTest.cpp | 201 +++++++++--------- 6 files changed, 155 insertions(+), 226 deletions(-) diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index 747b85874..3aca39f31 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -1,6 +1,3 @@ -// -// Created by Jip Spel on 12.09.18. -// #include #include "AssumptionChecker.h" @@ -166,7 +163,7 @@ namespace storm { if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) { if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Greater - && lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()) != Lattice::UNKNOWN) { + && lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()) != Lattice::NodeComparison::UNKNOWN) { // The assumption should be the greater assumption // If the result is unknown, we cannot compare, also SMTSolver will not help result = validateAssumptionFunction(lattice, state1succ1, state1succ2, state2succ1, @@ -206,10 +203,10 @@ namespace storm { // Calculate the difference in probability for the "highest" successor state ValueType prob; auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()); - assert (comp == Lattice::ABOVE || comp == Lattice::BELOW); - if (comp == Lattice::ABOVE) { + assert (comp == Lattice::NodeComparison::ABOVE || comp == Lattice::NodeComparison::BELOW); + if (comp == Lattice::NodeComparison::ABOVE) { prob = state1succ1->getValue() - state2succ1->getValue(); - } else if (comp == Lattice::BELOW) { + } else if (comp == Lattice::NodeComparison::BELOW) { prob = state1succ2->getValue() - state2succ2->getValue(); } @@ -266,13 +263,13 @@ namespace storm { stateVariables.insert(manager->declareRationalVariable(varname2)); } auto comp = lattice->compare(itr1->getColumn(), itr2->getColumn()); - if (comp == Lattice::ABOVE) { + if (comp == Lattice::NodeComparison::ABOVE) { exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) <= manager->getVariable(varname2)); - } else if (comp == Lattice::BELOW) { + } else if (comp == Lattice::NodeComparison::BELOW) { exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) >= manager->getVariable(varname2)); - } else if (comp == Lattice::SAME) { + } else if (comp == Lattice::NodeComparison::SAME) { exprOrderSucc = exprOrderSucc && (manager->getVariable(varname1) = manager->getVariable(varname2)); } else { diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h index b7746000f..3f98189ae 100644 --- a/src/storm-pars/analysis/AssumptionChecker.h +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -1,7 +1,3 @@ -// -// Created by Jip Spel on 12.09.18. -// - #ifndef STORM_ASSUMPTIONCHECKER_H #define STORM_ASSUMPTIONCHECKER_H diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 665d39537..c585bb000 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -1,7 +1,3 @@ -// -// Created by Jip Spel on 24.07.18. -// - #include #include #include "Lattice.h" @@ -24,7 +20,6 @@ namespace storm { top->statesAbove = storm::storage::BitVector(numberOfStates); bottom->statesAbove = storm::storage::BitVector(numberOfStates); - for (auto const& i : *topStates) { addedStates->set(i); bottom->statesAbove.set(i); @@ -116,15 +111,11 @@ namespace storm { assert (compare(above, below) == ABOVE); } - void Lattice::addRelation(uint_fast64_t above, uint_fast64_t below) { - addRelationNodes(getNode(above), getNode(below)); - } - - int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { + Lattice::NodeComparison Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { return compare(getNode(state1), getNode(state2)); } - int Lattice::compare(Node* node1, Node* node2) { + Lattice::NodeComparison Lattice::compare(Node* node1, Node* node2) { if (node1 != nullptr && node2 != nullptr) { if (node1 == node2) { return SAME; @@ -185,7 +176,6 @@ namespace storm { } std::vector Lattice::sortStates(storm::storage::BitVector* states) { - // TODO improve auto numberOfSetBits = states->getNumberOfSetBits(); auto stateSize = states->size(); auto result = std::vector(numberOfSetBits, stateSize); @@ -201,7 +191,7 @@ namespace storm { added = true; } else { auto compareRes = compare(state, result[i]); - if (compareRes == Lattice::ABOVE) { + if (compareRes == ABOVE) { auto temp = result[i]; result[i] = state; for (auto j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) { @@ -210,9 +200,9 @@ namespace storm { temp = temp2; } added = true; - } else if (compareRes == Lattice::UNKNOWN) { + } else if (compareRes == UNKNOWN) { break; - } else if (compareRes == Lattice::SAME) { + } else if (compareRes == SAME) { ++i; auto temp = result[i]; result[i] = state; @@ -257,47 +247,6 @@ namespace storm { } } - void Lattice::toDotFile(std::ostream &out) { - assert (false); -// 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 < (*itr)->states.size()) { -// out << index; -// index = (*itr)->states.getNextSetIndex(index + 1); -// if (index < (*itr)->states.size()) { -// out << ", "; -// } -// } -// -// 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 = getBelow(*itr); -// for (auto itr2 = below.begin(); itr2 != below.end(); ++itr2) { -// out << "\t\"" << (*itr) << "\" -> \"" << (*itr2) << "\";" << std::endl; -// } -// printed.push_back(*itr); -// } -// } -// -// out << "}" << std::endl; - } - - bool Lattice::above(Node *node1, Node *node2) { bool found = false; for (auto const& state : node1->states) { @@ -335,7 +284,6 @@ namespace storm { } } if (!found) { - // TODO: kan dit niet anders? nodePrev->statesAbove|=((node2->statesAbove)); statesSeen->operator|=(((node2->statesAbove))); diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 0e1790fc3..e0aef5acd 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -1,7 +1,3 @@ -// -// Created by Jip Spel on 24.07.18. -// - #ifndef LATTICE_LATTICE_H #define LATTICE_LATTICE_H @@ -15,9 +11,19 @@ namespace storm { namespace analysis { + class Lattice { public: + /*! + * Constants for comparison of nodes/states + */ + enum NodeComparison { + UNKNOWN, + BELOW, + ABOVE, + SAME, + }; struct Node { boost::container::flat_set states; storm::storage::BitVector statesAbove; @@ -63,30 +69,23 @@ namespace storm { void add(uint_fast64_t state); /*! - * Adds a new relation between two nodes to the lattice - * @param above The node closest to the top Node of the Lattice. - * @param below The node closest to the bottom Node of 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 below The node closest to the bottom Node of the Lattice. + */ void addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below); - /*! - * Adds a new relation between two nodes to the lattice - * @param above The node closest to the top Node of the Lattice. - * @param below The node closest to the bottom Node of the Lattice. - */ - void addRelation(uint_fast64_t above, uint_fast64_t below); - /*! * Compares the level of the nodes of the states. * Behaviour unknown when one or more of the states doesnot occur at any Node in the Lattice. * @param state1 The first state. * @param state2 The second state. - * @return 0 if the nodes are on the same level; - * 1 if the node of the first state is closer to top then the node of the second state; - * 2 if the node of the second state is closer to top then the node of the first state; - * -1 if it is unclear from the structure of the lattice how the nodes relate. + * @return SAME if the nodes are on the same level; + * ABOVE if the node of the first state is closer to top then the node of the second state; + * BELOW if the node of the second state is closer to top then the node of the first state; + * UNKNOWN if it is unclear from the structure of the lattice how the nodes relate. */ - int compare(uint_fast64_t state1, uint_fast64_t state2); + Lattice::NodeComparison compare(uint_fast64_t state1, uint_fast64_t state2); /*! * Retrieves the pointer to a Node at which the state occurs. @@ -127,13 +126,32 @@ namespace storm { */ storm::storage::BitVector* getAddedStates(); + /*! + * Returns true if done building the lattice. + * @return + */ bool getDoneBuilding(); - int compare(Node* node1, Node* node2); - + /*! + * Compares two nodes in the lattice + * @param node1 + * @param node2 + * @return BELOW, ABOVE, SAME or UNKNOWN + */ + NodeComparison compare(Node* node1, Node* node2); + /*! + * Sorts the given stats if possible. + * + * @param states Bitvector of the states to sort + * @return Vector with states sorted, length equals number of states to sort. + * If states cannot be sorted, last state of the vector will always equal the length of the BitVector + */ std::vector sortStates(storm::storage::BitVector* states); + /*! + * If the lattice is fully build, this can be set to true. + */ void setDoneBuilding(bool done); /*! @@ -143,13 +161,6 @@ namespace storm { */ 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); - /*! * Merges node2 into node1 * @param node1 @@ -163,17 +174,6 @@ namespace storm { */ void merge(uint_fast64_t var1, uint_fast64_t var2); - - /*! - * Constants for comparison of nodes/states - */ - enum { - UNKNOWN = -1, - BELOW = 2, - ABOVE = 1, - SAME = 0, - }; - private: std::vector nodes; @@ -189,8 +189,6 @@ namespace storm { bool above(Node * node1, Node * node2, storm::analysis::Lattice::Node *nodePrev, storm::storage::BitVector *statesSeen); - std::unordered_map> comparisons; - bool doneBuilding; }; } diff --git a/src/test/storm-pars/analysis/LatticeExtenderTest.cpp b/src/test/storm-pars/analysis/LatticeExtenderTest.cpp index b174d3873..cda1d7233 100644 --- a/src/test/storm-pars/analysis/LatticeExtenderTest.cpp +++ b/src/test/storm-pars/analysis/LatticeExtenderTest.cpp @@ -1,8 +1,3 @@ -// -// Created by Jip Spel on 20.09.18. -// - -// TODO: cleanup includes #include "gtest/gtest.h" #include "storm-config.h" #include "test/storm_gtest.h" @@ -63,11 +58,11 @@ TEST(LatticeExtenderTest, Brp_with_bisimulation) { } // Check on some nodes - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice->compare(1,0)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice->compare(1,5)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice->compare(5,0)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice->compare(94,5)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice->compare(7,13)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice->compare(1,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice->compare(1,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice->compare(5,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice->compare(94,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice->compare(7,13)); } TEST(LatticeExtenderTest, Brp_without_bisimulation) { diff --git a/src/test/storm-pars/analysis/LatticeTest.cpp b/src/test/storm-pars/analysis/LatticeTest.cpp index 27806bc50..dbb590c41 100644 --- a/src/test/storm-pars/analysis/LatticeTest.cpp +++ b/src/test/storm-pars/analysis/LatticeTest.cpp @@ -1,8 +1,3 @@ -// -// Created by Jip Spel on 20.09.18. -// - -// TODO: cleanup includes #include "gtest/gtest.h" #include "storm-config.h" #include "test/storm_gtest.h" @@ -18,60 +13,60 @@ TEST(LatticeTest, Simple) { auto initialMiddle = storm::storage::BitVector(numberOfStates); auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,1)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,1)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,0)); EXPECT_EQ(nullptr, lattice.getNode(2)); lattice.add(2); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,2)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(2,0)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(2,1)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(2,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(2,1)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,2)); lattice.add(3); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(2,3)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(3,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(2,3)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(3,2)); lattice.addToNode(4, lattice.getNode(2)); - EXPECT_EQ(storm::analysis::Lattice::SAME, lattice.compare(2,4)); - EXPECT_EQ(storm::analysis::Lattice::SAME, lattice.compare(4,2)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,4)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(4,0)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(4,1)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,4)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(4,3)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(3,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, lattice.compare(2,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, lattice.compare(4,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(4,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(4,1)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(4,3)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(3,4)); lattice.addBetween(5, lattice.getNode(0), lattice.getNode(3)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(5,0)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,5)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(5,3)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,5)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(5,1)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,5)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(5,2)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(2,5)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(5,4)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(4,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(5,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(5,3)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(3,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(5,1)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(5,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(2,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(5,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(4,5)); lattice.addBetween(6, lattice.getNode(5), lattice.getNode(3)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,0)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,6)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(6,1)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,6)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(6,2)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(2,6)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(6,3)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,6)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(6,4)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(6,4)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,5)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(5,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(6,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(6,1)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(6,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(2,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(6,3)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(3,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(6,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(6,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(6,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(5,6)); lattice.addRelationNodes(lattice.getNode(6), lattice.getNode(4)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(6,4)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(4,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(6,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(4,6)); } @@ -93,51 +88,51 @@ TEST(LatticeTest, copy_lattice) { auto latticeCopy = storm::analysis::Lattice(lattice); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(0,1)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(1,0)); - - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(0,2)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(2,0)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(2,1)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(1,2)); - - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, latticeCopy.compare(2,3)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, latticeCopy.compare(3,2)); - - EXPECT_EQ(storm::analysis::Lattice::SAME, latticeCopy.compare(2,4)); - EXPECT_EQ(storm::analysis::Lattice::SAME, latticeCopy.compare(4,2)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(0,4)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(4,0)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(4,1)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(1,4)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, latticeCopy.compare(4,3)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, latticeCopy.compare(3,4)); - - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(5,0)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(0,5)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(5,3)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(3,5)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(5,1)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(1,5)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, latticeCopy.compare(5,2)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, latticeCopy.compare(5,2)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, latticeCopy.compare(5,4)); - EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, latticeCopy.compare(5,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(0,1)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(1,0)); + + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(0,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(2,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(2,1)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(1,2)); + + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(2,3)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(3,2)); + + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, latticeCopy.compare(2,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, latticeCopy.compare(4,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(0,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(4,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(4,1)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(1,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(4,3)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(3,4)); + + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(5,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(0,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(5,3)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(3,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(5,1)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(1,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(5,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(5,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(5,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(5,4)); lattice.addRelationNodes(lattice.getNode(6), lattice.getNode(4)); latticeCopy = storm::analysis::Lattice(lattice); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(6,0)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(0,6)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(6,1)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(1,6)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(6,2)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(2,6)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(6,3)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(3,6)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(6,4)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(4,6)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(6,5)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(5,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(6,0)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(0,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(6,1)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(1,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(6,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(2,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(6,3)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(3,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(6,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(4,6)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(6,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(5,6)); } TEST(LatticeTest, merge_nodes) { @@ -156,20 +151,20 @@ TEST(LatticeTest, merge_nodes) { lattice.addBetween(6, lattice.getNode(5), lattice.getNode(3)); lattice.mergeNodes(lattice.getNode(4), lattice.getNode(5)); - EXPECT_EQ(storm::analysis::Lattice::SAME, lattice.compare(2,4)); - EXPECT_EQ(storm::analysis::Lattice::SAME, lattice.compare(2,5)); - - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,5)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,2)); - EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,4)); - - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,2)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,4)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,5)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,2)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,4)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,5)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,2)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,4)); - EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, lattice.compare(2,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, lattice.compare(2,5)); + + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,4)); + + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(6,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(6,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(6,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(3,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(3,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(3,5)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,2)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,4)); + EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,5)); }