sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Clean up Lattice

tempestpy_adaptions
Jip Spel 6 years ago
parent
fa97e0138f
commit
c0aa6eefa3
6 changed files with 155 additions and 226 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 17
      src/storm-pars/analysis/AssumptionChecker.cpp
  2. 4
      src/storm-pars/analysis/AssumptionChecker.h
  3. 62
      src/storm-pars/analysis/Lattice.cpp
  4. 82
      src/storm-pars/analysis/Lattice.h
  5. 15
      src/test/storm-pars/analysis/LatticeExtenderTest.cpp
  6. 201
      src/test/storm-pars/analysis/LatticeTest.cpp

17
src/storm-pars/analysis/AssumptionChecker.cpp
View File

@ -1,6 +1,3 @@
//
// Created by Jip Spel on 12.09.18.
//
#include <storm/solver/Z3SmtSolver.h> #include <storm/solver/Z3SmtSolver.h>
#include "AssumptionChecker.h" #include "AssumptionChecker.h"
@ -166,7 +163,7 @@ namespace storm {
if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) { if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) {
if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Greater 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 // The assumption should be the greater assumption
// If the result is unknown, we cannot compare, also SMTSolver will not help // If the result is unknown, we cannot compare, also SMTSolver will not help
result = validateAssumptionFunction(lattice, state1succ1, state1succ2, state2succ1, result = validateAssumptionFunction(lattice, state1succ1, state1succ2, state2succ1,
@ -206,10 +203,10 @@ namespace storm {
// Calculate the difference in probability for the "highest" successor state // Calculate the difference in probability for the "highest" successor state
ValueType prob; ValueType prob;
auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()); 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(); prob = state1succ1->getValue() - state2succ1->getValue();
} else if (comp == Lattice::BELOW) {
} else if (comp == Lattice::NodeComparison::BELOW) {
prob = state1succ2->getValue() - state2succ2->getValue(); prob = state1succ2->getValue() - state2succ2->getValue();
} }
@ -266,13 +263,13 @@ namespace storm {
stateVariables.insert(manager->declareRationalVariable(varname2)); stateVariables.insert(manager->declareRationalVariable(varname2));
} }
auto comp = lattice->compare(itr1->getColumn(), itr2->getColumn()); auto comp = lattice->compare(itr1->getColumn(), itr2->getColumn());
if (comp == Lattice::ABOVE) {
if (comp == Lattice::NodeComparison::ABOVE) {
exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) <= exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) <=
manager->getVariable(varname2)); manager->getVariable(varname2));
} else if (comp == Lattice::BELOW) {
} else if (comp == Lattice::NodeComparison::BELOW) {
exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) >= exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) >=
manager->getVariable(varname2)); manager->getVariable(varname2));
} else if (comp == Lattice::SAME) {
} else if (comp == Lattice::NodeComparison::SAME) {
exprOrderSucc = exprOrderSucc && exprOrderSucc = exprOrderSucc &&
(manager->getVariable(varname1) = manager->getVariable(varname2)); (manager->getVariable(varname1) = manager->getVariable(varname2));
} else { } else {

4
src/storm-pars/analysis/AssumptionChecker.h
View File

@ -1,7 +1,3 @@
//
// Created by Jip Spel on 12.09.18.
//
#ifndef STORM_ASSUMPTIONCHECKER_H #ifndef STORM_ASSUMPTIONCHECKER_H
#define STORM_ASSUMPTIONCHECKER_H #define STORM_ASSUMPTIONCHECKER_H

62
src/storm-pars/analysis/Lattice.cpp
View File

@ -1,7 +1,3 @@
//
// Created by Jip Spel on 24.07.18.
//
#include <iostream> #include <iostream>
#include <fstream> #include <fstream>
#include "Lattice.h" #include "Lattice.h"
@ -24,7 +20,6 @@ namespace storm {
top->statesAbove = storm::storage::BitVector(numberOfStates); top->statesAbove = storm::storage::BitVector(numberOfStates);
bottom->statesAbove = storm::storage::BitVector(numberOfStates); bottom->statesAbove = storm::storage::BitVector(numberOfStates);
for (auto const& i : *topStates) { for (auto const& i : *topStates) {
addedStates->set(i); addedStates->set(i);
bottom->statesAbove.set(i); bottom->statesAbove.set(i);
@ -116,15 +111,11 @@ namespace storm {
assert (compare(above, below) == ABOVE); 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)); 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 != nullptr && node2 != nullptr) {
if (node1 == node2) { if (node1 == node2) {
return SAME; return SAME;
@ -185,7 +176,6 @@ namespace storm {
} }
std::vector<uint_fast64_t> Lattice::sortStates(storm::storage::BitVector* states) { std::vector<uint_fast64_t> Lattice::sortStates(storm::storage::BitVector* states) {
// TODO improve
auto numberOfSetBits = states->getNumberOfSetBits(); auto numberOfSetBits = states->getNumberOfSetBits();
auto stateSize = states->size(); auto stateSize = states->size();
auto result = std::vector<uint_fast64_t>(numberOfSetBits, stateSize); auto result = std::vector<uint_fast64_t>(numberOfSetBits, stateSize);
@ -201,7 +191,7 @@ namespace storm {
added = true; added = true;
} else { } else {
auto compareRes = compare(state, result[i]); auto compareRes = compare(state, result[i]);
if (compareRes == Lattice::ABOVE) {
if (compareRes == ABOVE) {
auto temp = result[i]; auto temp = result[i];
result[i] = state; result[i] = state;
for (auto j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) { for (auto j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) {
@ -210,9 +200,9 @@ namespace storm {
temp = temp2; temp = temp2;
} }
added = true; added = true;
} else if (compareRes == Lattice::UNKNOWN) {
} else if (compareRes == UNKNOWN) {
break; break;
} else if (compareRes == Lattice::SAME) {
} else if (compareRes == SAME) {
++i; ++i;
auto temp = result[i]; auto temp = result[i];
result[i] = state; 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<Node*> 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 Lattice::above(Node *node1, Node *node2) {
bool found = false; bool found = false;
for (auto const& state : node1->states) { for (auto const& state : node1->states) {
@ -335,7 +284,6 @@ namespace storm {
} }
} }
if (!found) { if (!found) {
// TODO: kan dit niet anders?
nodePrev->statesAbove|=((node2->statesAbove)); nodePrev->statesAbove|=((node2->statesAbove));
statesSeen->operator|=(((node2->statesAbove))); statesSeen->operator|=(((node2->statesAbove)));

82
src/storm-pars/analysis/Lattice.h
View File

@ -1,7 +1,3 @@
//
// Created by Jip Spel on 24.07.18.
//
#ifndef LATTICE_LATTICE_H #ifndef LATTICE_LATTICE_H
#define LATTICE_LATTICE_H #define LATTICE_LATTICE_H
@ -15,9 +11,19 @@
namespace storm { namespace storm {
namespace analysis { namespace analysis {
class Lattice { class Lattice {
public: public:
/*!
* Constants for comparison of nodes/states
*/
enum NodeComparison {
UNKNOWN,
BELOW,
ABOVE,
SAME,
};
struct Node { struct Node {
boost::container::flat_set<uint_fast64_t> states; boost::container::flat_set<uint_fast64_t> states;
storm::storage::BitVector statesAbove; storm::storage::BitVector statesAbove;
@ -63,30 +69,23 @@ namespace storm {
void add(uint_fast64_t state); 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); 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. * 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. * Behaviour unknown when one or more of the states doesnot occur at any Node in the Lattice.
* @param state1 The first state. * @param state1 The first state.
* @param state2 The second 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. * Retrieves the pointer to a Node at which the state occurs.
@ -127,13 +126,32 @@ namespace storm {
*/ */
storm::storage::BitVector* getAddedStates(); storm::storage::BitVector* getAddedStates();
/*!
* Returns true if done building the lattice.
* @return
*/
bool getDoneBuilding(); 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<uint_fast64_t> sortStates(storm::storage::BitVector* states); std::vector<uint_fast64_t> sortStates(storm::storage::BitVector* states);
/*!
* If the lattice is fully build, this can be set to true.
*/
void setDoneBuilding(bool done); void setDoneBuilding(bool done);
/*! /*!
@ -143,13 +161,6 @@ namespace storm {
*/ */
void toString(std::ostream &out); 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 * Merges node2 into node1
* @param node1 * @param node1
@ -163,17 +174,6 @@ namespace storm {
*/ */
void merge(uint_fast64_t var1, uint_fast64_t var2); 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: private:
std::vector<Node*> nodes; std::vector<Node*> nodes;
@ -189,8 +189,6 @@ namespace storm {
bool above(Node * node1, Node * node2, storm::analysis::Lattice::Node *nodePrev, storm::storage::BitVector *statesSeen); bool above(Node * node1, Node * node2, storm::analysis::Lattice::Node *nodePrev, storm::storage::BitVector *statesSeen);
std::unordered_map<uint_fast64_t, std::unordered_map<uint_fast64_t, uint_fast64_t>> comparisons;
bool doneBuilding; bool doneBuilding;
}; };
} }

15
src/test/storm-pars/analysis/LatticeExtenderTest.cpp
View File

@ -1,8 +1,3 @@
//
// Created by Jip Spel on 20.09.18.
//
// TODO: cleanup includes
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "storm-config.h" #include "storm-config.h"
#include "test/storm_gtest.h" #include "test/storm_gtest.h"
@ -63,11 +58,11 @@ TEST(LatticeExtenderTest, Brp_with_bisimulation) {
} }
// Check on some nodes // 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) { TEST(LatticeExtenderTest, Brp_without_bisimulation) {

201
src/test/storm-pars/analysis/LatticeTest.cpp
View File

@ -1,8 +1,3 @@
//
// Created by Jip Spel on 20.09.18.
//
// TODO: cleanup includes
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "storm-config.h" #include "storm-config.h"
#include "test/storm_gtest.h" #include "test/storm_gtest.h"
@ -18,60 +13,60 @@ TEST(LatticeTest, Simple) {
auto initialMiddle = storm::storage::BitVector(numberOfStates); auto initialMiddle = storm::storage::BitVector(numberOfStates);
auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, 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)); EXPECT_EQ(nullptr, lattice.getNode(2));
lattice.add(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); 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)); 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)); 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)); 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)); 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); 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)); lattice.addRelationNodes(lattice.getNode(6), lattice.getNode(4));
latticeCopy = storm::analysis::Lattice(lattice); 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) { TEST(LatticeTest, merge_nodes) {
@ -156,20 +151,20 @@ TEST(LatticeTest, merge_nodes) {
lattice.addBetween(6, lattice.getNode(5), lattice.getNode(3)); lattice.addBetween(6, lattice.getNode(5), lattice.getNode(3));
lattice.mergeNodes(lattice.getNode(4), lattice.getNode(5)); 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));
} }
Write Preview
Loading…
Cancel
Save