From 2f7f5eb212ef199bf2ddae8e2fd4ba4d4d6de851 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Sat, 24 Dec 2016 00:22:00 +0100 Subject: [PATCH] ksp: forward-declare model --- src/storm/utility/shortestPaths.cpp | 10 ++++----- src/storm/utility/shortestPaths.h | 35 +++++++++++++++++------------ 2 files changed, 26 insertions(+), 19 deletions(-) diff --git a/src/storm/utility/shortestPaths.cpp b/src/storm/utility/shortestPaths.cpp index 1bd11f8aa..9bf630953 100644 --- a/src/storm/utility/shortestPaths.cpp +++ b/src/storm/utility/shortestPaths.cpp @@ -2,11 +2,12 @@ #include #include +#include "storm/models/sparse/Model.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/storage/sparse/StateType.h" +#include "storm/utility/graph.h" #include "storm/utility/macros.h" #include "storm/utility/shortestPaths.h" -#include "storm/utility/graph.h" - -#include "storm/models/sparse/StandardRewardModel.h" // FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required! // Accessing zero should trigger a warning! @@ -177,7 +178,6 @@ namespace storm { } } else { // node only has one "virtual edge" (with prob as per targetProbMap) to meta-target - // FIXME: double check T alternateDistance = shortestPathDistances[currentNode] * targetProbMap[currentNode]; if (alternateDistance > shortestPathDistances[metaTarget]) { shortestPathDistances[metaTarget] = alternateDistance; @@ -252,7 +252,7 @@ namespace storm { } else { // edge must be "virtual edge" to meta-target assert(isMetaTargetPredecessor(tailNode)); - return targetProbMap.at(tailNode); // FIXME double check + return targetProbMap.at(tailNode); } } diff --git a/src/storm/utility/shortestPaths.h b/src/storm/utility/shortestPaths.h index e7cb38df6..359a30c5e 100644 --- a/src/storm/utility/shortestPaths.h +++ b/src/storm/utility/shortestPaths.h @@ -1,26 +1,33 @@ #ifndef STORM_UTIL_SHORTESTPATHS_H_ #define STORM_UTIL_SHORTESTPATHS_H_ +#include #include #include -#include -#include "storm/models/sparse/Model.h" -#include "storm/storage/sparse/StateType.h" + #include "constants.h" +#include "storm/storage/BitVector.h" + +namespace storm { + namespace storage { + template + class SparseMatrix; -// NOTE: You'll (eventually) find the usual API documentation below; -// for more information about the purpose, design decisions, -// etc., you may consult `shortestPath.md`. - Tom + namespace sparse { + typedef uint_fast64_t state_type; + } + } -// TODO: test whether using BitVector instead of vector is -// faster for storing predecessors etc. + namespace models { + namespace sparse { + template + class StandardRewardModel; -// Now using BitVectors instead of vector in the API because -// BitVectors are used throughout Storm to represent a (unordered) list -// of states. -// (Even though both initialStates and targets are probably very sparse.) + template + class Model; + } + } -namespace storm { namespace utility { namespace ksp { using state_t = storage::sparse::state_type; @@ -60,7 +67,7 @@ namespace storm { public: using Matrix = storage::SparseMatrix; using StateProbMap = std::unordered_map; - using Model = models::sparse::Model; + using Model = models::sparse::Model>; /*! * Performs precomputations (including meta-target insertion and Dijkstra).