diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index cf5981beb..edead7737 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -8,47 +8,49 @@ namespace storm { namespace analysis { - Lattice::Lattice(storm::storage::BitVector topStates, - storm::storage::BitVector bottomStates, - storm::storage::BitVector initialMiddleStates, + Lattice::Lattice(storm::storage::BitVector* topStates, + storm::storage::BitVector* bottomStates, + storm::storage::BitVector* initialMiddleStates, uint_fast64_t numberOfStates) { - assert(topStates.getNumberOfSetBits() != 0); - assert(bottomStates.getNumberOfSetBits() != 0); - assert((topStates & bottomStates).getNumberOfSetBits() == 0); + assert(topStates->getNumberOfSetBits() != 0); + assert(bottomStates->getNumberOfSetBits() != 0); + assert((*topStates & *bottomStates).getNumberOfSetBits() == 0); nodes = std::vector(numberOfStates); top = new Node(); - top->states = topStates; - for (auto i = topStates.getNextSetIndex(0); i < topStates.size(); i = topStates.getNextSetIndex(i+1)) { - nodes.at(i) = top; + top->states = *topStates; + for (auto const& i : *topStates) { + nodes[i] = top; } bottom = new Node(); - bottom->states = bottomStates; - for (auto i = bottomStates.getNextSetIndex(0); i < bottomStates.size(); i = bottomStates.getNextSetIndex(i+1)) { - nodes.at(i) = bottom; + bottom->states = *bottomStates; + for (auto const& i : *bottomStates) { + nodes[i] = bottom; } top->statesAbove = storm::storage::BitVector(numberOfStates); - setStatesBelow(top, bottomStates, false); + bottom->statesAbove = *topStates; +// setStatesBelow(top, bottomStates, false); - bottom->statesBelow = storm::storage::BitVector(numberOfStates); - setStatesAbove(bottom, topStates, false); +// bottom->statesBelow = storm::storage::BitVector(numberOfStates); +// setStatesAbove(bottom, topStates, false); this->numberOfStates = numberOfStates; - this->addedStates = storm::storage::BitVector(numberOfStates); - this->addedStates |= (topStates); - this->addedStates |= (bottomStates); + this->addedStates = new storm::storage::BitVector(numberOfStates); + *addedStates |= *(topStates); + *addedStates |= *(bottomStates); - for (auto state = initialMiddleStates.getNextSetIndex(0); state < numberOfStates; state = initialMiddleStates.getNextSetIndex(state + 1)) { + for (auto const &state : *initialMiddleStates) { add(state); } } Lattice::Lattice(Lattice* lattice) { - numberOfStates = lattice->getAddedStates().size(); +// assert (false); + numberOfStates = lattice->getAddedStates()->size(); nodes = std::vector(numberOfStates); - addedStates = storm::storage::BitVector(numberOfStates); + addedStates = new storm::storage::BitVector(numberOfStates); auto oldNodes = lattice->getNodes(); // Create nodes @@ -59,8 +61,8 @@ namespace storm { newNode->states = storm::storage::BitVector(oldNode->states); for (auto i = newNode->states.getNextSetIndex(0); i < newNode->states.size(); i = newNode->states.getNextSetIndex(i + 1)) { - addedStates.set(i); - nodes.at(i) = newNode; + addedStates->set(i); + nodes[i] = newNode; } if (oldNode == lattice->getTop()) { top = newNode; @@ -77,77 +79,83 @@ namespace storm { Node *oldNode = (*itr); if (oldNode != nullptr && oldNode != lattice->getTop() && oldNode != lattice->getBottom()) { Node *newNode = getNode(oldNode->states.getNextSetIndex(0)); - setStatesAbove(newNode, oldNode->statesAbove, false); - setStatesBelow(newNode, oldNode->statesBelow, false); + newNode->statesAbove = storm::storage::BitVector(oldNode->statesAbove); +// setStatesAbove(newNode, oldNode->statesAbove, false); +// setStatesBelow(newNode, oldNode->statesBelow, false); } else if (oldNode != nullptr && oldNode == lattice->getBottom()) { - setStatesAbove(bottom, lattice->getBottom()->statesAbove, false); - bottom->statesBelow = storm::storage::BitVector(numberOfStates); - } else if (oldNode != nullptr && oldNode == lattice->getTop()) { - top->statesAbove = storm::storage::BitVector(numberOfStates); - setStatesBelow(top, lattice->getTop()->statesBelow, false); + bottom->statesAbove = storm::storage::BitVector(oldNode->statesAbove); +// setStatesAbove(bottom, lattice->getBottom()->statesAbove, false); +// bottom->statesBelow = storm::storage::BitVector(numberOfStates); +// } else if (oldNode != nullptr && oldNode == lattice->getTop()) { +// top->statesAbove = storm::storage::BitVector(numberOfStates); +// setStatesBelow(top, lattice->getTop()->statesBelow, false); } } } - void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) { - assert(!addedStates[state]); + void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) { + assert(!(*addedStates)[state]); assert(compare(above, below) == ABOVE); Node *newNode = new Node(); - nodes.at(state) = newNode; + nodes[state] = newNode; newNode->states = storm::storage::BitVector(numberOfStates); newNode->states.set(state); - setStatesAbove(newNode, above->statesAbove | above->states, false); - setStatesBelow(newNode, below->statesBelow | below->states, false); - setStatesBelow(above, state, true); - setStatesAbove(below, state, true); - - for (auto i = below->statesBelow.getNextSetIndex(0); i < below->statesBelow.size(); i = below->statesBelow.getNextSetIndex(i + 1)) { - setStatesAbove(getNode(i), state, true); - } - - for (auto i = above->statesAbove.getNextSetIndex(0); i < above->statesAbove.size(); i = above->statesAbove.getNextSetIndex(i + 1)) { - setStatesBelow(getNode(i), state, true); - } + newNode->statesAbove = above->states | above->statesAbove; + below->statesAbove |= newNode->states; +// setStatesAbove(newNode, above->statesAbove | above->states, false); +// setStatesBelow(newNode, below->statesBelow | below->states, false); +// setStatesBelow(above, state, true); +// setStatesAbove(below, state, true); + +// for (auto i = below->statesBelow.getNextSetIndex(0); i < below->statesBelow.size(); i = below->statesBelow.getNextSetIndex(i + 1)) { +// setStatesAbove(getNode(i), state, true); +// } +// +// for (auto i = above->statesAbove.getNextSetIndex(0); i < above->statesAbove.size(); i = above->statesAbove.getNextSetIndex(i + 1)) { +// setStatesBelow(getNode(i), state, true); +// } - addedStates.set(state); + addedStates->set(state); } void Lattice::addToNode(uint_fast64_t state, Node *node) { - assert(!addedStates[state]); + assert(!(*addedStates)[state]); node->states.set(state); - nodes.at(state) = node; - addedStates.set(state); - - for (auto i = node->statesBelow.getNextSetIndex(0); i < node->statesBelow.size(); i = node->statesBelow.getNextSetIndex(i + 1)) { - setStatesAbove(getNode(i), state, true); - } + nodes[state] = node; + addedStates->set(state); - for (auto i = node->statesAbove.getNextSetIndex(0); i < node->statesAbove.size(); i = node->statesAbove.getNextSetIndex(i + 1)) { - setStatesBelow(getNode(i), state, true); - } +// for (auto i = node->statesBelow.getNextSetIndex(0); i < node->statesBelow.size(); i = node->statesBelow.getNextSetIndex(i + 1)) { +// setStatesAbove(getNode(i), state, true); +// } +// +// for (auto i = node->statesAbove.getNextSetIndex(0); i < node->statesAbove.size(); i = node->statesAbove.getNextSetIndex(i + 1)) { +// setStatesBelow(getNode(i), state, true); +// } } void Lattice::add(uint_fast64_t state) { - assert(!addedStates[state]); + assert(!(*addedStates)[state]); addBetween(state, top, bottom); } void Lattice::addRelationNodes(Lattice::Node *above, Lattice::Node * below) { assert (compare(above, below) == UNKNOWN); - assert ((above->statesAbove & below->statesBelow).getNumberOfSetBits() == 0); - 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 | 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 | below->statesBelow, true); - } + // TODO: welke assert +// assert ((above->statesAbove & below->statesBelow).getNumberOfSetBits() == 0); +// setStatesBelow(above, below->states | below->statesBelow, true); +// setStatesAbove(below, above->states | above->statesAbove, true); + below->statesAbove |= above->states | above->statesAbove; + +// for (auto i = below->statesBelow.getNextSetIndex(0); i < below->statesBelow.size(); i = below->statesBelow.getNextSetIndex(i + 1)) { +// 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 | below->statesBelow, true); +// } } @@ -189,35 +197,66 @@ namespace storm { return nodes; } - storm::storage::BitVector Lattice::getAddedStates() { + storm::storage::BitVector* Lattice::getAddedStates() { 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)); + std::vector Lattice::sortStates(storm::storage::BitVector* states) { + auto result = std::vector(states->getNumberOfSetBits(), -1); + for (auto state : *states) { + if (result[0] == -1) { + result[0] = state; + } else { + for (auto i = 0; i < states->getNumberOfSetBits() && result[i] != -1; i++) { + auto compareRes = compare(state, result[i]); + if (compareRes == Lattice::ABOVE) { + for (auto j = i; j < states->getNumberOfSetBits() -1 && result[j+1] != -1; j++) { + auto temp = result[j]; + result[j] = state; + result[j+1] = temp; + } + } else if (compareRes == Lattice::UNKNOWN) { + break; + } else if (compareRes == Lattice::SAME) { + for (auto j = i+1; j < states->getNumberOfSetBits() -1 && result[j+1] != -1; j++) { + auto temp = result[j]; + result[j] = state; + result[j+1] = temp; + } + } + } + } } - 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; } +// 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) { + assert (false); std::vector printedNodes = std::vector({}); for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { @@ -237,15 +276,15 @@ namespace storm { out << " Address: " << node << "\n"; out << " Above: {"; - auto statesAbove = getAbove(node); - for (auto itr2 = statesAbove.begin(); itr2 != statesAbove.end(); ++itr2) { - Node *above = *itr2; - index = above->states.getNextSetIndex(0); + auto statesAbove = node->statesAbove; + for (auto above : statesAbove) { + Node* nodeAbove = getNode(above); + index = nodeAbove->states.getNextSetIndex(0); out << "{"; - while (index < above->states.size()) { + while (index < nodeAbove->states.size()) { out << index; - index = above->states.getNextSetIndex(index + 1); - if (index < above->states.size()) { + index = nodeAbove->states.getNextSetIndex(index + 1); + if (index < nodeAbove->states.size()) { out << ", "; } } @@ -255,140 +294,176 @@ namespace storm { out << "}" << "\n"; - out << " Below: {"; - auto statesBelow = getBelow(node); - for (auto itr2 = statesBelow.begin(); itr2 != statesBelow.end(); ++itr2) { - Node *below = *itr2; - out << "{"; - index = below->states.getNextSetIndex(0); - while (index < below->states.size()) { - out << index; - index = below->states.getNextSetIndex(index + 1); - if (index < below->states.size()) { - out << ", "; - } - } - - out << "}"; - } +// out << " Below: {"; +// auto statesBelow = getBelow(node); +// for (auto itr2 = statesBelow.begin(); itr2 != statesBelow.end(); ++itr2) { +// Node *below = *itr2; +// out << "{"; +// index = below->states.getNextSetIndex(0); +// while (index < below->states.size()) { +// out << index; +// index = below->states.getNextSetIndex(index + 1); +// if (index < below->states.size()) { +// out << ", "; +// } +// } +// +// out << "}"; +// } out << "}" << "\n"; } } } void Lattice::toDotFile(std::ostream &out) { - out << "digraph \"Lattice\" {" << std::endl; - - // print all nodes - std::vector printed; - out << "\t" << "node [shape=ellipse]" << std::endl; - for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { + assert (false); +// out << "digraph \"Lattice\" {" << std::endl; +// +// // print all nodes +// std::vector printed; +// out << "\t" << "node [shape=ellipse]" << std::endl; +// for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { +// +// if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) { +// out << "\t\"" << (*itr) << "\" [label = \""; +// uint_fast64_t index = (*itr)->states.getNextSetIndex(0); +// while (index < (*itr)->states.size()) { +// out << index; +// index = (*itr)->states.getNextSetIndex(index + 1); +// if (index < (*itr)->states.size()) { +// out << ", "; +// } +// } +// +// out << "\"]" << std::endl; +// printed.push_back(*itr); +// } +// } +// +// // print arcs +// printed.clear(); +// for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { +// if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) { +// auto below = getBelow(*itr); +// for (auto itr2 = below.begin(); itr2 != below.end(); ++itr2) { +// out << "\t\"" << (*itr) << "\" -> \"" << (*itr2) << "\";" << std::endl; +// } +// printed.push_back(*itr); +// } +// } +// +// out << "}" << std::endl; + } - if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) { - out << "\t\"" << (*itr) << "\" [label = \""; - uint_fast64_t index = (*itr)->states.getNextSetIndex(0); - while (index < (*itr)->states.size()) { - out << index; - index = (*itr)->states.getNextSetIndex(index + 1); - if (index < (*itr)->states.size()) { - out << ", "; - } - } - out << "\"]" << std::endl; - printed.push_back(*itr); + bool Lattice::above(Node *node1, Node *node2) { + // ligt node 1 boven node 2 ? + // oftewel is er een state in node2.above die met een state in node1 matched + bool found = (node2->statesAbove & node1->states).getNumberOfSetBits() != 0; + storm::storage::BitVector statesSeen(node2->statesAbove); + for (auto const& i: node2->statesAbove) { + auto nodeI = getNode(i); + if ((nodeI->statesAbove & statesSeen) != nodeI->statesAbove) { + found = above(node1, nodeI, node2, &statesSeen); } - } - - // print arcs - printed.clear(); - for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { - if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) { - auto below = getBelow(*itr); - for (auto itr2 = below.begin(); itr2 != below.end(); ++itr2) { - out << "\t\"" << (*itr) << "\" -> \"" << (*itr2) << "\";" << std::endl; - } - printed.push_back(*itr); + if (found) { + break; } } - - out << "}" << std::endl; - } - - bool Lattice::above(Node *node1, Node *node2) { - return node1->statesBelow[node2->states.getNextSetIndex(0)]; - } - - void Lattice::setStatesAbove(Lattice::Node *node, uint_fast64_t state, bool alreadyInitialized) { - assert (!node->states[state]); - - if (!alreadyInitialized) { - node->statesAbove = storm::storage::BitVector(numberOfStates); - } - - assert (!node->statesBelow[state]); - node->statesAbove.set(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); - } - assert (!node->statesAbove[state]); - node->statesBelow.set(state); + return found; } - void Lattice::setStatesAbove(Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized) { - assert((states.getNumberOfSetBits() - (node->states & states).getNumberOfSetBits()) != 0); - // the states to add to the above state of the current node shouldnt occur in either statesbelow or states of ndoe - - assert ((node->states & states).getNumberOfSetBits() ==0); - if (alreadyInitialized) { - assert ((node->statesBelow & states).getNumberOfSetBits() == 0); - - node->statesAbove |= (states); - } else { - node->statesAbove = (storm::storage::BitVector(states)); - } - } - - void Lattice::setStatesBelow(Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized) { - assert((states.getNumberOfSetBits() - (node->states & states).getNumberOfSetBits()) != 0); - - assert ((node->states & states).getNumberOfSetBits() ==0); - if (alreadyInitialized) { - assert ((node->statesAbove & states).getNumberOfSetBits() == 0); - node->statesBelow |= (states); - } else { - node->statesBelow = (storm::storage::BitVector(states)); + bool Lattice::above(storm::analysis::Lattice::Node *node1, storm::analysis::Lattice::Node *node2, + storm::analysis::Lattice::Node *nodePrev, storm::storage::BitVector *statesSeen) { + bool found = (node2->statesAbove & node1->states).getNumberOfSetBits() != 0; + // TODO: kan dit niet anders? + statesSeen->operator|=(node2->statesAbove); + nodePrev->statesAbove |= node2->statesAbove; + + storm::storage::BitVector states = storm::storage::BitVector((node2->statesAbove & (statesSeen->operator~()))); + for (auto const& i: states) { +// assert (!statesSeen[i]); + auto nodeI = getNode(i); + if ((nodeI->statesAbove & *statesSeen) != nodeI->statesAbove) { + found = above(node1, nodeI, node2, statesSeen); + } + if (found) { + break; + } } + return found; } +// +// void Lattice::setStatesAbove(Lattice::Node *node, uint_fast64_t state, bool alreadyInitialized) { +// assert (!node->states[state]); +// +// if (!alreadyInitialized) { +// node->statesAbove = storm::storage::BitVector(numberOfStates); +// } +// +// assert (!node->statesBelow[state]); +// node->statesAbove.set(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); +// } +// assert (!node->statesAbove[state]); +// node->statesBelow.set(state); +// } +// +// void Lattice::setStatesAbove(Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized) { +// assert((states.getNumberOfSetBits() - (node->states & states).getNumberOfSetBits()) != 0); +// // the states to add to the above state of the current node shouldnt occur in either statesbelow or states of ndoe +// +// assert ((node->states & states).getNumberOfSetBits() ==0); +// if (alreadyInitialized) { +// assert ((node->statesBelow & states).getNumberOfSetBits() == 0); +// +// node->statesAbove |= (states); +// } else { +// node->statesAbove = (storm::storage::BitVector(states)); +// } +// } +// +// void Lattice::setStatesBelow(Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized) { +// assert((states.getNumberOfSetBits() - (node->states & states).getNumberOfSetBits()) != 0); +// +// assert ((node->states & states).getNumberOfSetBits() ==0); +// if (alreadyInitialized) { +// assert ((node->statesAbove & states).getNumberOfSetBits() == 0); +// node->statesBelow |= (states); +// } else { +// node->statesBelow = (storm::storage::BitVector(states)); +// } +// } void Lattice::mergeNodes(storm::analysis::Lattice::Node *node1, storm::analysis::Lattice::Node *node2) { +// assert (false); // Merges node2 into node 1 // everything above n2 also above n1 node1->statesAbove |= node2->statesAbove; // everything below node 2 also below node 1 - node1->statesBelow |= node2->statesBelow; +// node1->statesBelow |= node2->statesBelow; // add states of node 2 to node 1 node1->states|= node2->states; for(auto i = node2->states.getNextSetIndex(0); i < node2->states.size(); i = node2->states.getNextSetIndex(i+1)) { - nodes.at(i) = node1; + nodes[i] = node1; } - // TODO hier gaat het op magische wijze nog fout - // Add all states of combined node to states Above of all states Below of node1 - for (auto i = node1->statesBelow.getNextSetIndex(0); i < node1->statesBelow.size(); i= node1->statesBelow.getNextSetIndex(i+1)) { - getNode(i)->statesAbove |= node1->states | node1->statesAbove; - } +// // Add all states of combined node to states Above of all states Below of node1 +// for (auto i = node1->statesBelow.getNextSetIndex(0); i < node1->statesBelow.size(); i= node1->statesBelow.getNextSetIndex(i+1)) { +// getNode(i)->statesAbove |= node1->states | node1->statesAbove; +// } // Add all states of combined node to states Below of all states Above of node1 - for (auto i = node1->statesAbove.getNextSetIndex(0); i < node1->statesAbove.size(); i= node1->statesAbove.getNextSetIndex(i+1)) { - getNode(i)->statesBelow |= node1->states | node1->statesBelow; - } +// for (auto i = node1->statesAbove.getNextSetIndex(0); i < node1->statesAbove.size(); i= node1->statesAbove.getNextSetIndex(i+1)) { +// getNode(i)->statesBelow |= node1->states | node1->statesBelow; +// } } } diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 057ff9f30..d47d76bf9 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -19,7 +19,7 @@ namespace storm { struct Node { storm::storage::BitVector states; storm::storage::BitVector statesAbove; - storm::storage::BitVector statesBelow; +// storm::storage::BitVector statesBelow; }; /*! @@ -28,9 +28,9 @@ namespace storm { * @param topNode The top node of the resulting lattice. * @param bottomNode The bottom node of the resulting lattice. */ - Lattice(storm::storage::BitVector topStates, - storm::storage::BitVector bottomStates, - storm::storage::BitVector initialMiddleStates, + Lattice(storm::storage::BitVector* topStates, + storm::storage::BitVector* bottomStates, + storm::storage::BitVector* initialMiddleStates, uint_fast64_t numberOfStates); /*! @@ -117,39 +117,41 @@ namespace storm { * * @return The BitVector with all added states. */ - storm::storage::BitVector getAddedStates(); + storm::storage::BitVector* getAddedStates(); - /*! - * Returns a set with the nodes which are above the state. - * - * @param state The state number. - * @return The set with all nodes which are above the state. - */ - std::set getAbove(uint_fast64_t state); - - /*! - * Returns a set with the nodes which are below the state. - * - * @param state The state number. - * @return The set with all nodes which are below the state. - */ - std::set getBelow(uint_fast64_t state); - - /*! - * Returns a set with the nodes which are above the node. - * - * @param node The node. - * @return The set with all nodes which are above the node. - */ - std::set getAbove(Lattice::Node* node); + std::vector sortStates(storm::storage::BitVector* states); - /*! - * Returns a set with the nodes which are below the node. - * - * @param node The node. - * @return The set with all nodes which are below the node. - */ - std::set getBelow(Lattice::Node* node); +// /*! +// * Returns a set with the nodes which are above the state. +// * +// * @param state The state number. +// * @return The set with all nodes which are above the state. +// */ +// std::set getAbove(uint_fast64_t state); +// +// /*! +// * Returns a set with the nodes which are below the state. +// * +// * @param state The state number. +// * @return The set with all nodes which are below the state. +// */ +// std::set getBelow(uint_fast64_t state); +// +// /*! +// * Returns a set with the nodes which are above the node. +// * +// * @param node The node. +// * @return The set with all nodes which are above the node. +// */ +// std::set getAbove(Lattice::Node* node); +// +// /*! +// * Returns a set with the nodes which are below the node. +// * +// * @param node The node. +// * @return The set with all nodes which are below the node. +// */ +// std::set getBelow(Lattice::Node* node); /*! * Prints a string representation of the lattice to the output stream. @@ -185,7 +187,7 @@ namespace storm { private: std::vector nodes; - storm::storage::BitVector addedStates; + storm::storage::BitVector* addedStates; Node* top; @@ -195,15 +197,17 @@ namespace storm { bool above(Node * node1, Node * node2); + bool above(Node * node1, Node * node2, storm::analysis::Lattice::Node *nodePrev, storm::storage::BitVector *statesSeen); + int compare(Node* node1, Node* node2); - void setStatesAbove(Node* node, uint_fast64_t state, bool alreadyInitialized); +// void setStatesAbove(Node* node, uint_fast64_t state, bool alreadyInitialized); - void setStatesBelow(Node* node, uint_fast64_t state, bool alreadyInitialized); +// void setStatesBelow(Node* node, uint_fast64_t state, bool alreadyInitialized); - void setStatesAbove(storm::analysis::Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized); +// void setStatesAbove(storm::analysis::Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized); - void setStatesBelow(storm::analysis::Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized); +// void setStatesBelow(storm::analysis::Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized); }; } } diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index 4d3d8df7f..045fa6c9c 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -80,13 +80,13 @@ namespace storm { statesSorted = storm::utility::graph::getTopologicalSort(matrix); } else { for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - stateMap[i] = storm::storage::BitVector(numberOfStates, false); + stateMap[i] = new storm::storage::BitVector(numberOfStates, false); auto row = matrix.getRow(i); for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { // ignore self-loops when there are more transitions if (i != rowItr->getColumn() || row.getNumberOfEntries() == 1) { - stateMap[i].set(rowItr->getColumn(), true); + stateMap[i]->set(rowItr->getColumn(), true); } } } @@ -95,16 +95,15 @@ namespace storm { if (scc.size() > 1) { auto states = scc.getStates(); // check if the state has already one successor in bottom of top, in that case pick it - bool found = false; - for (auto stateItr = states.begin(); !found && stateItr < states.end(); ++stateItr) { - auto successors = stateMap[*stateItr]; - if (successors.getNumberOfSetBits() == 2) { - auto succ1 = successors.getNextSetIndex(0); - auto succ2 = successors.getNextSetIndex(succ1 + 1); + for (auto const& state : states) { + auto successors = stateMap[state]; + if (successors->getNumberOfSetBits() == 2) { + auto succ1 = successors->getNextSetIndex(0); + auto succ2 = successors->getNextSetIndex(succ1 + 1); auto intersection = bottomStates | topStates; if (intersection[succ1] || intersection[succ2]) { - initialMiddleStates.set(*stateItr); - found = true; + initialMiddleStates.set(state); + break; } } } @@ -112,10 +111,10 @@ namespace storm { } } - statesToHandle = initialMiddleStates; + statesToHandle = &initialMiddleStates; // Create the Lattice - Lattice *lattice = new Lattice(topStates, bottomStates, initialMiddleStates, numberOfStates); + Lattice *lattice = new Lattice(&topStates, &bottomStates, &initialMiddleStates, numberOfStates); // latticeWatch.stop(); // STORM_PRINT(std::endl << "Time for initialization of lattice: " << latticeWatch << "." << std::endl << std::endl); @@ -179,17 +178,17 @@ namespace storm { } template - std::tuple LatticeExtender::extendAllSuccAdded(Lattice* lattice, uint_fast64_t stateNumber, storm::storage::BitVector successors) { - auto numberOfStates = successors.size(); - assert (lattice->getAddedStates().size() == numberOfStates); + std::tuple LatticeExtender::extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors) { + auto numberOfStates = successors->size(); + assert (lattice->getAddedStates()->size() == numberOfStates); - if (successors.getNumberOfSetBits() == 1) { + if (successors->getNumberOfSetBits() == 1) { // As there is only one successor the current state and its successor must be at the same nodes. - lattice->addToNode(stateNumber, lattice->getNode(successors.getNextSetIndex(0))); - } else if (successors.getNumberOfSetBits() == 2) { + lattice->addToNode(stateNumber, lattice->getNode(successors->getNextSetIndex(0))); + } else if (successors->getNumberOfSetBits() == 2) { // Otherwise, check how the two states compare, and add if the comparison is possible. - uint_fast64_t successor1 = successors.getNextSetIndex(0); - uint_fast64_t successor2 = successors.getNextSetIndex(successor1 + 1); + uint_fast64_t successor1 = successors->getNextSetIndex(0); + uint_fast64_t successor2 = successors->getNextSetIndex(successor1 + 1); int compareResult = lattice->compare(successor1, successor2); if (compareResult == Lattice::ABOVE) { @@ -207,18 +206,18 @@ namespace storm { assert(lattice->compare(successor1, successor2) == Lattice::UNKNOWN); return std::make_tuple(lattice, successor1, successor2); } - } else if (successors.getNumberOfSetBits() > 2) { - for (auto i = successors.getNextSetIndex(0); i < numberOfStates; i = successors.getNextSetIndex(i+1)) { - for (auto j = successors.getNextSetIndex(i+1); j < numberOfStates; j = successors.getNextSetIndex(j+1)) { + } else if (successors->getNumberOfSetBits() > 2) { + for (auto const& i : *successors) { + for (auto j = successors->getNextSetIndex(i+1); j < numberOfStates; j = successors->getNextSetIndex(j+1)) { if (lattice->compare(i,j) == Lattice::UNKNOWN) { return std::make_tuple(lattice, i, j); } } } - auto highest = successors.getNextSetIndex(0); + auto highest = successors->getNextSetIndex(0); auto lowest = highest; - for (auto i = successors.getNextSetIndex(highest+1); i < numberOfStates; i = successors.getNextSetIndex(i+1)) { + for (auto i = successors->getNextSetIndex(highest+1); i < numberOfStates; i = successors->getNextSetIndex(i+1)) { if (lattice->compare(i, highest) == Lattice::ABOVE) { highest = i; } @@ -246,31 +245,30 @@ namespace storm { } auto oldNumberSet = numberOfStates; - while (oldNumberSet != lattice->getAddedStates().getNumberOfSetBits()) { - oldNumberSet = lattice->getAddedStates().getNumberOfSetBits(); + while (oldNumberSet != lattice->getAddedStates()->getNumberOfSetBits()) { + oldNumberSet = lattice->getAddedStates()->getNumberOfSetBits(); if (!assumptionSeen && acyclic) { if (statesSorted.size() > 0) { auto nextState = *(statesSorted.begin()); - while (lattice->getAddedStates()[nextState] && statesSorted.size() > 1) { + while ((*(lattice->getAddedStates()))[nextState] && statesSorted.size() > 1) { // states.size()>1 such that there is at least one state left after erase statesSorted.erase(statesSorted.begin()); nextState = *(statesSorted.begin()); } - if (!lattice->getAddedStates()[nextState]) { + if (!(*(lattice->getAddedStates()))[nextState]) { auto row = this->model->getTransitionMatrix().getRow(nextState); - auto successors = storm::storage::BitVector(lattice->getAddedStates().size()); + auto successors = new storm::storage::BitVector(lattice->getAddedStates()->size()); for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { // ignore self-loops when there are more transitions if (nextState != rowItr->getColumn()) { - successors.set(rowItr->getColumn()); + successors->set(rowItr->getColumn()); } } - auto seenStates = (lattice->getAddedStates()); - assert ((seenStates & successors) == successors); + assert ((*(lattice->getAddedStates()) & *successors) == *successors); auto result = extendAllSuccAdded(lattice, nextState, successors); if (std::get<1>(result) != numberOfStates) { @@ -280,33 +278,32 @@ namespace storm { statesSorted.erase(statesSorted.begin()); } } - auto added = lattice->getAddedStates().getNumberOfSetBits(); + auto added = lattice->getAddedStates()->getNumberOfSetBits(); assert (lattice->getNode(nextState) != nullptr); - assert (lattice->getAddedStates()[nextState]); + assert ((*lattice->getAddedStates())[nextState]); } } else if (assumptionSeen && acyclic) { auto states = statesSorted; if (states.size() > 0) { auto nextState = *(states.begin()); - while (lattice->getAddedStates()[nextState] && states.size() > 1) { + while ((*(lattice->getAddedStates()))[nextState] && states.size() > 1) { // states.size()>1 such that there is at least one state left after erase states.erase(states.begin()); nextState = *(states.begin()); } - if (!lattice->getAddedStates()[nextState]) { + if (!(*(lattice->getAddedStates()))[nextState]) { auto row = this->model->getTransitionMatrix().getRow(nextState); - auto successors = storm::storage::BitVector(lattice->getAddedStates().size()); + auto successors = new storm::storage::BitVector(lattice->getAddedStates()->size()); for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { // ignore self-loops when there are more transitions if (nextState != rowItr->getColumn()) { - successors.set(rowItr->getColumn()); + successors->set(rowItr->getColumn()); } } - auto seenStates = (lattice->getAddedStates()); - assert ((seenStates & successors) == successors); + assert ((*(lattice->getAddedStates()) & *successors) == *successors); auto result = extendAllSuccAdded(lattice, nextState, successors); if (std::get<1>(result) != numberOfStates) { @@ -320,9 +317,8 @@ namespace storm { } } - auto added = lattice->getAddedStates().getNumberOfSetBits(); assert (lattice->getNode(nextState) != nullptr); - assert (lattice->getAddedStates()[nextState]); + assert ((*lattice->getAddedStates())[nextState]); } } else if (!acyclic) { @@ -331,20 +327,20 @@ namespace storm { if (assumptionSeen) { statesToHandle = addedStates; } - auto stateNumber = statesToHandle.getNextSetIndex(0); + auto stateNumber = statesToHandle->getNextSetIndex(0); while (stateNumber != numberOfStates) { addedStates = lattice->getAddedStates(); - storm::storage::BitVector successors = stateMap[stateNumber]; + storm::storage::BitVector* successors = stateMap[stateNumber]; // Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet - auto succ1 = successors.getNextSetIndex(0); - auto succ2 = successors.getNextSetIndex(succ1 + 1); + auto succ1 = successors->getNextSetIndex(0); + auto succ2 = successors->getNextSetIndex(succ1 + 1); - assert (addedStates[stateNumber]); - if (successors.getNumberOfSetBits() == 2 - && ((addedStates[succ1] && !addedStates[succ2]) - || (!addedStates[succ1] && addedStates[succ2]))) { + assert ((*addedStates)[stateNumber]); + if (successors->getNumberOfSetBits() == 2 + && (((*(addedStates))[succ1] && !(*(addedStates))[succ2]) + || (!(*(addedStates))[succ1] && (*(addedStates))[succ2]))) { - if (!addedStates[succ1]) { + if (!(*(addedStates))[succ1]) { std::swap(succ1, succ2); } @@ -356,45 +352,45 @@ namespace storm { } else { assert(false); } - statesToHandle.set(succ2); - statesToHandle.set(stateNumber, false); - stateNumber = statesToHandle.getNextSetIndex(0); - } else if (!((addedStates[succ1] && !addedStates[succ2]) - || (!addedStates[succ1] && addedStates[succ2]))) { - stateNumber = statesToHandle.getNextSetIndex(stateNumber + 1); + statesToHandle->set(succ2); + statesToHandle->set(stateNumber, false); + stateNumber = statesToHandle->getNextSetIndex(0); + } else if (!(((*(addedStates))[succ1] && !(*(addedStates))[succ2]) + || (!(*(addedStates))[succ1] && (*(addedStates))[succ2]))) { + stateNumber = statesToHandle->getNextSetIndex(stateNumber + 1); } else { - assert (successors.getNumberOfSetBits() == 2); - statesToHandle.set(stateNumber, false); - stateNumber = statesToHandle.getNextSetIndex(0); + assert (successors->getNumberOfSetBits() == 2); + statesToHandle->set(stateNumber, false); + stateNumber = statesToHandle->getNextSetIndex(0); } } addedStates = lattice->getAddedStates(); - for (auto stateNumber = addedStates.getNextUnsetIndex(0); stateNumber < numberOfStates; stateNumber = addedStates.getNextUnsetIndex(stateNumber + 1)) { + for (auto stateNumber : *addedStates) { // Iterate over all not yet added states - storm::storage::BitVector successors = stateMap[stateNumber]; + storm::storage::BitVector* successors = stateMap[stateNumber]; // Check if current state has not been added yet, and all successors have, ignore selfloop in this - successors.set(stateNumber, false); - if ((successors & addedStates) == successors) { + successors->set(stateNumber, false); + if ((*successors & *addedStates) == *successors) { auto result = extendAllSuccAdded(lattice, stateNumber, successors); - if (std::get<1>(result) != successors.size()) { + if (std::get<1>(result) != successors->size()) { return result; } - statesToHandle.set(stateNumber); + statesToHandle->set(stateNumber); } } // if nothing changed and there are states left, then add a state between top and bottom - if (oldNumberSet == lattice->getAddedStates().getNumberOfSetBits() && oldNumberSet != numberOfStates) { - auto stateNumber = lattice->getAddedStates().getNextUnsetIndex(0); + if (oldNumberSet == lattice->getAddedStates()->getNumberOfSetBits() && oldNumberSet != numberOfStates) { + auto stateNumber = lattice->getAddedStates()->getNextUnsetIndex(0); lattice->add(stateNumber); - statesToHandle.set(stateNumber); + statesToHandle->set(stateNumber); } } } - assert (lattice->getAddedStates().getNumberOfSetBits() == numberOfStates); + assert (lattice->getAddedStates()->getNumberOfSetBits() == numberOfStates); return std::make_tuple(lattice, numberOfStates, numberOfStates); } template class LatticeExtender; diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index 0d4787f00..63f224792 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -52,7 +52,7 @@ namespace storm { private: std::shared_ptr> model; - std::map stateMap; + std::map stateMap; std::vector statesSorted; @@ -60,11 +60,11 @@ namespace storm { bool assumptionSeen; - storm::storage::BitVector statesToHandle; + storm::storage::BitVector* statesToHandle; void handleAssumption(Lattice* lattice, std::shared_ptr assumption); - std::tuple extendAllSuccAdded(Lattice* lattice, uint_fast64_t stateNumber, storm::storage::BitVector successors); + std::tuple extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors); }; } } diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 26b23673e..8c5214ca0 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -26,6 +26,7 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/RationalFunctionToExpression.h" +#include "storm/utility/constants.h" namespace storm { namespace analysis { @@ -151,8 +152,8 @@ namespace storm { for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) { auto lattice = itr->first; - auto addedStates = lattice->getAddedStates().getNumberOfSetBits(); - assert (addedStates == lattice->getAddedStates().size()); + auto addedStates = lattice->getAddedStates()->getNumberOfSetBits(); + assert (addedStates == lattice->getAddedStates()->size()); std::map> varsMonotone = analyseMonotonicity(i, lattice, matrix); @@ -299,7 +300,7 @@ namespace storm { auto numberOfStates = model->getNumberOfStates(); if (val1 == numberOfStates || val2 == numberOfStates) { assert (val1 == val2); - assert (lattice->getAddedStates().size() == lattice->getAddedStates().getNumberOfSetBits()); + assert (lattice->getAddedStates()->size() == lattice->getAddedStates()->getNumberOfSetBits()); result.insert(std::pair>>(lattice, assumptions)); } else { @@ -388,26 +389,55 @@ namespace storm { return result; } + template + ValueType MonotonicityChecker::getDerivative(ValueType function, carl::Variable var) { + if (function.isConstant()) { + return storm::utility::zero(); + } + if ((derivatives[function]).find(var) == (derivatives[function]).end()) { + (derivatives[function])[var] = function.derivative(var); + } + + return (derivatives[function])[var]; + } + template std::map> MonotonicityChecker::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) { // storm::utility::Stopwatch analyseWatch(true); + std::cout << "Analyzing monotonicity" << std::endl; std::map> varsMonotone; for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { // go over all rows auto row = matrix.getRow(i); - auto first = (*row.begin()); - if (first.getValue() != ValueType(1)) { + // only enter if you are in a state with at least two successors (so there must be successors, + // and first prob shouldnt be 1) + if (row.begin() != row.end() && !row.begin()->getValue().isOne()) { std::map transitions; - for (auto itr = row.begin(); itr != row.end(); ++itr) { - transitions.insert(std::pair((*itr).getColumn(), (*itr).getValue())); + auto states = new storm::storage::BitVector(matrix.getColumnCount()); + std::set vars; + for (auto const& entry : row) { + if (!entry.getValue().isConstant()) { + // only analyse take non constant transitions + transitions.insert(std::pair(entry.getColumn(), entry.getValue())); + for (auto const& var:entry.getValue().gatherVariables()) { + vars.insert(var); + states->set(entry.getColumn()); + } + } } - auto val = first.getValue(); - auto vars = val.gatherVariables(); - for (auto itr = vars.begin(); itr != vars.end(); ++itr) { + auto sortedStates = lattice->sortStates(states); + + assert (sortedStates.size() >=2); + + assert (sortedStates.size() == states->getNumberOfSetBits()); + if (sortedStates[sortedStates.size() - 1] == -1) { +// auto val = first.getValue(); +// auto vars = val.gatherVariables(); + for (auto itr = vars.begin(); itr != vars.end(); ++itr) { // if (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end() && // (!resultCheckOnSamples[*itr].first && !resultCheckOnSamples[*itr].second)) { // if (varsMonotone.find(*itr) == varsMonotone.end()) { @@ -422,42 +452,85 @@ namespace storm { std::pair *value = &varsMonotone.find(*itr)->second; std::pair old = *value; + + // states are not properly sorted for (auto itr2 = transitions.begin(); itr2 != transitions.end(); ++itr2) { for (auto itr3 = transitions.begin(); itr3 != transitions.end(); ++itr3) { - auto derivative2 = itr2->second.derivative(*itr); - auto derivative3 = itr3->second.derivative(*itr); - - auto compare = lattice->compare(itr2->first, itr3->first); - - if (compare == storm::analysis::Lattice::ABOVE) { - // As the first state (itr2) is above the second state (itr3) it is sufficient to look at the derivative of itr2. - std::pair mon2; - if (derivative2.isConstant()) { - mon2 = std::pair(derivative2.constantPart() >= 0, derivative2.constantPart() <=0); - } else { - mon2 = checkDerivative(derivative2); - } - value->first &= mon2.first; - value->second &= mon2.second; - } else if (compare == storm::analysis::Lattice::BELOW) { - // As the second state (itr3) is above the first state (itr2) it is sufficient to look at the derivative of itr3. - std::pair mon3; - if (derivative2.isConstant()) { - mon3 = std::pair(derivative3.constantPart() >= 0, derivative3.constantPart() <=0); + if (itr2->first < itr3->first) { + + auto derivative2 = getDerivative(itr2->second, *itr); + auto derivative3 = getDerivative(itr3->second, *itr); + + auto compare = lattice->compare(itr2->first, itr3->first); + + if (compare == storm::analysis::Lattice::ABOVE) { + // As the first state (itr2) is above the second state (itr3) it is sufficient to look at the derivative of itr2. + std::pair mon2; + if (derivative2.isConstant()) { + mon2 = std::pair(derivative2.constantPart() >= 0, + derivative2.constantPart() <= 0); + } else { + mon2 = checkDerivative(derivative2); + } + value->first &= mon2.first; + value->second &= mon2.second; + } else if (compare == storm::analysis::Lattice::BELOW) { + // As the second state (itr3) is above the first state (itr2) it is sufficient to look at the derivative of itr3. + std::pair mon3; + if (derivative2.isConstant()) { + mon3 = std::pair(derivative3.constantPart() >= 0, + derivative3.constantPart() <= 0); + } else { + mon3 = checkDerivative(derivative3); + } + value->first &= mon3.first; + value->second &= mon3.second; + } else if (compare == storm::analysis::Lattice::SAME) { + // TODO: klopt dit + // Behaviour doesn't matter, as the states are at the same level. } else { - mon3 = checkDerivative(derivative3); + // As the relation between the states is unknown, we can't claim anything about the monotonicity. + value->first = false; + value->second = false; } - value->first &= mon3.first; - value->second &= mon3.second; - } else if (compare == storm::analysis::Lattice::SAME) { - // TODO: klopt dit - // Behaviour doesn't matter, as the states are at the same level. - } else { - // As the relation between the states is unknown, we can't claim anything about the monotonicity. - value->first = false; - value->second = false; } // } + } + } + } + } else { + bool change = false; + for (auto var : vars) { +// if (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end() && +// (!resultCheckOnSamples[*itr].first && !resultCheckOnSamples[*itr].second)) { +// if (varsMonotone.find(*itr) == varsMonotone.end()) { +// varsMonotone[*itr].first = false; +// varsMonotone[*itr].second = false; +// } +// } else { + if (varsMonotone.find(var) == varsMonotone.end()) { + varsMonotone[var].first = true; + varsMonotone[var].second = true; + } + std::pair *value = &varsMonotone.find(var)->second; + + for (auto const &i : sortedStates) { +// auto res = checkDerivative(transitions[i].derivative(var)); + auto res = checkDerivative(getDerivative(transitions[i], var)); + change = change || (!(value->first && value->second) // they do not hold both + && ((value->first && !res.first) + || (value->second && !res.second))); + + if (change) { + value->first &= res.second; + value->second &= res.first; + } else { + value->first &= res.first; + value->second &= res.second; + } + if (!value->first && !value->second) { + break; + } } } } @@ -478,6 +551,9 @@ namespace storm { if (derivative.isZero()) { monIncr = true; monDecr = true; + } else if (derivative.isConstant()) { + monIncr = derivative.constantPart() >= 0; + monDecr = derivative.constantPart() <= 0; } else { std::shared_ptr smtSolverFactory = std::make_shared(); diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index b4b6db84c..94cb39ff3 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -62,6 +62,10 @@ namespace storm { std::pair checkDerivative(ValueType derivative); + std::unordered_map> derivatives; + + ValueType getDerivative(ValueType function, carl::Variable var); + std::vector> checkAssumptionsOnRegion(std::vector> assumptions); std::map>> extendLatticeWithAssumptions(storm::analysis::Lattice* lattice, storm::analysis::AssumptionMaker* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector> assumptions); diff --git a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp index b8ac1981e..ab0b25d18 100644 --- a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp @@ -82,7 +82,7 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) { below.set(1); storm::storage::BitVector initialMiddle(8); - auto dummyLattice = new storm::analysis::Lattice(above, below, initialMiddle, 8); + auto dummyLattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 8); // Validate assumption EXPECT_FALSE(checker.validateAssumption(assumption, dummyLattice)); EXPECT_FALSE(checker.validated(assumption)); @@ -99,7 +99,7 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) { below = storm::storage::BitVector(13); below.set(9); initialMiddle = storm::storage::BitVector(13); - dummyLattice = new storm::analysis::Lattice(above, below, initialMiddle, 13); + dummyLattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 13); EXPECT_FALSE(checker.checkOnSamples(assumption)); EXPECT_FALSE(checker.validateAssumption(assumption, dummyLattice)); EXPECT_TRUE(checker.validated(assumption)); diff --git a/src/test/storm-pars/analysis/LatticeExtenderTest.cpp b/src/test/storm-pars/analysis/LatticeExtenderTest.cpp index 59f739b84..b174d3873 100644 --- a/src/test/storm-pars/analysis/LatticeExtenderTest.cpp +++ b/src/test/storm-pars/analysis/LatticeExtenderTest.cpp @@ -59,7 +59,7 @@ TEST(LatticeExtenderTest, Brp_with_bisimulation) { auto lattice = std::get<0>(criticalTuple); for (auto i = 0; i < dtmc->getNumberOfStates(); ++i) { - EXPECT_TRUE(lattice->getAddedStates()[i]); + EXPECT_TRUE((*lattice->getAddedStates())[i]); } // Check on some nodes diff --git a/src/test/storm-pars/analysis/LatticeTest.cpp b/src/test/storm-pars/analysis/LatticeTest.cpp index ad65b98c7..27806bc50 100644 --- a/src/test/storm-pars/analysis/LatticeTest.cpp +++ b/src/test/storm-pars/analysis/LatticeTest.cpp @@ -17,7 +17,7 @@ TEST(LatticeTest, Simple) { below.set(1); auto initialMiddle = storm::storage::BitVector(numberOfStates); - auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates); + auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates); EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,1)); EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,0)); EXPECT_EQ(nullptr, lattice.getNode(2)); @@ -83,7 +83,7 @@ TEST(LatticeTest, copy_lattice) { below.set(1); auto initialMiddle = storm::storage::BitVector(numberOfStates); - auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates); + auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates); lattice.add(2); lattice.add(3); lattice.addToNode(4, lattice.getNode(2)); @@ -148,7 +148,7 @@ TEST(LatticeTest, merge_nodes) { below.set(1); auto initialMiddle = storm::storage::BitVector(numberOfStates); - auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates); + auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates); lattice.add(2); lattice.add(3); lattice.addToNode(4, lattice.getNode(2)); diff --git a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp index 12631b65a..3367f3d09 100644 --- a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp @@ -38,7 +38,7 @@ TEST(MonotonicityCheckerTest, Monotone_no_model) { auto below = storm::storage::BitVector(numberOfStates); below.set(0); auto initialMiddle = storm::storage::BitVector(numberOfStates); - auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates); + auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates); lattice.add(2); lattice.add(3); // Build map @@ -84,7 +84,7 @@ TEST(MonotonicityCheckerTest, Not_monotone_no_model) { auto below = storm::storage::BitVector(numberOfStates); below.set(0); auto initialMiddle = storm::storage::BitVector(numberOfStates); - auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates); + auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates); lattice.add(2); lattice.add(3); // Build map