Browse Source

Make sure statesAbove/Below are set correctly

tempestpy_adaptions
Jip Spel 6 years ago
parent
commit
7563d168e4
  1. 107
      src/storm-pars/analysis/Lattice.cpp
  2. 10
      src/storm-pars/analysis/Lattice.h
  3. 42
      src/storm-pars/analysis/LatticeExtender.cpp
  4. 1
      src/storm-pars/analysis/MonotonicityChecker.cpp

107
src/storm-pars/analysis/Lattice.cpp

@ -27,25 +27,19 @@ namespace storm {
nodes.at(i) = bottom;
}
top->above = new std::set<Lattice::Node*>({});
top->statesAbove = storm::storage::BitVector(numberOfStates);
setStatesBelow(top, bottomStates, false);
assert(top->statesAbove.size() == numberOfStates);
assert(top->statesBelow.size() == numberOfStates);
assert(top->statesAbove.getNumberOfSetBits() == 0);
assert(top->statesBelow.getNumberOfSetBits() == bottomStates.getNumberOfSetBits());
assert(top->above->size() == 0);
assert(top->below->size() == bottomStates.getNumberOfSetBits());
bottom->below = new std::set<Lattice::Node*>({});
bottom->statesBelow = storm::storage::BitVector(numberOfStates);
setStatesAbove(bottom, topStates, false);
assert(bottom->statesAbove.size() == numberOfStates);
assert(bottom->statesBelow.size() == numberOfStates);
assert(bottom->statesBelow.getNumberOfSetBits() == 0);
assert(bottom->statesAbove.getNumberOfSetBits() == topStates.getNumberOfSetBits());
assert(bottom->below->size() == 0);
assert(bottom->above->size() == topStates.getNumberOfSetBits());
this->numberOfStates = numberOfStates;
this->addedStates = storm::storage::BitVector(numberOfStates);
@ -56,28 +50,13 @@ namespace storm {
Lattice::Lattice(Lattice* lattice) {
numberOfStates = lattice->getAddedStates().size();
nodes = std::vector<Node *>(numberOfStates);
top = new Node();
top->states = storm::storage::BitVector(lattice->getTop()->states);
for (auto i = top->states.getNextSetIndex(0); i < top->states.size(); i = top->states.getNextSetIndex(i+1)) {
nodes.at(i) = top;
}
bottom = new Node();
bottom->states = storm::storage::BitVector(lattice->getBottom()->states);
for (auto i = bottom->states.getNextSetIndex(0); i < bottom->states.size(); i = bottom->states.getNextSetIndex(i+1)) {
nodes.at(i) = bottom;
}
addedStates = storm::storage::BitVector(numberOfStates);
addedStates |= (top->states);
addedStates |= (bottom->states);
auto oldNodes = lattice->getNodes();
// Create nodes
for (auto itr = oldNodes.begin(); itr != oldNodes.end(); ++itr) {
Node *oldNode = (*itr);
if (oldNode != nullptr && oldNode != lattice->getTop() && oldNode != lattice->getBottom()) {
if (oldNode != nullptr) {
Node *newNode = new Node();
newNode->states = storm::storage::BitVector(oldNode->states);
for (auto i = newNode->states.getNextSetIndex(0);
@ -85,6 +64,11 @@ namespace storm {
addedStates.set(i);
nodes.at(i) = newNode;
}
if (oldNode == lattice->getTop()) {
top = newNode;
} else if (oldNode == lattice->getBottom()) {
bottom = newNode;
}
}
}
assert(addedStates == lattice->getAddedStates());
@ -98,27 +82,18 @@ namespace storm {
setStatesBelow(newNode, oldNode->statesBelow, false);
} else if (oldNode != nullptr && oldNode == lattice->getBottom()) {
setStatesAbove(bottom, lattice->getBottom()->statesAbove, false);
assert(lattice->getBottom()->statesBelow.getNumberOfSetBits() == 0);
bottom->below = new std::set<Lattice::Node*>({});
bottom->statesBelow = storm::storage::BitVector(numberOfStates);
assert(bottom->statesAbove.size() == numberOfStates);
assert(bottom->statesBelow.size() == numberOfStates);
} else if (oldNode != nullptr && oldNode == lattice->getTop()) {
top->above = new std::set<Lattice::Node*>({});
top->statesAbove = storm::storage::BitVector(numberOfStates);
assert(lattice->getTop()->statesAbove.getNumberOfSetBits() == 0);
setStatesBelow(top, lattice->getTop()->statesBelow, false);
assert(top->statesAbove.size() == numberOfStates);
assert(top->statesBelow.size() == numberOfStates);
}
// To check if everything went well
if (oldNode!= nullptr) {
Node *newNode = getNode(oldNode->states.getNextSetIndex(0));
assert((newNode->statesAbove & newNode->statesBelow).getNumberOfSetBits() == 0);
assert(newNode->statesAbove == oldNode->statesAbove);
assert(newNode->statesBelow == oldNode->statesBelow);
assert(newNode->above->size() == oldNode->above->size());
assert(newNode->below->size() == oldNode->below->size());
}
}
}
@ -167,17 +142,16 @@ namespace storm {
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, true);
setStatesAbove(below, above->states, true);
setStatesBelow(above, below->states | below->statesBelow, true);
setStatesAbove(below, above->states | above->statesAbove, true);
for (auto i = below->statesBelow.getNextSetIndex(0); i < below->statesBelow.size(); i = below->statesBelow.getNextSetIndex(i + 1)) {
setStatesAbove(getNode(i), above->states, true);
setStatesAbove(getNode(i), above->states | above->statesAbove, true);
}
for (auto i = above->statesAbove.getNextSetIndex(0); i < above->statesAbove.size(); i = above->statesAbove.getNextSetIndex(i + 1)) {
setStatesBelow(getNode(i), below->states, true);
setStatesBelow(getNode(i), below->states | below->statesBelow, true);
}
}
@ -223,6 +197,30 @@ namespace storm {
return addedStates;
}
std::set<Lattice::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) {
std::vector<Node*> printedNodes = std::vector<Node*>({});
for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
@ -243,7 +241,8 @@ namespace storm {
out << " Address: " << node << "\n";
out << " Above: {";
for (auto itr2 = node->above->begin(); itr2 != node->above->end(); ++itr2) {
auto statesAbove = getAbove(node);
for (auto itr2 = statesAbove.begin(); itr2 != statesAbove.end(); ++itr2) {
Node *above = *itr2;
index = above->states.getNextSetIndex(0);
out << "{";
@ -261,7 +260,8 @@ namespace storm {
out << " Below: {";
for (auto itr2 = node->below->begin(); itr2 != node->below->end(); ++itr2) {
auto statesBelow = getBelow(node);
for (auto itr2 = statesBelow.begin(); itr2 != statesBelow.end(); ++itr2) {
Node *below = *itr2;
out << "{";
index = below->states.getNextSetIndex(0);
@ -308,8 +308,8 @@ namespace storm {
printed.clear();
for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) {
auto below = (*itr)->below;
for (auto itr2 = below->begin(); itr2 != below->end(); ++itr2) {
auto below = getBelow(*itr);
for (auto itr2 = below.begin(); itr2 != below.end(); ++itr2) {
out << "\t\"" << (*itr) << "\" -> \"" << (*itr2) << "\";" << std::endl;
}
printed.push_back(*itr);
@ -320,6 +320,21 @@ namespace storm {
}
bool Lattice::above(Node *node1, Node *node2) {
bool check = node1->statesBelow.get(node2->states.getNextSetIndex(0));
for (auto i = node2->states.getNextSetIndex(0); i < node2->states.size(); i = node2->states.getNextSetIndex(i+1)) {
if (check) {
assert(node1->statesBelow.get(i));
} else {
assert(!node1->statesBelow.get(i));
}
}
for (auto i = node1->states.getNextSetIndex(0); i < node1->states.size(); i = node1->states.getNextSetIndex(i+1)) {
if (check) {
assert(node2->statesAbove.get(i));
} else {
assert(!node2->statesAbove.get(i));
}
}
return node1->statesBelow.get(node2->states.getNextSetIndex(0));
}
@ -327,20 +342,16 @@ namespace storm {
assert (!node->states.get(state));
if (!alreadyInitialized) {
node->statesAbove = storm::storage::BitVector(numberOfStates);
node->above = new std::set<Lattice::Node*>({});
}
node->statesAbove.set(state);
node->above->insert(getNode(state));
}
void Lattice::setStatesBelow(Lattice::Node *node, uint_fast64_t state, bool alreadyInitialized) {
assert (!node->states.get(state));
if (!alreadyInitialized) {
node->statesBelow = storm::storage::BitVector(numberOfStates);
node->below = new std::set<Lattice::Node*>({});
}
node->statesBelow.set(state);
node->below->insert(getNode(state));
}
void Lattice::setStatesAbove(Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized) {
@ -350,13 +361,10 @@ namespace storm {
node->statesAbove |= states;
} else {
node->statesAbove = storm::storage::BitVector(states);
node->above = new std::set<Lattice::Node*>({});
}
for (auto i = states.getNextSetIndex(0); i < states.size(); i = states.getNextSetIndex(i + 1)) {
if (node->states.get(i)) {
node->statesAbove.set(i, false);
} else {
node->above->insert(getNode(i));
}
}
}
@ -367,13 +375,10 @@ namespace storm {
node->statesBelow |= states;
} else {
node->statesBelow = storm::storage::BitVector(states);
node->below = new std::set<Lattice::Node*>({});
}
for (auto i = states.getNextSetIndex(0); i < states.size(); i = states.getNextSetIndex(i + 1)) {
if (node->states.get(i)) {
node->statesBelow.set(i, false);
} else {
node->below->insert(getNode(i));
}
}
}

10
src/storm-pars/analysis/Lattice.h

@ -20,8 +20,6 @@ namespace storm {
storm::storage::BitVector states;
storm::storage::BitVector statesAbove;
storm::storage::BitVector statesBelow;
std::set<Lattice::Node*>* above;
std::set<Lattice::Node*>* below;
};
/*!
@ -114,6 +112,14 @@ namespace storm {
*/
storm::storage::BitVector getAddedStates();
std::set<Lattice::Node*> getAbove(uint_fast64_t state);
std::set<Lattice::Node*> getBelow(uint_fast64_t state);
std::set<Lattice::Node*> getAbove(Lattice::Node* node);
std::set<Lattice::Node*> getBelow(Lattice::Node* node);
/*!
* Prints a string representation of the lattice to the output stream.
*

42
src/storm-pars/analysis/LatticeExtender.cpp

@ -34,7 +34,7 @@ namespace storm {
}
template <typename ValueType>
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
storm::utility::Stopwatch latticeWatch(true);
STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis");
@ -107,7 +107,7 @@ namespace storm {
}
// Create the Lattice
storm::analysis::Lattice *lattice = new storm::analysis::Lattice(topStates, bottomStates, numberOfStates);
Lattice *lattice = new Lattice(topStates, bottomStates, numberOfStates);
for (auto state = initialMiddleStates.getNextSetIndex(0); state != numberOfStates; state = initialMiddleStates.getNextSetIndex(state + 1)) {
lattice->add(state);
}
@ -119,7 +119,7 @@ namespace storm {
}
template <typename ValueType>
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
// TODO: split up
auto numberOfStates = this->model->getNumberOfStates();
// First handle assumption
@ -137,9 +137,9 @@ namespace storm {
auto val1 = std::stoul(var1.getName(), nullptr, 0);
auto val2 = std::stoul(var2.getName(), nullptr, 0);
auto comp = lattice->compare(val1, val2);
assert (comp == storm::analysis::Lattice::UNKNOWN || comp == storm::analysis::Lattice::SAME);
storm::analysis::Lattice::Node *n1 = lattice->getNode(val1);
storm::analysis::Lattice::Node *n2 = lattice->getNode(val2);
assert (comp == Lattice::UNKNOWN || comp == Lattice::SAME);
Lattice::Node *n1 = lattice->getNode(val1);
Lattice::Node *n2 = lattice->getNode(val2);
if (n1 != nullptr && n2 != nullptr) {
assert(false);
@ -157,12 +157,13 @@ namespace storm {
assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable());
storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable();
storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable();
if (lattice->compare(std::stoul(largest.getName(), nullptr, 0),
std::stoul(smallest.getName(), nullptr, 0)) !=
storm::analysis::Lattice::ABOVE) {
storm::analysis::Lattice::Node *n1 = lattice->getNode(
auto compareRes = lattice->compare(std::stoul(largest.getName(), nullptr, 0),
std::stoul(smallest.getName(), nullptr, 0));
assert(compareRes == Lattice::UNKNOWN);
if (compareRes != Lattice::ABOVE) {
Lattice::Node *n1 = lattice->getNode(
std::stoul(largest.getName(), nullptr, 0));
storm::analysis::Lattice::Node *n2 = lattice->getNode(
Lattice::Node *n2 = lattice->getNode(
std::stoul(smallest.getName(), nullptr, 0));
if (n1 != nullptr && n2 != nullptr) {
@ -209,24 +210,25 @@ namespace storm {
uint_fast64_t successor2 = successors.getNextSetIndex(successor1 + 1);
int compareResult = lattice->compare(successor1, successor2);
if (compareResult == storm::analysis::Lattice::ABOVE) {
if (compareResult == Lattice::ABOVE) {
// successor 1 is closer to top than successor 2
lattice->addBetween(stateNumber, lattice->getNode(successor1),
lattice->getNode(successor2));
} else if (compareResult == storm::analysis::Lattice::BELOW) {
} else if (compareResult == Lattice::BELOW) {
// successor 2 is closer to top than successor 1
lattice->addBetween(stateNumber, lattice->getNode(successor2),
lattice->getNode(successor1));
} else if (compareResult == storm::analysis::Lattice::SAME) {
} else if (compareResult == Lattice::SAME) {
// the successors are at the same level
lattice->addToNode(stateNumber, lattice->getNode(successor1));
} else {
assert(lattice->compare(successor1, successor2) == Lattice::UNKNOWN);
return std::make_tuple(lattice, successor1, successor2);
}
} else if (check && successors.getNumberOfSetBits() > 2) {
for (auto i = successors.getNextSetIndex(0); i < successors.size(); i = successors.getNextSetIndex(i+1)) {
for (auto j = successors.getNextSetIndex(i+1); j < successors.size(); j = successors.getNextSetIndex(j+1)) {
if (lattice->compare(i,j) == storm::analysis::Lattice::UNKNOWN) {
if (lattice->compare(i,j) == Lattice::UNKNOWN) {
return std::make_tuple(lattice, i, j);
}
}
@ -235,16 +237,18 @@ namespace storm {
auto highest = successors.getNextSetIndex(0);
auto lowest = highest;
for (auto i = successors.getNextSetIndex(highest+1); i < successors.size(); i = successors.getNextSetIndex(i+1)) {
if (lattice->compare(i, highest) == storm::analysis::Lattice::ABOVE) {
if (lattice->compare(i, highest) == Lattice::ABOVE) {
highest = i;
}
if (lattice->compare(lowest, i) == storm::analysis::Lattice::ABOVE) {
if (lattice->compare(lowest, i) == Lattice::ABOVE) {
lowest = i;
}
}
lattice->addBetween(stateNumber, lattice->getNode(highest), lattice->getNode(lowest));
}
// Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet
bool checkOneSuccLeft = seenStates[stateNumber] && successors.getNumberOfSetBits() <= 2;
bool helper = true;
for (auto succIndex = successors.getNextSetIndex(0); (check || checkOneSuccLeft) && succIndex != numberOfStates; succIndex = successors.getNextSetIndex(++succIndex)) {
@ -268,9 +272,9 @@ namespace storm {
assert (seenStates[succ1]);
auto nodeSucc = lattice->getNode(succ1);
auto compare = lattice->compare(stateNumber, succ1);
if (compare == storm::analysis::Lattice::ABOVE) {
if (compare == Lattice::ABOVE) {
lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber));
} else if (compare == storm::analysis::Lattice::BELOW) {
} else if (compare == Lattice::BELOW) {
lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom());
}
}

1
src/storm-pars/analysis/MonotonicityChecker.cpp

@ -196,6 +196,7 @@ namespace storm {
auto assumption2 = *itr;
if (!assumption1.second && !assumption2.second) {
// TODO: hier niet verder gaan als je iets gevonden hebt?
auto assumptionsCopy = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
auto latticeCopy = new storm::analysis::Lattice(lattice);
assumptions.push_back(assumption1.first);

Loading…
Cancel
Save