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

comments and fixes (?) to graph.cpp's Dijkstra 

This implementation seemed pretty wrong in multiple ways;
I attempted to fix it (a long time ago) (see diff, you'll see what I'm
talking about), then gave up.
Luckily (?) the code is unused, just sitting there, sad and broken.
tempestpy_adaptions
Tom Janson 8 years ago
parent
07fc8e32ec
commit
b71ef02692
3 changed files with 38 additions and 15 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. 49
      src/storm/utility/graph.cpp
  2. 3
      src/storm/utility/graph.h
  3. 1
      src/test/utility/GraphTest.cpp

49
src/storm/utility/graph.cpp
View File

@ -992,7 +992,8 @@ namespace storm {
}
// There seems to be a lot of stuff wrong here. FIXME: Check whether it works now. -Tom
template <typename T>
std::pair<std::vector<T>, std::vector<uint_fast64_t>> performDijkstra(storm::models::sparse::Model<T> const& model,
storm::storage::SparseMatrix<T> const& transitions,
@ -1016,26 +1017,43 @@ namespace storm {
// As long as there is one reachable state, we need to consider it.
while (!probabilityStateSet.empty()) {
// Get the state with the least distance from the set and remove it.
std::pair<T, uint_fast64_t> probabilityStatePair = probabilityStateSet.erase(probabilityStateSet.begin());
// FIXME? is this correct? this used to take the second element!!
std::pair<T, uint_fast64_t> probabilityStatePair = *(probabilityStateSet.begin());
probabilityStateSet.erase(probabilityStateSet.begin());
uint_fast64_t currentNode = probabilityStatePair.second;
// Now check the new distances for all successors of the current state.
typename storm::storage::SparseMatrix<T>::Rows row = transitions.getRow(probabilityStatePair.second);
typename storm::storage::SparseMatrix<T>::const_rows row = transitions.getRowGroup(currentNode);
for (auto const& transition : row) {
uint_fast64_t targetNode = transition.getColumn();
// Only follow the transition if it lies within the filtered states.
if (filterStates != nullptr && filterStates->get(transition.first)) {
// -- shouldn't "no filter" (nullptr) mean that all nodes are checked? - Tom FIXME
if (filterStates == nullptr || filterStates->get(targetNode)) {
// Calculate the distance we achieve when we take the path to the successor via the current state.
T newDistance = probabilityStatePair.first;
// FIXME: this should be multiplied with the distance to the current node, right?
//T newDistance = probabilityStatePair.first;
T edgeProbability = probabilityStatePair.first;
T newDistance = probabilities[currentNode] * edgeProbability;
// DEBUG
if (newDistance != 1) {
std::cout << "yay" << std::endl;
}
// We found a cheaper way to get to the target state of the transition.
if (newDistance > probabilities[transition.first]) {
if (newDistance > probabilities[targetNode]) {
// Remove the old distance.
if (probabilities[transition.first] != noPredecessorValue) {
probabilityStateSet.erase(std::make_pair(probabilities[transition.first], transition.first));
if (probabilities[targetNode] != noPredecessorValue) {
probabilityStateSet.erase(std::make_pair(probabilities[targetNode], targetNode));
}
// Set and add the new distance.
probabilities[transition.first] = newDistance;
predecessors[transition.first] = probabilityStatePair.second;
probabilityStateSet.insert(std::make_pair(newDistance, transition.first));
probabilities[targetNode] = newDistance;
predecessors[targetNode] = currentNode;
probabilityStateSet.insert(std::make_pair(newDistance, targetNode));
}
}
}
@ -1179,8 +1197,11 @@ namespace storm {
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<float> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<float> const& matrix) ;
template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<float> const& matrix);
template std::pair<std::vector<double>, std::vector<uint_fast64_t>> performDijkstra(storm::models::sparse::Model<double> const& model, storm::storage::SparseMatrix<double> const& transitions, storm::storage::BitVector const& startingStates, storm::storage::BitVector const* filterStates);
// Instantiations for storm::RationalNumber.
#ifdef STORM_HAVE_CARL
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);

3
src/storm/utility/graph.h
View File

@ -544,13 +544,14 @@ namespace storm {
* @param transitions The transitions wrt to which to compute the most probable paths.
* @param startingStates The starting states of the Dijkstra search.
* @param filterStates A set of states that must not be left on any path.
* @return A pair consisting of a vector of distances and a vector of shortest path predecessors
*/
template <typename T>
std::pair<std::vector<T>, std::vector<uint_fast64_t>> performDijkstra(storm::models::sparse::Model<T> const& model,
storm::storage::SparseMatrix<T> const& transitions,
storm::storage::BitVector const& startingStates,
storm::storage::BitVector const* filterStates = nullptr);
} // namespace graph
} // namespace utility
} // namespace storm

1
src/test/utility/GraphTest.cpp
View File

@ -12,6 +12,7 @@
#include "storm/builder/DdPrismModelBuilder.h"
#include "storm/builder/ExplicitModelBuilder.h"
#include "storm/utility/graph.h"
#include "storm/utility/shortestPaths.cpp"
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/dd/DdManager.h"

Write Preview
Loading…
Cancel
Save