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

Clean up

tempestpy_adaptions
Jip Spel 6 years ago
parent
2c4d5c0d3f
commit
1364ec8729
3 changed files with 60 additions and 90 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 100
      src/storm-pars-cli/storm-pars.cpp
  2. 46
      src/storm-pars/analysis/Lattice.cpp
  3. 4
      src/storm-pars/analysis/Lattice.h

100
src/storm-pars-cli/storm-pars.cpp
View File

@ -511,12 +511,11 @@ namespace storm {
} }
stateVector.push_back(state); stateVector.push_back(state);
} }
// Start creating the Lattice // Start creating the Lattice
storm::analysis::Lattice *lattice = new storm::analysis::Lattice(topStates, bottomStates, numberOfStates); storm::analysis::Lattice *lattice = new storm::analysis::Lattice(topStates, bottomStates, numberOfStates);
storm::storage::BitVector oldStates(numberOfStates); storm::storage::BitVector oldStates(numberOfStates);
// Create a copy of the states already present in the lattice. // Create a copy of the states already present in the lattice.
storm::storage::BitVector seenStates = topStates|=bottomStates;
storm::storage::BitVector seenStates = topStates|= bottomStates;
while (oldStates != seenStates) { while (oldStates != seenStates) {
// As long as new states are added to the lattice, continue. // As long as new states are added to the lattice, continue.
@ -530,65 +529,60 @@ namespace storm {
&& seenStates[currentState->successor1] && seenStates[currentState->successor1]
&& seenStates[currentState->successor2]) { && seenStates[currentState->successor2]) {
// Check if the current state number has not been added, but its successors have been added.
if (currentState->successor1 == currentState->successor2) {
// If there is only one successor, the state should be added to the same Node as its successor
lattice->addToNode(currentState->stateNumber, lattice->getNode(currentState->successor1));
// Add stateNumber to the set with seen states.
seenStates.set(currentState->stateNumber);
} else {
// Otherwise, check how the two states compare, and add if the comparison is possible.
uint_fast64_t successor1 = currentState->successor1;
uint_fast64_t successor2 = currentState->successor2;
int compareResult = lattice->compare(successor1, successor2);
if (compareResult == 1 || compareResult == 2) {
if (compareResult == 2) {
// swap
auto temp = successor1;
successor1 = successor2;
successor2 = temp;
}
// Additional check, if states have the same probability of reaching a given next state,
// then they should be at the same node
// TODO: can this be removed, e.g. adding a step to preprocessing, making this superfluous
storm::analysis::Lattice::Node *above = lattice->getNode(successor1);
storm::analysis::Lattice::Node *below = lattice->getNode(successor2);
std::vector<storm::analysis::Lattice::Node *> states1 = above->below;
std::vector<storm::analysis::Lattice::Node *> states2 = below->above;
for (auto itr1 = states1.begin(); itr1 < states1.end(); ++itr1) {
for (auto itr2 = states2.begin(); itr2 < states2.end(); ++itr2) {
if ((*itr1)->states == (*itr2)->states) {
ValueType prob1 = getProbability(currentState->stateNumber, successor1, matrix);
ValueType prob2 = getProbability(currentState->stateNumber, successor2, matrix);
if (prob1 != ValueType(1)
&& prob2 != ValueType(1)
&& getProbability((*itr1)->states, above->states, matrix) == prob1
&& getProbability((*itr1)->states, below->states, matrix) == prob2) {
lattice->addToNode(currentState->stateNumber, (*itr1));
seenStates.set(currentState->stateNumber);
}
// Otherwise, check how the two states compare, and add if the comparison is possible.
uint_fast64_t successor1 = currentState->successor1;
uint_fast64_t successor2 = currentState->successor2;
int compareResult = lattice->compare(successor1, successor2);
if (compareResult == 1 || compareResult == 2) {
// getNode will not return nullptr, as compare already checked this
if (compareResult == 2) {
// swap
auto temp = successor1;
successor1 = successor2;
successor2 = temp;
}
// Additional check, if states have the same probability of reaching a given next state,
// then they should be at the same node
// TODO: can this be removed, e.g. adding a step to preprocessing, making this superfluous
// TODO: 1 prob. and same probs to same states should be removed from matrix
storm::analysis::Lattice::Node *above = lattice->getNode(successor1);
storm::analysis::Lattice::Node *below = lattice->getNode(successor2);
std::vector<storm::analysis::Lattice::Node *> states1 = above->below;
std::vector<storm::analysis::Lattice::Node *> states2 = below->above;
for (auto itr1 = states1.begin(); itr1 < states1.end(); ++itr1) {
for (auto itr2 = states2.begin(); itr2 < states2.end(); ++itr2) {
if ((*itr1)->states == (*itr2)->states) {
ValueType prob1 = getProbability(currentState->stateNumber, successor1, matrix);
ValueType prob2 = getProbability(currentState->stateNumber, successor2, matrix);
if (prob1 != ValueType(1)
&& prob2 != ValueType(1)
&& getProbability((*itr1)->states, above->states, matrix) == prob1
&& getProbability((*itr1)->states, below->states, matrix) == prob2) {
lattice->addToNode(currentState->stateNumber, (*itr1));
seenStates.set(currentState->stateNumber);
} }
} }
} }
}
if (!seenStates.get(currentState->stateNumber)) {
// successor 1 is closer to top than successor 2
lattice->addBetween(currentState->stateNumber, lattice->getNode(successor1),
lattice->getNode(successor2));
// Add stateNumber to the set with seen states.
seenStates.set(currentState->stateNumber);
}
} else if (compareResult == 0) {
// the successors are at the same level
lattice->addToNode(currentState->stateNumber, lattice->getNode(successor1));
if (!seenStates.get(currentState->stateNumber)) {
// successor 1 is closer to top than successor 2
lattice->addBetween(currentState->stateNumber, lattice->getNode(successor1),
lattice->getNode(successor2));
// Add stateNumber to the set with seen states. // Add stateNumber to the set with seen states.
seenStates.set(currentState->stateNumber); seenStates.set(currentState->stateNumber);
} else {
// TODO: what to do?
STORM_LOG_DEBUG("Failed to add" << currentState->stateNumber << "\n");
} }
} else if (compareResult == 0) {
// the successors are at the same level
lattice->addToNode(currentState->stateNumber, lattice->getNode(successor1));
// Add stateNumber to the set with seen states.
seenStates.set(currentState->stateNumber);
} else {
// TODO: what to do?
STORM_LOG_DEBUG("Failed to add" << currentState->stateNumber << "\n");
} }
} }
} }
} }

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

