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

Update implementation

tempestpy_adaptions
Jip Spel 6 years ago
parent
46aa007f33
commit
ed0768cf60
4 changed files with 106 additions and 82 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. 171
      src/storm-pars/analysis/Lattice.cpp
  2. 4
      src/storm-pars/analysis/Lattice.h
  3. 4
      src/storm-pars/analysis/LatticeExtender.cpp
  4. 9
      src/storm-pars/analysis/MonotonicityChecker.cpp

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

@ -87,11 +87,11 @@ namespace storm {
Node *oldNode = (*itr);
if (oldNode != nullptr && oldNode != lattice->getTop() && oldNode != lattice->getBottom()) {
Node *newNode = getNode(*(oldNode->states.begin()));
newNode->statesAbove = storm::storage::BitVector(oldNode->statesAbove);
newNode->statesAbove = storm::storage::BitVector((oldNode->statesAbove));
// setStatesAbove(newNode, oldNode->statesAbove, false);
// setStatesBelow(newNode, oldNode->statesBelow, false);
} else if (oldNode != nullptr && oldNode == lattice->getBottom()) {
bottom->statesAbove = storm::storage::BitVector(oldNode->statesAbove);
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()) {
@ -110,11 +110,13 @@ namespace storm {
// newNode->states = storm::storage::BitVector(numberOfStates);
newNode->states.insert(state);
newNode->statesAbove = above->statesAbove;
newNode->statesAbove = storm::storage::BitVector((above->statesAbove));
for (auto const& state : above->states) {
newNode->statesAbove.set(state);
}
below->statesAbove.set(state);
addedStates->set(state);
// comparisons[state] = comparisons[above->states.getNextSetIndex(0)];
// setStatesAbove(newNode, above->statesAbove | above->states, false);
// setStatesBelow(newNode, below->statesBelow | below->states, false);
@ -129,7 +131,6 @@ namespace storm {
// setStatesBelow(getNode(i), state, true);
// }
addedStates->set(state);
}
@ -163,7 +164,7 @@ namespace storm {
for (auto const& state : above->states) {
below->statesAbove.set(state);
}
below->statesAbove |= above->statesAbove;
below->statesAbove|=((above->statesAbove));
// TODO: comparisons
// for (auto i = below->statesBelow.getNextSetIndex(0); i < below->statesBelow.size(); i = below->statesBelow.getNextSetIndex(i + 1)) {
@ -206,6 +207,20 @@ namespace storm {
// comparisons[state2][state1] = ABOVE;
return BELOW;
}
// tweak for cyclic pmcs
if (doneBuilding) {
doneBuilding = false;
if (above(node1, node2)) {
assert(!above(node2, node1));
doneBuilding = true;
return ABOVE;
}
if (above(node2, node1)) {
doneBuilding = true;
return BELOW;
}
}
}
return UNKNOWN;
}
@ -240,29 +255,48 @@ namespace storm {
std::vector<uint_fast64_t> Lattice::sortStates(storm::storage::BitVector* states) {
auto numberOfSetBits = states->getNumberOfSetBits();
auto result = std::vector<uint_fast64_t>(numberOfSetBits, -1);
auto stateSize = states->size();
auto result = std::vector<uint_fast64_t>(numberOfSetBits, stateSize);
for (auto state : *states) {
if (result[0] == -1) {
if (result[0] == stateSize) {
result[0] = state;
} else {
for (auto i = 0; i < numberOfSetBits && result[i] != -1; i++) {
auto compareRes = compare(state, result[i]);
if (compareRes == Lattice::ABOVE) {
for (auto j = i; j < numberOfSetBits -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 < numberOfSetBits -1 && result[j+1] != -1; j++) {
auto temp = result[j];
result[j] = state;
result[j+1] = temp;
auto i = 0;
bool added = false;
while (i < numberOfSetBits && !added) {
if (result[i] == stateSize) {
result[i] = state;
added = true;
} else {
auto compareRes = compare(state, result[i]);
if (compareRes == Lattice::ABOVE) {
auto temp = result[i];
result[i] = state;
for (auto j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) {
auto temp2 = result[j];
result[j] = temp;
temp = temp2;
}
added = true;
} else if (compareRes == Lattice::UNKNOWN) {
break;
} else if (compareRes == Lattice::SAME) {
++i;
auto temp = result[i];
result[i] = state;
for (auto j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) {
auto temp2 = result[j];
result[j] = temp;
temp = temp2;
}
added = true;
}
}
++i;
}
// if (i < numberOfSetBits && result[i] == stateSize) {
// result[i] = state;
// }
}
}
@ -294,42 +328,26 @@ namespace storm {
// }
void Lattice::toString(std::ostream &out) {
// assert (false);
// std::vector<Node*> printedNodes = std::vector<Node*>({});
// for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
//
// if ((*itr) != nullptr && std::find(printedNodes.begin(), printedNodes.end(), (*itr)) == printedNodes.end()) {
// Node *node = *itr;
// printedNodes.push_back(*itr);
// out << "Node: {";
// uint_fast64_t index = node->states.getNextSetIndex(0);
// while (index < node->states.size()) {
// out << index;
// index = node->states.getNextSetIndex(index + 1);
// if (index < node->states.size()) {
// out << ", ";
// }
// }
// out << "}" << "\n";
// out << " Address: " << node << "\n";
// out << " Above: {";
//
// auto statesAbove = node->statesAbove;
// for (auto above : statesAbove) {
// Node* nodeAbove = getNode(above);
// index = nodeAbove->states.getNextSetIndex(0);
// out << "{";
// while (index < nodeAbove->states.size()) {
// out << index;
// index = nodeAbove->states.getNextSetIndex(index + 1);
// if (index < nodeAbove->states.size()) {
// out << ", ";
// }
// }
//
// out << "}";
// }
// out << "}" << "\n";
std::vector<Node*> printedNodes = std::vector<Node*>({});
for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
if ((*itr) != nullptr && std::find(printedNodes.begin(), printedNodes.end(), (*itr)) == printedNodes.end()) {
Node *node = *itr;
printedNodes.push_back(*itr);
out << "Node: {";
for (auto const & state:node->states) {
out << state << "; ";
}
out << "}" << "\n";
out << " Address: " << node << "\n";
out << " Above: {";
auto statesAbove = node->statesAbove;
for (auto const & state:(node->statesAbove)) {
out << state << "; ";
}
out << "}" << "\n";
// out << " Below: {";
@ -349,8 +367,8 @@ namespace storm {
// out << "}";
// }
// out << "}" << "\n";
// }
// }
}
}
}
void Lattice::toDotFile(std::ostream &out) {
@ -399,17 +417,17 @@ namespace storm {
// oftewel is er een state in node2.above die met een state in node1 matched
bool found = false;
for (auto const& state : node1->states) {
found = node2->statesAbove[state];
found = ((node2->statesAbove))[state];
if (found) {
break;
}
}
if (!found && !doneBuilding) {
storm::storage::BitVector statesSeen(node2->statesAbove);
for (auto const &i: node2->statesAbove) {
storm::storage::BitVector statesSeen((node2->statesAbove));
for (auto const &i: (node2->statesAbove)) {
auto nodeI = getNode(i);
if ((nodeI->statesAbove & statesSeen) != nodeI->statesAbove) {
if (((nodeI->statesAbove) & statesSeen) != (nodeI->statesAbove)) {
found = above(node1, nodeI, node2, &statesSeen);
}
if (found) {
@ -428,7 +446,7 @@ namespace storm {
// bool found = (node2->statesAbove & node1->states).getNumberOfSetBits() != 0;
bool found = false;
for (auto const& state : node1->states) {
found = node2->statesAbove[state];
found = ((node2->statesAbove))[state];
if (found) {
break;
}
@ -436,19 +454,20 @@ namespace storm {
// bool found = !(node2->statesAbove & node1->states).empty();
if (!found) {
// TODO: kan dit niet anders?
nodePrev->statesAbove |= node2->statesAbove;
auto complement = (statesSeen->operator~());
nodePrev->statesAbove|=((node2->statesAbove));
// auto complement = storm::storage::BitVector(statesSeen->operator~());
storm::storage::BitVector states = storm::storage::BitVector(
(node2->statesAbove & complement));
statesSeen->operator|=(node2->statesAbove);
// storm::storage::BitVector states = storm::storage::BitVector(node2->statesAbove & complement);
statesSeen->operator|=(((node2->statesAbove)));
for (auto const &i: states) {
for (auto const &i: node2->statesAbove) {
// assert (!statesSeen[i]);
auto nodeI = getNode(i);
if (!(nodeI->statesAbove & complement).empty()) {
found = above(node1, nodeI, node2, statesSeen);
}
if (!(*statesSeen)[i]) {
auto nodeI = getNode(i);
if (((nodeI->statesAbove) & *statesSeen) != (nodeI->statesAbove)) {
found = above(node1, nodeI, node2, statesSeen);
}
}
if (found) {
break;
}
@ -509,7 +528,7 @@ namespace storm {
// assert (false);
// Merges node2 into node 1
// everything above n2 also above n1
node1->statesAbove |= node2->statesAbove;
node1->statesAbove|=((node2->statesAbove));
// everything below node 2 also below node 1
// node1->statesBelow |= node2->statesBelow;

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

@ -123,6 +123,9 @@ namespace storm {
bool getDoneBuilding();
int compare(Node* node1, Node* node2);
std::vector<uint_fast64_t> sortStates(storm::storage::BitVector* states);
// /*!
@ -204,7 +207,6 @@ namespace storm {
bool above(Node * node1, Node * node2, storm::analysis::Lattice::Node *nodePrev, storm::storage::BitVector *statesSeen);
int compare(Node* node1, Node* node2);
std::unordered_map<uint_fast64_t, std::unordered_map<uint_fast64_t, uint_fast64_t>> comparisons;

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

@ -367,7 +367,8 @@ namespace storm {
}
addedStates = lattice->getAddedStates();
for (auto stateNumber : *addedStates) {
auto notAddedStates = addedStates->operator~();
for (auto stateNumber : notAddedStates) {
// Iterate over all not yet added states
storm::storage::BitVector* successors = stateMap[stateNumber];
@ -392,6 +393,7 @@ namespace storm {
}
}
assert (lattice->getAddedStates()->getNumberOfSetBits() == numberOfStates);
lattice->setDoneBuilding(true);
return std::make_tuple(lattice, numberOfStates, numberOfStates);
}
template class LatticeExtender<storm::RationalFunction>;

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

@ -404,7 +404,6 @@ namespace storm {
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);
lattice->setDoneBuilding(true);
std::map<carl::Variable, std::pair<bool, bool>> varsMonotone;
for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) {
@ -430,10 +429,12 @@ namespace storm {
auto sortedStates = lattice->sortStates(states);
assert(sortedStates[sortedStates.size() - 1] != matrix.getColumnCount());
assert (sortedStates.size() >=2);
assert (sortedStates.size() == states->getNumberOfSetBits());
if (sortedStates[sortedStates.size() - 1] == -1) {
if (sortedStates[sortedStates.size() - 1] == matrix.getColumnCount()) {
// auto val = first.getValue();
// auto vars = val.gatherVariables();
for (auto itr = vars.begin(); itr != vars.end(); ++itr) {
@ -498,7 +499,7 @@ namespace storm {
}
}
} else {
bool change = false;
for (auto var : vars) {
// if (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end() &&
// (!resultCheckOnSamples[*itr].first && !resultCheckOnSamples[*itr].second)) {
@ -512,7 +513,7 @@ namespace storm {
varsMonotone[var].second = true;
}
std::pair<bool, bool> *value = &varsMonotone.find(var)->second;
bool change = false;
for (auto const &i : sortedStates) {
// auto res = checkDerivative(transitions[i].derivative(var));
auto res = checkDerivative(getDerivative(transitions[i], var));

Write Preview
Loading…
Cancel
Save