Browse Source

TODO added create deep copy not yet working correctly

tempestpy_adaptions
Jip Spel 6 years ago
parent
commit
2e4991a75e
  1. 3
      src/storm-pars-cli/storm-pars.cpp
  2. 8
      src/storm-pars/analysis/Lattice.cpp
  3. 2
      src/storm-pars/analysis/Lattice.h

3
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;
}

8
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);
}
// }
}

2
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

Loading…
Cancel
Save