diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index d16aad8ad..e8d351097 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -27,25 +27,19 @@ namespace storm { nodes.at(i) = bottom; } - top->above = new std::set({}); top->statesAbove = storm::storage::BitVector(numberOfStates); setStatesBelow(top, bottomStates, false); assert(top->statesAbove.size() == numberOfStates); assert(top->statesBelow.size() == numberOfStates); assert(top->statesAbove.getNumberOfSetBits() == 0); assert(top->statesBelow.getNumberOfSetBits() == bottomStates.getNumberOfSetBits()); - assert(top->above->size() == 0); - assert(top->below->size() == bottomStates.getNumberOfSetBits()); - bottom->below = new std::set({}); bottom->statesBelow = storm::storage::BitVector(numberOfStates); setStatesAbove(bottom, topStates, false); assert(bottom->statesAbove.size() == numberOfStates); assert(bottom->statesBelow.size() == numberOfStates); assert(bottom->statesBelow.getNumberOfSetBits() == 0); assert(bottom->statesAbove.getNumberOfSetBits() == topStates.getNumberOfSetBits()); - assert(bottom->below->size() == 0); - assert(bottom->above->size() == topStates.getNumberOfSetBits()); this->numberOfStates = numberOfStates; this->addedStates = storm::storage::BitVector(numberOfStates); @@ -56,28 +50,13 @@ namespace storm { Lattice::Lattice(Lattice* lattice) { numberOfStates = lattice->getAddedStates().size(); nodes = std::vector(numberOfStates); - - top = new Node(); - top->states = storm::storage::BitVector(lattice->getTop()->states); - for (auto i = top->states.getNextSetIndex(0); i < top->states.size(); i = top->states.getNextSetIndex(i+1)) { - nodes.at(i) = top; - } - - bottom = new Node(); - bottom->states = storm::storage::BitVector(lattice->getBottom()->states); - for (auto i = bottom->states.getNextSetIndex(0); i < bottom->states.size(); i = bottom->states.getNextSetIndex(i+1)) { - nodes.at(i) = bottom; - } - addedStates = storm::storage::BitVector(numberOfStates); - addedStates |= (top->states); - addedStates |= (bottom->states); auto oldNodes = lattice->getNodes(); // Create nodes for (auto itr = oldNodes.begin(); itr != oldNodes.end(); ++itr) { Node *oldNode = (*itr); - if (oldNode != nullptr && oldNode != lattice->getTop() && oldNode != lattice->getBottom()) { + if (oldNode != nullptr) { Node *newNode = new Node(); newNode->states = storm::storage::BitVector(oldNode->states); for (auto i = newNode->states.getNextSetIndex(0); @@ -85,6 +64,11 @@ namespace storm { addedStates.set(i); nodes.at(i) = newNode; } + if (oldNode == lattice->getTop()) { + top = newNode; + } else if (oldNode == lattice->getBottom()) { + bottom = newNode; + } } } assert(addedStates == lattice->getAddedStates()); @@ -98,27 +82,18 @@ namespace storm { setStatesBelow(newNode, oldNode->statesBelow, false); } else if (oldNode != nullptr && oldNode == lattice->getBottom()) { setStatesAbove(bottom, lattice->getBottom()->statesAbove, false); - assert(lattice->getBottom()->statesBelow.getNumberOfSetBits() == 0); - bottom->below = new std::set({}); bottom->statesBelow = storm::storage::BitVector(numberOfStates); - assert(bottom->statesAbove.size() == numberOfStates); - assert(bottom->statesBelow.size() == numberOfStates); } else if (oldNode != nullptr && oldNode == lattice->getTop()) { - top->above = new std::set({}); top->statesAbove = storm::storage::BitVector(numberOfStates); - assert(lattice->getTop()->statesAbove.getNumberOfSetBits() == 0); setStatesBelow(top, lattice->getTop()->statesBelow, false); - assert(top->statesAbove.size() == numberOfStates); - assert(top->statesBelow.size() == numberOfStates); } + // To check if everything went well if (oldNode!= nullptr) { Node *newNode = getNode(oldNode->states.getNextSetIndex(0)); assert((newNode->statesAbove & newNode->statesBelow).getNumberOfSetBits() == 0); assert(newNode->statesAbove == oldNode->statesAbove); assert(newNode->statesBelow == oldNode->statesBelow); - assert(newNode->above->size() == oldNode->above->size()); - assert(newNode->below->size() == oldNode->below->size()); } } } @@ -166,18 +141,17 @@ namespace storm { } void Lattice::addRelationNodes(Lattice::Node *above, Lattice::Node * below) { - assert(compare(above, below) == UNKNOWN); - assert((above->statesAbove & below->statesBelow).getNumberOfSetBits() == 0); + assert (compare(above, below) == UNKNOWN); - setStatesBelow(above, below->states, true); - setStatesAbove(below, above->states, true); + setStatesBelow(above, below->states | below->statesBelow, true); + setStatesAbove(below, above->states | above->statesAbove, true); for (auto i = below->statesBelow.getNextSetIndex(0); i < below->statesBelow.size(); i = below->statesBelow.getNextSetIndex(i + 1)) { - setStatesAbove(getNode(i), above->states, true); + setStatesAbove(getNode(i), above->states | above->statesAbove, true); } for (auto i = above->statesAbove.getNextSetIndex(0); i < above->statesAbove.size(); i = above->statesAbove.getNextSetIndex(i + 1)) { - setStatesBelow(getNode(i), below->states, true); + setStatesBelow(getNode(i), below->states | below->statesBelow, true); } } @@ -223,6 +197,30 @@ namespace storm { return addedStates; } + std::set Lattice::getAbove(uint_fast64_t state) { + return getAbove(getNode(state)); + } + + std::set Lattice::getBelow(uint_fast64_t state) { + return getBelow(getNode(state)); + } + + std::set Lattice::getAbove(Lattice::Node* node) { + std::set result({}); + for (auto i = node->statesAbove.getNextSetIndex(0); i < node->statesAbove.size(); i = node->statesAbove.getNextSetIndex(i + 1)) { + result.insert(getNode(i)); + } + return result; + } + + std::set Lattice::getBelow(Lattice::Node* node) { + std::set result({}); + for (auto i = node->statesBelow.getNextSetIndex(0); i < node->statesBelow.size(); i = node->statesBelow.getNextSetIndex(i + 1)) { + result.insert(getNode(i)); + } + return result; + } + void Lattice::toString(std::ostream &out) { std::vector printedNodes = std::vector({}); for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { @@ -243,7 +241,8 @@ namespace storm { out << " Address: " << node << "\n"; out << " Above: {"; - for (auto itr2 = node->above->begin(); itr2 != node->above->end(); ++itr2) { + auto statesAbove = getAbove(node); + for (auto itr2 = statesAbove.begin(); itr2 != statesAbove.end(); ++itr2) { Node *above = *itr2; index = above->states.getNextSetIndex(0); out << "{"; @@ -261,7 +260,8 @@ namespace storm { out << " Below: {"; - for (auto itr2 = node->below->begin(); itr2 != node->below->end(); ++itr2) { + auto statesBelow = getBelow(node); + for (auto itr2 = statesBelow.begin(); itr2 != statesBelow.end(); ++itr2) { Node *below = *itr2; out << "{"; index = below->states.getNextSetIndex(0); @@ -308,8 +308,8 @@ namespace storm { printed.clear(); for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) { - auto below = (*itr)->below; - for (auto itr2 = below->begin(); itr2 != below->end(); ++itr2) { + auto below = getBelow(*itr); + for (auto itr2 = below.begin(); itr2 != below.end(); ++itr2) { out << "\t\"" << (*itr) << "\" -> \"" << (*itr2) << "\";" << std::endl; } printed.push_back(*itr); @@ -320,6 +320,21 @@ namespace storm { } bool Lattice::above(Node *node1, Node *node2) { + bool check = node1->statesBelow.get(node2->states.getNextSetIndex(0)); + for (auto i = node2->states.getNextSetIndex(0); i < node2->states.size(); i = node2->states.getNextSetIndex(i+1)) { + if (check) { + assert(node1->statesBelow.get(i)); + } else { + assert(!node1->statesBelow.get(i)); + } + } + for (auto i = node1->states.getNextSetIndex(0); i < node1->states.size(); i = node1->states.getNextSetIndex(i+1)) { + if (check) { + assert(node2->statesAbove.get(i)); + } else { + assert(!node2->statesAbove.get(i)); + } + } return node1->statesBelow.get(node2->states.getNextSetIndex(0)); } @@ -327,20 +342,16 @@ namespace storm { assert (!node->states.get(state)); if (!alreadyInitialized) { node->statesAbove = storm::storage::BitVector(numberOfStates); - node->above = new std::set({}); } node->statesAbove.set(state); - node->above->insert(getNode(state)); } void Lattice::setStatesBelow(Lattice::Node *node, uint_fast64_t state, bool alreadyInitialized) { assert (!node->states.get(state)); if (!alreadyInitialized) { node->statesBelow = storm::storage::BitVector(numberOfStates); - node->below = new std::set({}); } node->statesBelow.set(state); - node->below->insert(getNode(state)); } void Lattice::setStatesAbove(Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized) { @@ -350,13 +361,10 @@ namespace storm { node->statesAbove |= states; } else { node->statesAbove = storm::storage::BitVector(states); - node->above = new std::set({}); } for (auto i = states.getNextSetIndex(0); i < states.size(); i = states.getNextSetIndex(i + 1)) { if (node->states.get(i)) { node->statesAbove.set(i, false); - } else { - node->above->insert(getNode(i)); } } } @@ -367,13 +375,10 @@ namespace storm { node->statesBelow |= states; } else { node->statesBelow = storm::storage::BitVector(states); - node->below = new std::set({}); } for (auto i = states.getNextSetIndex(0); i < states.size(); i = states.getNextSetIndex(i + 1)) { if (node->states.get(i)) { node->statesBelow.set(i, false); - } else { - node->below->insert(getNode(i)); } } } diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 9d433b602..aeec31fb3 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -20,8 +20,6 @@ namespace storm { storm::storage::BitVector states; storm::storage::BitVector statesAbove; storm::storage::BitVector statesBelow; - std::set* above; - std::set* below; }; /*! @@ -114,6 +112,14 @@ namespace storm { */ storm::storage::BitVector getAddedStates(); + std::set getAbove(uint_fast64_t state); + + std::set getBelow(uint_fast64_t state); + + std::set getAbove(Lattice::Node* node); + + std::set getBelow(Lattice::Node* node); + /*! * Prints a string representation of the lattice to the output stream. * diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index 89d4d6ec9..4cc596571 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -34,7 +34,7 @@ namespace storm { } template - std::tuple LatticeExtender::toLattice(std::vector> formulas) { + std::tuple LatticeExtender::toLattice(std::vector> formulas) { storm::utility::Stopwatch latticeWatch(true); STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis"); @@ -107,7 +107,7 @@ namespace storm { } // Create the Lattice - storm::analysis::Lattice *lattice = new storm::analysis::Lattice(topStates, bottomStates, numberOfStates); + Lattice *lattice = new Lattice(topStates, bottomStates, numberOfStates); for (auto state = initialMiddleStates.getNextSetIndex(0); state != numberOfStates; state = initialMiddleStates.getNextSetIndex(state + 1)) { lattice->add(state); } @@ -119,7 +119,7 @@ namespace storm { } template - std::tuple LatticeExtender::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr assumption) { + std::tuple LatticeExtender::extendLattice(Lattice* lattice, std::shared_ptr assumption) { // TODO: split up auto numberOfStates = this->model->getNumberOfStates(); // First handle assumption @@ -137,9 +137,9 @@ namespace storm { auto val1 = std::stoul(var1.getName(), nullptr, 0); auto val2 = std::stoul(var2.getName(), nullptr, 0); auto comp = lattice->compare(val1, val2); - assert (comp == storm::analysis::Lattice::UNKNOWN || comp == storm::analysis::Lattice::SAME); - storm::analysis::Lattice::Node *n1 = lattice->getNode(val1); - storm::analysis::Lattice::Node *n2 = lattice->getNode(val2); + assert (comp == Lattice::UNKNOWN || comp == Lattice::SAME); + Lattice::Node *n1 = lattice->getNode(val1); + Lattice::Node *n2 = lattice->getNode(val2); if (n1 != nullptr && n2 != nullptr) { assert(false); @@ -157,12 +157,13 @@ namespace storm { assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()); storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable(); storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable(); - if (lattice->compare(std::stoul(largest.getName(), nullptr, 0), - std::stoul(smallest.getName(), nullptr, 0)) != - storm::analysis::Lattice::ABOVE) { - storm::analysis::Lattice::Node *n1 = lattice->getNode( + auto compareRes = lattice->compare(std::stoul(largest.getName(), nullptr, 0), + std::stoul(smallest.getName(), nullptr, 0)); + assert(compareRes == Lattice::UNKNOWN); + if (compareRes != Lattice::ABOVE) { + Lattice::Node *n1 = lattice->getNode( std::stoul(largest.getName(), nullptr, 0)); - storm::analysis::Lattice::Node *n2 = lattice->getNode( + Lattice::Node *n2 = lattice->getNode( std::stoul(smallest.getName(), nullptr, 0)); if (n1 != nullptr && n2 != nullptr) { @@ -209,24 +210,25 @@ namespace storm { uint_fast64_t successor2 = successors.getNextSetIndex(successor1 + 1); int compareResult = lattice->compare(successor1, successor2); - if (compareResult == storm::analysis::Lattice::ABOVE) { + if (compareResult == Lattice::ABOVE) { // successor 1 is closer to top than successor 2 lattice->addBetween(stateNumber, lattice->getNode(successor1), lattice->getNode(successor2)); - } else if (compareResult == storm::analysis::Lattice::BELOW) { + } else if (compareResult == Lattice::BELOW) { // successor 2 is closer to top than successor 1 lattice->addBetween(stateNumber, lattice->getNode(successor2), lattice->getNode(successor1)); - } else if (compareResult == storm::analysis::Lattice::SAME) { + } else if (compareResult == Lattice::SAME) { // the successors are at the same level lattice->addToNode(stateNumber, lattice->getNode(successor1)); } else { + assert(lattice->compare(successor1, successor2) == Lattice::UNKNOWN); return std::make_tuple(lattice, successor1, successor2); } } else if (check && successors.getNumberOfSetBits() > 2) { for (auto i = successors.getNextSetIndex(0); i < successors.size(); i = successors.getNextSetIndex(i+1)) { for (auto j = successors.getNextSetIndex(i+1); j < successors.size(); j = successors.getNextSetIndex(j+1)) { - if (lattice->compare(i,j) == storm::analysis::Lattice::UNKNOWN) { + if (lattice->compare(i,j) == Lattice::UNKNOWN) { return std::make_tuple(lattice, i, j); } } @@ -235,16 +237,18 @@ namespace storm { auto highest = successors.getNextSetIndex(0); auto lowest = highest; for (auto i = successors.getNextSetIndex(highest+1); i < successors.size(); i = successors.getNextSetIndex(i+1)) { - if (lattice->compare(i, highest) == storm::analysis::Lattice::ABOVE) { + if (lattice->compare(i, highest) == Lattice::ABOVE) { highest = i; } - if (lattice->compare(lowest, i) == storm::analysis::Lattice::ABOVE) { + if (lattice->compare(lowest, i) == Lattice::ABOVE) { lowest = i; } } lattice->addBetween(stateNumber, lattice->getNode(highest), lattice->getNode(lowest)); } + + // Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet bool checkOneSuccLeft = seenStates[stateNumber] && successors.getNumberOfSetBits() <= 2; bool helper = true; for (auto succIndex = successors.getNextSetIndex(0); (check || checkOneSuccLeft) && succIndex != numberOfStates; succIndex = successors.getNextSetIndex(++succIndex)) { @@ -268,9 +272,9 @@ namespace storm { assert (seenStates[succ1]); auto nodeSucc = lattice->getNode(succ1); auto compare = lattice->compare(stateNumber, succ1); - if (compare == storm::analysis::Lattice::ABOVE) { + if (compare == Lattice::ABOVE) { lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber)); - } else if (compare == storm::analysis::Lattice::BELOW) { + } else if (compare == Lattice::BELOW) { lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom()); } } diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index d29779181..464cffe7b 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -196,6 +196,7 @@ namespace storm { auto assumption2 = *itr; if (!assumption1.second && !assumption2.second) { + // TODO: hier niet verder gaan als je iets gevonden hebt? auto assumptionsCopy = std::vector>(assumptions); auto latticeCopy = new storm::analysis::Lattice(lattice); assumptions.push_back(assumption1.first);