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