From 2e4991a75e69004c649edcd93f9feae4655594f5 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Thu, 6 Sep 2018 13:46:57 +0200
Subject: [PATCH] TODO added create deep copy not yet working correctly

---
 src/storm-pars-cli/storm-pars.cpp   | 3 ---
 src/storm-pars/analysis/Lattice.cpp | 8 ++++----
 src/storm-pars/analysis/Lattice.h   | 2 +-
 3 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 3a67b13a9..d57c4932f 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -541,16 +541,13 @@ namespace storm {
                 latticeWatch.stop();
                 STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
 
-
                 // Monotonicity?
-
                 storm::utility::Stopwatch monotonicityWatch(true);
                 auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>();
                 monotonicityChecker.checkMonotonicity(result, sparseModel->getTransitionMatrix());
                 monotonicityWatch.stop();
                 STORM_PRINT(std::endl << "Time for monotonicity: " << monotonicityWatch << "." << std::endl << std::endl);
 
-
                 std::cout << "Bye, Jip2" << std::endl;
                 return;
             }
diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp
index e65363cd0..ddb0003a6 100644
--- a/src/storm-pars/analysis/Lattice.cpp
+++ b/src/storm-pars/analysis/Lattice.cpp
@@ -208,14 +208,14 @@ namespace storm {
             Lattice* result = new Lattice(top->states, bottom->states, numberOfStates);
 
             for (auto itr = top->below.begin(); itr != top->below.end(); ++itr) {
-                result->nogBedenken(*itr, result->getTop(), storm::storage::BitVector(numberOfStates));
+                result->createLattice(*itr, result->getTop(), storm::storage::BitVector(numberOfStates));
             }
 
-
             return result;
         }
 
-        void Lattice::nogBedenken(Lattice::Node* nodeFromOld, Lattice::Node* higherNode, storm::storage::BitVector seenStates) {
+        void Lattice::createLattice(Lattice::Node* nodeFromOld, Lattice::Node* higherNode, storm::storage::BitVector seenStates) {
+            //TODO: nog niet helemaal goed
             auto index = numberOfStates;
             std::set<Node*> seenNodes = std::set<Node*>({});
             for (auto i = nodeFromOld->states.getNextSetIndex(0); i < numberOfStates; i =nodeFromOld->states.getNextSetIndex(i+1)) {
@@ -243,7 +243,7 @@ namespace storm {
             for (auto itr = nodeFromOld->below.begin(); itr != nodeFromOld->below.end(); itr++) {
 //                if (!seenStates.get((*itr)->states.getNextSetIndex(0))) {
                     for (auto itr2 = seenNodes.begin(); itr2 != seenNodes.end(); ++itr2) {
-                        nogBedenken(*itr, *itr2, seenStates);
+                        createLattice(*itr, *itr2, seenStates);
                     }
 //                }
             }
diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h
index 02cbdf30a..5aeaf14cc 100644
--- a/src/storm-pars/analysis/Lattice.h
+++ b/src/storm-pars/analysis/Lattice.h
@@ -127,7 +127,7 @@ namespace storm {
 
                     uint_fast64_t numberOfStates;
 
-                    void nogBedenken(Node* nodeFromOld, Node* higherNode, storm::storage::BitVector seenStates);
+                    void createLattice(Node* nodeFromOld, Node* higherNode, storm::storage::BitVector seenStates);
                     /**
                      * Check if node1 lies above node2
                      * @param node1