From 78e5108e42a384d2fea7478c5f04c12f31a5fff8 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Fri, 26 Oct 2018 14:28:32 +0200
Subject: [PATCH] Extend Lattice test

---
 src/test/storm-pars/analysis/LatticeTest.cpp | 63 +++++++++++++++++++-
 1 file changed, 62 insertions(+), 1 deletion(-)

diff --git a/src/test/storm-pars/analysis/LatticeTest.cpp b/src/test/storm-pars/analysis/LatticeTest.cpp
index 7df231912..14cd55c38 100644
--- a/src/test/storm-pars/analysis/LatticeTest.cpp
+++ b/src/test/storm-pars/analysis/LatticeTest.cpp
@@ -10,7 +10,7 @@
 #include "storm/storage/BitVector.h"
 
 TEST(LatticeTest, Simple) {
-    auto numberOfStates = 5;
+    auto numberOfStates = 7;
     auto above = storm::storage::BitVector(numberOfStates);
     above.set(0);
     auto below = storm::storage::BitVector(numberOfStates);
@@ -35,4 +35,65 @@ TEST(LatticeTest, Simple) {
     EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(4,1));
     EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(4,3));
     EXPECT_EQ(storm::analysis::Lattice::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(5,3));
+    EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(5,1));
+    EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(5,2));
+    EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(5,4));
+
+    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(6,1));
+    EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(6,2));
+    EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(6,3));
+    EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, lattice.compare(6,4));
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,5));
 }
+
+TEST(LatticeTest, copy_lattice) {
+    auto numberOfStates = 7;
+    auto above = storm::storage::BitVector(numberOfStates);
+    above.set(0);
+    auto below = storm::storage::BitVector(numberOfStates);
+    below.set(1);
+
+    auto lattice = storm::analysis::Lattice(above, below, numberOfStates);
+    lattice.add(2);
+    lattice.add(3);
+    lattice.addToNode(4, lattice.getNode(2));
+    lattice.addBetween(5, lattice.getNode(0), lattice.getNode(3));
+    lattice.addBetween(6, lattice.getNode(5), lattice.getNode(3));
+
+
+    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::ABOVE, latticeCopy.compare(2,1));
+
+    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::ABOVE, latticeCopy.compare(0,4));
+    EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(4,1));
+    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(5,3));
+    EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(5,1));
+    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::BELOW, latticeCopy.compare(6,0));
+    EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(6,1));
+    EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, latticeCopy.compare(6,2));
+    EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(6,3));
+    EXPECT_EQ(storm::analysis::Lattice::UNKNOWN, latticeCopy.compare(6,4));
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(6,5));
+}
\ No newline at end of file