Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
shortestPaths.cpp
Go to the documentation of this file.
1#include <ostream>
2#include <queue>
3#include <set>
4#include <string>
5
11#include "storm/utility/graph.h"
14
15// FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required!
16// (Also, did I document this? I think so, somewhere. I went with k>=1 because
17// that's what the KSP paper used, but in retrospect k>=0 seems more intuitive ...)
18
19namespace storm {
20namespace utility {
21namespace ksp {
22template<typename T>
23ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> const& transitionMatrix, std::unordered_map<state_t, T> const& targetProbMap,
24 BitVector const& initialStates, MatrixFormat matrixFormat)
25 : transitionMatrix(transitionMatrix),
26 numStates(transitionMatrix.getColumnCount() + 1), // one more for meta-target
27 metaTarget(transitionMatrix.getColumnCount()), // first unused state index
28 initialStates(initialStates),
29 targetProbMap(targetProbMap),
30 matrixFormat(matrixFormat) {
31 computePredecessors();
32
33 // gives us SP-predecessors, SP-distances
34 performDijkstra();
35
36 computeSPSuccessors();
37
38 // constructs the recursive shortest path representations
39 initializeShortestPaths();
40
41 candidatePaths.resize(numStates);
42}
43
44template<typename T>
45ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> const& transitionMatrix, std::vector<T> const& targetProbVector,
46 BitVector const& initialStates, MatrixFormat matrixFormat)
47 : ShortestPathsGenerator<T>(transitionMatrix, vectorToMap(targetProbVector), initialStates, matrixFormat) {}
48
49// extracts the relevant info from the model and delegates to ctor above
50template<typename T>
52 : ShortestPathsGenerator<T>(model.getTransitionMatrix(), allProbOneMap(targetBV), model.getInitialStates(), MatrixFormat::straight) {}
53
54// several alternative ways to specify the targets are provided,
55// each converts the targets and delegates to the ctor above
56// I admit it's kind of ugly, but actually pretty convenient (and I've wanted to try C++11 delegation)
57template<typename T>
59 : ShortestPathsGenerator<T>(model, std::vector<state_t>{singleTarget}) {}
60
61template<typename T>
62ShortestPathsGenerator<T>::ShortestPathsGenerator(Model const& model, std::vector<state_t> const& targetList)
63 : ShortestPathsGenerator<T>(model, BitVector(model.getNumberOfStates(), targetList)) {}
64
65template<typename T>
66ShortestPathsGenerator<T>::ShortestPathsGenerator(Model const& model, std::string const& targetLabel)
67 : ShortestPathsGenerator<T>(model, model.getStates(targetLabel)) {}
68
69template<typename T>
71 computeKSP(k);
72 return kShortestPaths[metaTarget][k - 1].distance;
73}
74
75template<typename T>
77 computeKSP(k);
78 BitVector stateSet(numStates - 1, false); // no meta-target
79
80 Path<T> currentPath = kShortestPaths[metaTarget][k - 1];
81 boost::optional<state_t> maybePredecessor = currentPath.predecessorNode;
82 // this omits the first node, which is actually convenient since that's the meta-target
83
84 while (maybePredecessor) {
85 state_t predecessor = maybePredecessor.get();
86 stateSet.set(predecessor, true);
87
88 currentPath = kShortestPaths[predecessor][currentPath.predecessorK - 1]; // god damn you, index
89 maybePredecessor = currentPath.predecessorNode;
90 }
91
92 return stateSet;
93}
94
95template<typename T>
96std::vector<state_t> ShortestPathsGenerator<T>::getPathAsList(unsigned long k) {
97 computeKSP(k);
98
99 std::vector<state_t> backToFrontList;
100
101 Path<T> currentPath = kShortestPaths[metaTarget][k - 1];
102 boost::optional<state_t> maybePredecessor = currentPath.predecessorNode;
103 // this omits the first node, which is actually convenient since that's the meta-target
104
105 while (maybePredecessor) {
106 state_t predecessor = maybePredecessor.get();
107 backToFrontList.push_back(predecessor);
108
109 currentPath = kShortestPaths[predecessor][currentPath.predecessorK - 1];
110 maybePredecessor = currentPath.predecessorNode;
111 }
112
113 return backToFrontList;
114}
115
116template<typename T>
118 assert(transitionMatrix.hasTrivialRowGrouping());
119
120 // one more for meta-target
121 graphPredecessors.resize(numStates);
122
123 for (state_t i = 0; i < numStates - 1; i++) {
124 for (auto const& transition : transitionMatrix.getRowGroup(i)) {
125 // to avoid non-minimal paths, the meta-target-predecessors are
126 // *not* predecessors of any state but the meta-target
127 if (!isMetaTargetPredecessor(i)) {
128 graphPredecessors[transition.getColumn()].push_back(i);
129 }
130 }
131 }
132
133 // meta-target has exactly the meta-target-predecessors as predecessors
134 // (duh. note that the meta-target-predecessors used to be called target,
135 // but that's not necessarily true in the matrix/value invocation case)
136 for (auto targetProbPair : targetProbMap) {
137 graphPredecessors[metaTarget].push_back(targetProbPair.first);
138 }
139}
140
141template<typename T>
142void ShortestPathsGenerator<T>::performDijkstra() {
143 // the existing Dijkstra isn't working anyway AND
144 // doesn't fully meet our requirements, so let's roll our own
145
146 T inftyDistance = zero<T>();
147 T zeroDistance = one<T>();
148 shortestPathDistances.resize(numStates, inftyDistance);
149 shortestPathPredecessors.resize(numStates, boost::optional<state_t>());
150
151 // set serves as priority queue with unique membership
152 // default comparison on pair actually works fine if distance is the first entry
153 std::set<std::pair<T, state_t>, std::greater<std::pair<T, state_t>>> dijkstraQueue;
154
155 for (state_t initialState : initialStates) {
156 shortestPathDistances[initialState] = zeroDistance;
157 dijkstraQueue.emplace(zeroDistance, initialState);
158 }
159
160 while (!dijkstraQueue.empty()) {
161 state_t currentNode = (*dijkstraQueue.begin()).second;
162 dijkstraQueue.erase(dijkstraQueue.begin());
163
164 if (!isMetaTargetPredecessor(currentNode)) {
165 // non-target node, treated normally
166 for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) {
167 state_t otherNode = transition.getColumn();
168
169 // note that distances are probabilities, thus they are multiplied and larger is better
170 T alternateDistance = shortestPathDistances[currentNode] * convertDistance(currentNode, otherNode, transition.getValue());
171 assert((zero<T>() <= alternateDistance) && (alternateDistance <= one<T>()));
172 if (alternateDistance > shortestPathDistances[otherNode]) {
173 shortestPathDistances[otherNode] = alternateDistance;
174 shortestPathPredecessors[otherNode] = boost::optional<state_t>(currentNode);
175 dijkstraQueue.emplace(alternateDistance, otherNode);
176 }
177 }
178 } else {
179 // node only has one "virtual edge" (with prob as per targetProbMap) to meta-target
180 T alternateDistance = shortestPathDistances[currentNode] * targetProbMap[currentNode];
181 if (alternateDistance > shortestPathDistances[metaTarget]) {
182 shortestPathDistances[metaTarget] = alternateDistance;
183 shortestPathPredecessors[metaTarget] = boost::optional<state_t>(currentNode);
184 }
185 // no need to enqueue meta-target
186 }
187 }
188}
189
190template<typename T>
191void ShortestPathsGenerator<T>::computeSPSuccessors() {
192 shortestPathSuccessors.resize(numStates);
193
194 for (state_t i = 0; i < numStates; i++) {
195 if (shortestPathPredecessors[i]) {
196 state_t predecessor = shortestPathPredecessors[i].get();
197 shortestPathSuccessors[predecessor].push_back(i);
198 }
199 }
200}
201
202template<typename T>
203void ShortestPathsGenerator<T>::initializeShortestPaths() {
204 kShortestPaths.resize(numStates);
205
206 // BFS in Dijkstra-SP order
207 std::queue<state_t> bfsQueue;
208 for (state_t initialState : initialStates) {
209 bfsQueue.push(initialState);
210 }
211
212 while (!bfsQueue.empty()) {
213 state_t currentNode = bfsQueue.front();
214 bfsQueue.pop();
215
216 if (!kShortestPaths[currentNode].empty()) {
217 continue; // already visited
218 }
219
220 for (state_t successorNode : shortestPathSuccessors[currentNode]) {
221 bfsQueue.push(successorNode);
222 }
223
224 // note that `shortestPathPredecessor` may not be present
225 // if current node is an initial state
226 // in this case, the boost::optional copy of an uninitialized optional is hopefully also uninitialized
227 kShortestPaths[currentNode].push_back(Path<T>{shortestPathPredecessors[currentNode], 1, shortestPathDistances[currentNode]});
228 }
229}
230
231template<typename T>
232T ShortestPathsGenerator<T>::getEdgeDistance(state_t tailNode, state_t headNode) const {
233 // just to be clear, head is where the arrow points (obviously)
234 if (headNode != metaTarget) {
235 // edge is "normal", not to meta-target
236
237 for (auto const& transition : transitionMatrix.getRowGroup(tailNode)) {
238 if (transition.getColumn() == headNode) {
239 return convertDistance(tailNode, headNode, transition.getValue());
240 }
241 }
242
243 // there is no such edge
244 // let's disallow that for now, because I'm not expecting it to happen
245 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should not happen.");
246 } else {
247 // edge must be "virtual edge" to meta-target
248 assert(isMetaTargetPredecessor(tailNode));
249 return targetProbMap.at(tailNode);
250 }
251}
252
253template<typename T>
254void ShortestPathsGenerator<T>::computeNextPath(state_t node, unsigned long k) {
255 assert(k >= 2); // Dijkstra is used for k=1
256 assert(kShortestPaths[node].size() == k - 1); // if not, the previous SP must not exist
257
258 // TODO: I could extract the candidate generation to make this function more succinct
259 if (k == 2) {
260 // Step B.1 in J&M paper
261
262 Path<T> shortestPathToNode = kShortestPaths[node][1 - 1]; // never forget index shift :-|
263
264 for (state_t predecessor : graphPredecessors[node]) {
265 // add shortest paths to predecessors plus edge to current node
266 Path<T> pathToPredecessorPlusEdge = {boost::optional<state_t>(predecessor), 1,
267 shortestPathDistances[predecessor] * getEdgeDistance(predecessor, node)};
268 candidatePaths[node].insert(pathToPredecessorPlusEdge);
269
270 // ... but not the actual shortest path
271 auto it = std::find(candidatePaths[node].begin(), candidatePaths[node].end(), shortestPathToNode);
272 if (it != candidatePaths[node].end()) {
273 candidatePaths[node].erase(it);
274 }
275 }
276 }
277
278 if (not(k == 2 && isInitialState(node))) {
279 // Steps B.2-5 in J&M paper
280
281 // the (k-1)th shortest path (i.e., one better than the one we want to compute)
282 Path<T> previousShortestPath = kShortestPaths[node][k - 1 - 1]; // oh god, I forgot index shift AGAIN
283
284 // the predecessor node on that path
285 state_t predecessor = previousShortestPath.predecessorNode.get();
286 // the path to that predecessor was the `tailK`-shortest
287 unsigned long tailK = previousShortestPath.predecessorK;
288
289 // i.e. source ~~tailK-shortest path~~> predecessor --> node
290
291 // compute one-worse-shortest path to the predecessor (if it hasn't yet been computed)
292 if (kShortestPaths[predecessor].size() < tailK + 1) {
293 // TODO: investigate recursion depth and possible iterative alternative
294 computeNextPath(predecessor, tailK + 1);
295 }
296
297 if (kShortestPaths[predecessor].size() >= tailK + 1) {
298 // take that path, add an edge to the current node; that's a candidate
299 Path<T> pathToPredecessorPlusEdge = {boost::optional<state_t>(predecessor), tailK + 1,
300 kShortestPaths[predecessor][tailK + 1 - 1].distance * getEdgeDistance(predecessor, node)};
301 candidatePaths[node].insert(pathToPredecessorPlusEdge);
302 }
303 // else there was no path; TODO: does this need handling? -- yes, but not here (because the step B.1 may have added candidates)
304 }
305
306 // Step B.6 in J&M paper
307 if (!candidatePaths[node].empty()) {
308 Path<T> minDistanceCandidate = *(candidatePaths[node].begin());
309 for (auto path : candidatePaths[node]) {
310 if (path.distance > minDistanceCandidate.distance) {
311 minDistanceCandidate = path;
312 }
313 }
314
315 candidatePaths[node].erase(std::find(candidatePaths[node].begin(), candidatePaths[node].end(), minDistanceCandidate));
316 kShortestPaths[node].push_back(minDistanceCandidate);
317 } else {
318 // TODO: kSP does not exist. this is handled later, but it would be nice to catch it as early as possble, wouldn't it?
319 STORM_LOG_TRACE("KSP: no candidates, this will trigger nonexisting ksp after exiting these recursions. TODO: handle here");
320 }
321}
322
323template<typename T>
324void ShortestPathsGenerator<T>::computeKSP(unsigned long k) {
325 if (k == 0) {
326 throw std::invalid_argument("Index 0 is invalid, since we use 1-based indices (sorry)!");
327 }
328
329 unsigned long alreadyComputedK = kShortestPaths[metaTarget].size();
330
331 for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) {
332 computeNextPath(metaTarget, nextK);
333 if (kShortestPaths[metaTarget].size() < nextK) {
334 unsigned long lastExistingK = nextK - 1;
335 STORM_LOG_DEBUG("KSP throws (as expected) due to nonexistence -- maybe this is unhandled and causes the Python interface to segfault?");
336 STORM_LOG_DEBUG("last existing k-SP has k=" + std::to_string(lastExistingK));
337 STORM_LOG_DEBUG("maybe this is unhandled and causes the Python interface to segfault?");
338 throw std::invalid_argument("k-SP does not exist for k=" + std::to_string(k));
339 }
340 }
341}
342
343template<typename T>
344void ShortestPathsGenerator<T>::printKShortestPath(state_t targetNode, unsigned long k, bool head) const {
345 // note the index shift! risk of off-by-one
346 Path<T> p = kShortestPaths[targetNode][k - 1];
347
348 if (head) {
349 std::cout << "Path (reversed";
350 if (targetNode == metaTarget) {
351 std::cout << ", w/ meta-target";
352 }
353 std::cout << "), dist (prob)=" << p.distance << ": [";
354 }
355
356 std::cout << " " << targetNode;
357
358 if (p.predecessorNode) {
359 printKShortestPath(p.predecessorNode.get(), p.predecessorK, false);
360 } else {
361 std::cout << " ]\n";
362 }
363}
364
365template class ShortestPathsGenerator<double>;
366template class ShortestPathsGenerator<storm::RationalNumber>;
367
368// only prints the info stored in the Path struct;
369// does not traverse the actual path (see printKShortestPath for that)
370template<typename T>
371std::ostream& operator<<(std::ostream& out, Path<T> const& p) {
372 out << "Path with predecessorNode: " << ((p.predecessorNode) ? std::to_string(p.predecessorNode.get()) : "None");
373 out << " predecessorK: " << p.predecessorK << " distance: " << p.distance;
374 return out;
375}
376template std::ostream& operator<<(std::ostream& out, Path<double> const& p);
377} // namespace ksp
378} // namespace utility
379} // namespace storm
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
void set(uint_fast64_t index, bool value=true)
Sets the given truth value at the given index.
A class that holds a possibly non-square matrix in the compressed row storage format.
index_type getColumnCount() const
Returns the number of columns of the matrix.
bool hasTrivialRowGrouping() const
Retrieves whether the matrix has a trivial row grouping.
ShortestPathsGenerator(Model const &model, BitVector const &targetBV)
Performs precomputations (including meta-target insertion and Dijkstra).
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.
#define STORM_LOG_DEBUG(message)
Definition logging.h:23
#define STORM_LOG_TRACE(message)
Definition logging.h:17
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::ostream & operator<<(std::ostream &out, Path< T > const &p)
storage::sparse::state_type state_t
LabParser.cpp.
Definition cli.cpp:18
boost::optional< state_t > predecessorNode