Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
shortestPaths.h
Go to the documentation of this file.
1#ifndef STORM_UTIL_SHORTESTPATHS_H_
2#define STORM_UTIL_SHORTESTPATHS_H_
3
4#include <boost/optional/optional.hpp>
5#include <unordered_set>
6#include <vector>
7
8#include "constants.h"
10
11namespace storm {
12namespace storage {
13template<typename ValueType>
14class SparseMatrix;
15
16namespace sparse {
17typedef uint_fast64_t state_type;
18}
19} // namespace storage
20
21namespace models {
22namespace sparse {
23template<typename ValueType>
24class StandardRewardModel;
25
26template<class CValueType, class CRewardModelType>
27class Model;
28} // namespace sparse
29} // namespace models
30
31namespace utility {
32namespace ksp {
34using OrderedStateList = std::vector<state_t>;
36
37// -- helper structs/classes -----------------------------------------------------------------------------
38
39template<typename T>
40struct Path {
41 boost::optional<state_t> predecessorNode;
42 unsigned long predecessorK;
44
45 // arbitrary order for std::set
46 bool operator<(const Path<T>& rhs) const {
49 }
50 return predecessorK < rhs.predecessorK;
51 }
52
53 bool operator==(const Path<T>& rhs) const {
54 return (predecessorNode == rhs.predecessorNode) && (predecessorK == rhs.predecessorK);
55 }
56};
57
58template<typename T>
59std::ostream& operator<<(std::ostream& out, Path<T> const& p);
60
61// when using the raw matrix/vector invocation, this enum parameter
62// forces the caller to declare whether the matrix has the evil I-P
63// format, which requires back-conversion of the entries
65
66// -------------------------------------------------------------------------------------------------------
67
68template<typename T>
70 public:
72 using StateProbMap = std::unordered_map<state_t, T>;
74
80 ShortestPathsGenerator(Model const& model, BitVector const& targetBV);
81
82 // allow alternative ways of specifying the target,
83 // all of which will be converted to BitVector and delegated to constructor above
84 ShortestPathsGenerator(Model const& model, state_t singleTarget);
85 ShortestPathsGenerator(Model const& model, std::vector<state_t> const& targetList);
86 ShortestPathsGenerator(Model const& model, std::string const& targetLabel = "target");
87
88 // a further alternative: use transition matrix of maybe-states
89 // combined with target vector (e.g., the instantiated matrix/vector from SamplingModel);
90 // in this case separately specifying a target makes no sense
91 ShortestPathsGenerator(Matrix const& transitionMatrix, std::vector<T> const& targetProbVector, BitVector const& initialStates, MatrixFormat matrixFormat);
92 ShortestPathsGenerator(Matrix const& maybeTransitionMatrix, StateProbMap const& targetProbMap, BitVector const& initialStates, MatrixFormat matrixFormat);
93
95
101 T getDistance(unsigned long k);
102
109 storage::BitVector getStates(unsigned long k);
110
116 OrderedStateList getPathAsList(unsigned long k);
117
118 private:
119 Matrix const& transitionMatrix;
120 state_t numStates; // includes meta-target, i.e. states in model + 1
121 state_t metaTarget;
122 BitVector initialStates;
123 StateProbMap targetProbMap;
124
125 MatrixFormat matrixFormat;
126
127 std::vector<OrderedStateList> graphPredecessors;
128 std::vector<boost::optional<state_t>> shortestPathPredecessors;
129 std::vector<OrderedStateList> shortestPathSuccessors;
130 std::vector<T> shortestPathDistances;
131
132 std::vector<std::vector<Path<T>>> kShortestPaths;
133 std::vector<std::set<Path<T>>> candidatePaths;
134
141 void computePredecessors();
142
148 void performDijkstra();
149
155 void computeSPSuccessors();
156
162 void initializeShortestPaths();
163
167 void computeNextPath(state_t node, unsigned long k);
168
173 void computeKSP(unsigned long k);
174
178 void printKShortestPath(state_t targetNode, unsigned long k, bool head = true) const;
179
183 T getEdgeDistance(state_t tailNode, state_t headNode) const;
184
185 // --- tiny helper fcts ---
186
187 inline bool isInitialState(state_t node) const {
188 return std::find(initialStates.begin(), initialStates.end(), node) != initialStates.end();
189 }
190
191 inline bool isMetaTargetPredecessor(state_t node) const {
192 return targetProbMap.count(node) == 1;
193 }
194
195 // I dislike this. But it is necessary if we want to handle those ugly I-P matrices
196 inline T convertDistance(state_t tailNode, state_t headNode, T distance) const {
197 if (matrixFormat == MatrixFormat::straight) {
198 return distance;
199 } else {
200 if (tailNode == headNode) {
201 // diagonal: 1-p = dist
202 return one<T>() - distance;
203 } else {
204 // non-diag: -p = dist
205 return zero<T>() - distance;
206 }
207 }
208 }
209
213 inline StateProbMap allProbOneMap(BitVector bitVector) const {
214 StateProbMap stateProbMap;
215 for (state_t node : bitVector) {
216 stateProbMap.emplace(node, one<T>()); // FIXME check rvalue warning (here and below)
217 }
218 return stateProbMap;
219 }
220
225 inline std::unordered_map<state_t, T> vectorToMap(std::vector<T> probVector) const {
226 // assert(probVector.size() == numStates); // numStates may not yet be initialized! // still true?
227
228 std::unordered_map<state_t, T> stateProbMap;
229
230 for (state_t i = 0; i < probVector.size(); i++) {
231 T probEntry = probVector[i];
232
233 // only non-zero entries (i.e. true transitions) are added to the map
234 if (probEntry != 0) {
235 assert(0 < probEntry);
236 assert(probEntry <= 1);
237 stateProbMap.emplace(i, probEntry);
238 }
239 }
240
241 return stateProbMap;
242 }
243
244 // -----------------------
245};
246} // namespace ksp
247} // namespace utility
248} // namespace storm
249
250#endif // STORM_UTIL_SHORTESTPATHS_H_
Base class for all sparse models.
Definition Model.h:33
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
const_iterator end() const
Returns an iterator pointing at the element past the back of the bit vector.
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
A class that holds a possibly non-square matrix in the compressed row storage format.
std::unordered_map< state_t, T > StateProbMap
storage::BitVector getStates(unsigned long k)
Returns the states that occur in the KSP.
T getDistance(unsigned long k)
Returns distance (i.e., probability) of the KSP.
OrderedStateList getPathAsList(unsigned long k)
Returns the states of the KSP as back-to-front traversal.
ShortestPathsGenerator(Matrix const &maybeTransitionMatrix, StateProbMap const &targetProbMap, BitVector const &initialStates, MatrixFormat matrixFormat)
std::vector< state_t > OrderedStateList
storage::BitVector BitVector
std::ostream & operator<<(std::ostream &out, Path< T > const &p)
storage::sparse::state_type state_t
LabParser.cpp.
Definition cli.cpp:18
bool operator==(const Path< T > &rhs) const
bool operator<(const Path< T > &rhs) const
boost::optional< state_t > predecessorNode