25 : transitionMatrix(transitionMatrix),
28 initialStates(initialStates),
29 targetProbMap(targetProbMap),
30 matrixFormat(matrixFormat) {
31 computePredecessors();
36 computeSPSuccessors();
39 initializeShortestPaths();
41 candidatePaths.resize(numStates);
47 :
ShortestPathsGenerator<T>(transitionMatrix, vectorToMap(targetProbVector), initialStates, matrixFormat) {}
72 return kShortestPaths[metaTarget][k - 1].distance;
80 Path<T> currentPath = kShortestPaths[metaTarget][k - 1];
81 boost::optional<state_t> maybePredecessor = currentPath.
predecessorNode;
84 while (maybePredecessor) {
85 state_t predecessor = maybePredecessor.get();
86 stateSet.
set(predecessor,
true);
88 currentPath = kShortestPaths[predecessor][currentPath.
predecessorK - 1];
99 std::vector<state_t> backToFrontList;
101 Path<T> currentPath = kShortestPaths[metaTarget][k - 1];
102 boost::optional<state_t> maybePredecessor = currentPath.
predecessorNode;
105 while (maybePredecessor) {
106 state_t predecessor = maybePredecessor.get();
107 backToFrontList.push_back(predecessor);
109 currentPath = kShortestPaths[predecessor][currentPath.
predecessorK - 1];
113 return backToFrontList;
121 graphPredecessors.resize(numStates);
123 for (
state_t i = 0; i < numStates - 1; i++) {
124 for (
auto const& transition : transitionMatrix.getRowGroup(i)) {
127 if (!isMetaTargetPredecessor(i)) {
128 graphPredecessors[transition.getColumn()].push_back(i);
136 for (
auto targetProbPair : targetProbMap) {
137 graphPredecessors[metaTarget].push_back(targetProbPair.first);
142void ShortestPathsGenerator<T>::performDijkstra() {
146 T inftyDistance = zero<T>();
147 T zeroDistance = one<T>();
148 shortestPathDistances.resize(numStates, inftyDistance);
149 shortestPathPredecessors.resize(numStates, boost::optional<state_t>());
153 std::set<std::pair<T, state_t>, std::greater<std::pair<T, state_t>>> dijkstraQueue;
155 for (
state_t initialState : initialStates) {
156 shortestPathDistances[initialState] = zeroDistance;
157 dijkstraQueue.emplace(zeroDistance, initialState);
160 while (!dijkstraQueue.empty()) {
161 state_t currentNode = (*dijkstraQueue.begin()).second;
162 dijkstraQueue.erase(dijkstraQueue.begin());
164 if (!isMetaTargetPredecessor(currentNode)) {
166 for (
auto const& transition : transitionMatrix.getRowGroup(currentNode)) {
167 state_t otherNode = transition.getColumn();
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);
180 T alternateDistance = shortestPathDistances[currentNode] * targetProbMap[currentNode];
181 if (alternateDistance > shortestPathDistances[metaTarget]) {
182 shortestPathDistances[metaTarget] = alternateDistance;
183 shortestPathPredecessors[metaTarget] = boost::optional<state_t>(currentNode);
191void ShortestPathsGenerator<T>::computeSPSuccessors() {
192 shortestPathSuccessors.resize(numStates);
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);
203void ShortestPathsGenerator<T>::initializeShortestPaths() {
204 kShortestPaths.resize(numStates);
207 std::queue<state_t> bfsQueue;
208 for (
state_t initialState : initialStates) {
209 bfsQueue.push(initialState);
212 while (!bfsQueue.empty()) {
213 state_t currentNode = bfsQueue.front();
216 if (!kShortestPaths[currentNode].empty()) {
220 for (
state_t successorNode : shortestPathSuccessors[currentNode]) {
221 bfsQueue.push(successorNode);
227 kShortestPaths[currentNode].push_back(Path<T>{shortestPathPredecessors[currentNode], 1, shortestPathDistances[currentNode]});
232T ShortestPathsGenerator<T>::getEdgeDistance(
state_t tailNode,
state_t headNode)
const {
234 if (headNode != metaTarget) {
237 for (
auto const& transition : transitionMatrix.getRowGroup(tailNode)) {
238 if (transition.getColumn() == headNode) {
239 return convertDistance(tailNode, headNode, transition.getValue());
245 STORM_LOG_THROW(
false, storm::exceptions::UnexpectedException,
"Should not happen.");
248 assert(isMetaTargetPredecessor(tailNode));
249 return targetProbMap.at(tailNode);
254void ShortestPathsGenerator<T>::computeNextPath(
state_t node,
unsigned long k) {
256 assert(kShortestPaths[node].size() == k - 1);
262 Path<T> shortestPathToNode = kShortestPaths[node][1 - 1];
264 for (
state_t predecessor : graphPredecessors[node]) {
266 Path<T> pathToPredecessorPlusEdge = {boost::optional<state_t>(predecessor), 1,
267 shortestPathDistances[predecessor] * getEdgeDistance(predecessor, node)};
268 candidatePaths[node].insert(pathToPredecessorPlusEdge);
271 auto it = std::find(candidatePaths[node].begin(), candidatePaths[node].end(), shortestPathToNode);
272 if (it != candidatePaths[node].end()) {
273 candidatePaths[node].erase(it);
278 if (not(k == 2 && isInitialState(node))) {
282 Path<T> previousShortestPath = kShortestPaths[node][k - 1 - 1];
285 state_t predecessor = previousShortestPath.predecessorNode.get();
287 unsigned long tailK = previousShortestPath.predecessorK;
292 if (kShortestPaths[predecessor].size() < tailK + 1) {
294 computeNextPath(predecessor, tailK + 1);
297 if (kShortestPaths[predecessor].size() >= tailK + 1) {
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);
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;
315 candidatePaths[node].erase(std::find(candidatePaths[node].begin(), candidatePaths[node].end(), minDistanceCandidate));
316 kShortestPaths[node].push_back(minDistanceCandidate);
319 STORM_LOG_TRACE(
"KSP: no candidates, this will trigger nonexisting ksp after exiting these recursions. TODO: handle here");
324void ShortestPathsGenerator<T>::computeKSP(
unsigned long k) {
326 throw std::invalid_argument(
"Index 0 is invalid, since we use 1-based indices (sorry)!");
329 unsigned long alreadyComputedK = kShortestPaths[metaTarget].size();
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));
344void ShortestPathsGenerator<T>::printKShortestPath(
state_t targetNode,
unsigned long k,
bool head)
const {
346 Path<T> p = kShortestPaths[targetNode][k - 1];
349 std::cout <<
"Path (reversed";
350 if (targetNode == metaTarget) {
351 std::cout <<
", w/ meta-target";
353 std::cout <<
"), dist (prob)=" << p.distance <<
": [";
356 std::cout <<
" " << targetNode;
358 if (p.predecessorNode) {
359 printKShortestPath(p.predecessorNode.get(), p.predecessorK,
false);
365template class ShortestPathsGenerator<double>;
366template class ShortestPathsGenerator<storm::RationalNumber>;