@ -39,23 +39,24 @@ namespace storm {
Node *node1 = getNode(state1); Node *node1 = getNode(state1);
Node *node2 = getNode(state2); Node *node2 = getNode(state2);
if (node1 == node2) {
return 0;
}
if (node1 != nullptr && node2 != nullptr) {
if (node1 == node2) {
return 0;
}
if (above(node1, node2)) {
return 1;
}
if (above(node1, node2)) {
return 1;
}
if (below(node1, node2)) {
return 2;
if (above(node2, node1)) {
return 2;
}
} }
return -1; return -1;
} }
Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) { Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) {
// TODO: might return nullptr, what to do with it?
Node *node; Node *node;
for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
storm::storage::BitVector states = (*itr)->states; storm::storage::BitVector states = (*itr)->states;
@ -122,37 +123,14 @@ namespace storm {
} }
bool Lattice::above(Node *node1, Node *node2) { bool Lattice::above(Node *node1, Node *node2) {
if (node1->below.empty()) {
return false;
}
if (std::find(node1->below.begin(), node1->below.end(), node2) != node1->below.end()) {
return true;
}
bool result = !node1->below.empty() && std::find(node1->below.begin(), node1->below.end(), node2) != node1->below.end();
bool result = false;
for (auto itr = node1->below.begin(); node1->below.end() != itr; ++itr) {
for (auto itr = node1->below.begin(); !result && node1->below.end() != itr; ++itr) {
result |= above(*itr, node2); result |= above(*itr, node2);
} }
return result; return result;
} }
bool Lattice::below(Node *node1, Node *node2) {
if (node1->above.empty()) {
return false;
}
if (std::find(node1->above.begin(), node1->above.end(), node2) != node1->above.end()) {
return true;
}
bool result = false;
for (auto itr = node1->above.begin(); node1->above.end() != itr; ++itr) {
result |= below(*itr, node2);
}
return result;
}
void Lattice::remove(std::vector<Node *> *nodes, Node *node) { void Lattice::remove(std::vector<Node *> *nodes, Node *node) {
auto index = std::find(nodes->begin(), nodes->end(), node); auto index = std::find(nodes->begin(), nodes->end(), node);
if (index != nodes->end()) { if (index != nodes->end()) {

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

@ -63,7 +63,7 @@ namespace storm {
* *
* @param state The number of the state. * @param state The number of the state.
* *
* @return The pointer to the node of the state.
* @return The pointer to the node of the state, nullptr if the node does not exist
*/ */
Node *getNode(uint_fast64_t state); Node *getNode(uint_fast64_t state);
@ -83,8 +83,6 @@ namespace storm {
bool above(Node *, Node *); bool above(Node *, Node *);
bool below(Node *, Node *);
void remove(std::vector<Node *> *nodes, Node *node); void remove(std::vector<Node *> *nodes, Node *node);
void setStates(std::vector<uint_fast64_t> states, Node *node); void setStates(std::vector<uint_fast64_t> states, Node *node);

Write Preview
Loading…
Cancel
Save