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(); 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 seenNodes = std::set({}); 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