sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Speedup

main
Jip Spel 6 years ago
parent
f41b61fb7b
commit
26429925d6
10 changed files with 517 additions and 362 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 475
      src/storm-pars/analysis/Lattice.cpp
  2. 84
      src/storm-pars/analysis/Lattice.h
  3. 138
      src/storm-pars/analysis/LatticeExtender.cpp
  4. 6
      src/storm-pars/analysis/LatticeExtender.h
  5. 156
      src/storm-pars/analysis/MonotonicityChecker.cpp
  6. 4
      src/storm-pars/analysis/MonotonicityChecker.h
  7. 4
      src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
  8. 2
      src/test/storm-pars/analysis/LatticeExtenderTest.cpp
  9. 6
      src/test/storm-pars/analysis/LatticeTest.cpp
  10. 4
      src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp

475
src/storm-pars/analysis/Lattice.cpp
View File

@ -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<Node *>(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<Node *>(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::Node*> Lattice::getAbove(uint_fast64_t state) {
return getAbove(getNode(state));
}
std::set<Lattice::Node*> Lattice::getBelow(uint_fast64_t state) {
return getBelow(getNode(state));
}
std::set<Lattice::Node*> Lattice::getAbove(Lattice::Node* node) {
std::set<Lattice::Node*> result({});
for (auto i = node->statesAbove.getNextSetIndex(0); i < node->statesAbove.size(); i = node->statesAbove.getNextSetIndex(i + 1)) {
result.insert(getNode(i));
std::vector<uint_fast64_t> Lattice::sortStates(storm::storage::BitVector* states) {
auto result = std::vector<uint_fast64_t>(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::Node*> Lattice::getBelow(Lattice::Node* node) {
std::set<Lattice::Node*> 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::Node*> Lattice::getAbove(uint_fast64_t state) {
// return getAbove(getNode(state));
// }
//
// std::set<Lattice::Node*> Lattice::getBelow(uint_fast64_t state) {
// return getBelow(getNode(state));
// }
//
// std::set<Lattice::Node*> Lattice::getAbove(Lattice::Node* node) {
// std::set<Lattice::Node*> 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::Node*> Lattice::getBelow(Lattice::Node* node) {
// std::set<Lattice::Node*> 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<Node*> printedNodes = std::vector<Node*>({});
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<Node*> 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<Node*> 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;
// }
}
}

84
src/storm-pars/analysis/Lattice.h
View File

@ -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<Lattice::Node*> 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<Lattice::Node*> 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<Lattice::Node*> getAbove(Lattice::Node* node);
std::vector<uint_fast64_t> 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<Lattice::Node*> 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<Lattice::Node*> 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<Lattice::Node*> 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<Lattice::Node*> 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<Lattice::Node*> getBelow(Lattice::Node* node);
/*!
* Prints a string representation of the lattice to the output stream.
@ -185,7 +187,7 @@ namespace storm {
private:
std::vector<Node*> 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);
};
}
}

138
src/storm-pars/analysis/LatticeExtender.cpp
View File

@ -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 <typename ValueType>
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendAllSuccAdded(Lattice* lattice, uint_fast64_t stateNumber, storm::storage::BitVector successors) {
auto numberOfStates = successors.size();
assert (lattice->getAddedStates().size() == numberOfStates);
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::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<storm::RationalFunction>;

6
src/storm-pars/analysis/LatticeExtender.h
View File

@ -52,7 +52,7 @@ namespace storm {
private:
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::map<uint_fast64_t, storm::storage::BitVector> stateMap;
std::map<uint_fast64_t, storm::storage::BitVector*> stateMap;
std::vector<uint_fast64_t> statesSorted;
@ -60,11 +60,11 @@ namespace storm {
bool assumptionSeen;
storm::storage::BitVector statesToHandle;
storm::storage::BitVector* statesToHandle;
void handleAssumption(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> extendAllSuccAdded(Lattice* lattice, uint_fast64_t stateNumber, storm::storage::BitVector successors);
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors);
};
}
}

156
src/storm-pars/analysis/MonotonicityChecker.cpp
View File

@ -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<carl::Variable, std::pair<bool, bool>> 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<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, assumptions));
} else {
@ -388,26 +389,55 @@ namespace storm {
return result;
}
template <typename ValueType>
ValueType MonotonicityChecker<ValueType>::getDerivative(ValueType function, carl::Variable var) {
if (function.isConstant()) {
return storm::utility::zero<ValueType>();
}
if ((derivatives[function]).find(var) == (derivatives[function]).end()) {
(derivatives[function])[var] = function.derivative(var);
}
return (derivatives[function])[var];
}
template <typename ValueType>
std::map<carl::Variable, std::pair<bool, bool>> MonotonicityChecker<ValueType>::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) {
// storm::utility::Stopwatch analyseWatch(true);
std::cout << "Analyzing monotonicity" << std::endl;
std::map<carl::Variable, std::pair<bool, bool>> 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<uint_fast64_t, ValueType> transitions;
for (auto itr = row.begin(); itr != row.end(); ++itr) {
transitions.insert(std::pair<uint_fast64_t, ValueType>((*itr).getColumn(), (*itr).getValue()));
auto states = new storm::storage::BitVector(matrix.getColumnCount());
std::set<carl::Variable> vars;
for (auto const& entry : row) {
if (!entry.getValue().isConstant()) {
// only analyse take non constant transitions
transitions.insert(std::pair<uint_fast64_t, ValueType>(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<bool, bool> *value = &varsMonotone.find(*itr)->second;
std::pair<bool, bool> 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<bool,bool> mon2;
if (derivative2.isConstant()) {
mon2 = std::pair<bool,bool>(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<bool,bool> mon3;
if (derivative2.isConstant()) {
mon3 = std::pair<bool,bool>(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<bool, bool> mon2;
if (derivative2.isConstant()) {
mon2 = std::pair<bool, bool>(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<bool, bool> mon3;
if (derivative2.isConstant()) {
mon3 = std::pair<bool, bool>(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<bool, bool> *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<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();

4
src/storm-pars/analysis/MonotonicityChecker.h
View File

@ -62,6 +62,10 @@ namespace storm {
std::pair<bool, bool> checkDerivative(ValueType derivative);
std::unordered_map<ValueType, std::unordered_map<carl::Variable, ValueType>> derivatives;
ValueType getDerivative(ValueType function, carl::Variable var);
std::vector<storm::storage::ParameterRegion<ValueType>> checkAssumptionsOnRegion(std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> extendLatticeWithAssumptions(storm::analysis::Lattice* lattice, storm::analysis::AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);

4
src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
View File

@ -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));

2
src/test/storm-pars/analysis/LatticeExtenderTest.cpp
View File

@ -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

6
src/test/storm-pars/analysis/LatticeTest.cpp
View File

@ -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));

4
src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp
View File

@ -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

Write Preview
Loading…
Cancel
Save