From cf1fa2bfc9eed62327fa549e7b5f5ecaee0693a9 Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 12 Feb 2016 20:27:55 +0100
Subject: [PATCH 01/13] the plan
---
src/utility/shortestPaths.md | 22 ++++++++++++++++++++++
1 file changed, 22 insertions(+)
diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md
index 61f6fe1e3..db5dcc326 100644
--- a/src/utility/shortestPaths.md
+++ b/src/utility/shortestPaths.md
@@ -39,6 +39,28 @@ target group is required in the constructor. (It would have been possible to
allow for interchangeable target groups, but I don't anticipate that use
case.)
+#### Special case: Using Matrix/Vector from SamplingModel
+
+The class has been updated to support the matrix/vector that `SamplingModel`
+generates (as an instance of a PDTMC) as input. This is in fact closely
+related to the target groups, since it works as follows:
+
+The input is a (sub-stochastic) transition matrix of the maybe-states (only!)
+and a vector (again over the maybe-states) with the probabilities to an
+implied target state.
+
+This naturally corresponds to having a meta-target, except the probability
+of its incoming edges range over $(0,1]$ rather than being $1$.
+Thus, applying the term "target group" to the set of states with non-zero
+transitions to the meta-target is now misleading (I suppose the correct term
+would now be "meta-target predecessors"), but nevertheless it should work
+exactly the same. [Right?]
+
+In terms of implementation, in `getEdgeDistance` as well as in the loop of
+the Dijkstra, the "virtual" edges to the meta-target were checked for and
+set to probability $1$; this must now be changed to use the probability as
+indicated in the `targetProbVector` if this input format is used.
+
### Minimality of paths
Secondly, we define shortest paths as "minimal" shortest paths in the
following sense: The path may not visit any target state except at the
From e883c605198f7f7fe0d977549af379a7f5ee63a9 Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 12 Feb 2016 20:31:48 +0100
Subject: [PATCH 02/13] rm model as member; extracting all needed stuff in ctor
# Conflicts:
# src/utility/shortestPaths.cpp
---
src/utility/shortestPaths.cpp | 15 +++++++--------
src/utility/shortestPaths.h | 14 +++++++++-----
2 files changed, 16 insertions(+), 13 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index ac868070d..409030c32 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -8,12 +8,11 @@ namespace storm {
namespace ksp {
template <typename T>
ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model,
- state_list_t const& targets) : model(model), targets(targets) {
- // FIXME: does this create a copy? I don't need one, so I should avoid that
- transitionMatrix = model->getTransitionMatrix();
- numStates = model->getNumberOfStates() + 1; // one more for meta-target
-
- metaTarget = numStates - 1; // first unused state number
+ state_list_t const& targets) : transitionMatrix(model->getTransitionMatrix()),
+ numStates(model->getNumberOfStates() + 1), // one more for meta-target
+ metaTarget(model->getNumberOfStates()), // first unused state number
+ initialStates(model->getInitialStates()),
+ targets(targets) {
targetSet = std::unordered_set<state_t>(targets.begin(), targets.end());
computePredecessors();
@@ -126,7 +125,7 @@ namespace storm {
// default comparison on pair actually works fine if distance is the first entry
std::set<std::pair<T, state_t>, std::greater<std::pair<T, state_t>>> dijkstraQueue;
- for (state_t initialState : model->getInitialStates()) {
+ for (state_t initialState : initialStates) {
shortestPathDistances[initialState] = zeroDistance;
dijkstraQueue.emplace(zeroDistance, initialState);
}
@@ -179,7 +178,7 @@ namespace storm {
// BFS in Dijkstra-SP order
std::queue<state_t> bfsQueue;
- for (state_t initialState : model->getInitialStates()) {
+ for (state_t initialState : initialStates) {
bfsQueue.push(initialState);
}
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index 8139f1c91..64fa16ca6 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -63,7 +63,13 @@ namespace storm {
// all of which will be converted to list and delegated to constructor above
ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, state_t singleTarget);
ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, storage::BitVector const& targetBV);
- ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::string const& targetLabel);
+ ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::string const& targetLabel = "target");
+
+ // a further alternative: use transition matrix of maybe-states
+ // combined with target vector (e.g., the instantiated matrix/
+ // vector from SamplingModel);
+ // in this case separately specifying a target makes no sense
+ //ShortestPathsGenerator(storm::storage::SparseMatrix<T> maybeTransitionMatrix, std::vector<T> targetProbVector);
inline ~ShortestPathsGenerator(){}
@@ -91,13 +97,12 @@ namespace storm {
private:
- std::shared_ptr<models::sparse::Model<T>> model;
storage::SparseMatrix<T> transitionMatrix;
state_t numStates; // includes meta-target, i.e. states in model + 1
-
- state_list_t targets;
std::unordered_set<state_t> targetSet;
state_t metaTarget;
+ storage::BitVector initialStates;
+ state_list_t targets;
std::vector<state_list_t> graphPredecessors;
std::vector<boost::optional<state_t>> shortestPathPredecessors;
@@ -160,7 +165,6 @@ namespace storm {
// --- tiny helper fcts ---
inline bool isInitialState(state_t node) const {
- auto initialStates = model->getInitialStates();
return find(initialStates.begin(), initialStates.end(), node) != initialStates.end();
}
From 235671d67db81fefb6fda58f37e6cb8652ed5aaa Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 12 Feb 2016 20:41:55 +0100
Subject: [PATCH 03/13] use map rather than set for target[Prob]
---
src/utility/shortestPaths.cpp | 8 +++++---
src/utility/shortestPaths.h | 2 +-
2 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index 409030c32..3b6772464 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -13,7 +13,9 @@ namespace storm {
metaTarget(model->getNumberOfStates()), // first unused state number
initialStates(model->getInitialStates()),
targets(targets) {
- targetSet = std::unordered_set<state_t>(targets.begin(), targets.end());
+ for (state_t target : targets) {
+ targetProbMap.emplace(target, one<T>());
+ }
computePredecessors();
@@ -134,7 +136,7 @@ namespace storm {
state_t currentNode = (*dijkstraQueue.begin()).second;
dijkstraQueue.erase(dijkstraQueue.begin());
- if (targetSet.count(currentNode) == 0) {
+ if (targetProbMap.count(currentNode) == 0) {
// non-target node, treated normally
for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) {
state_t otherNode = transition.getColumn();
@@ -223,7 +225,7 @@ namespace storm {
return utility::zero<T>();
} else {
// edge must be "virtual edge" from target state to meta-target
- assert(targetSet.count(tailNode) == 1);
+ assert(targetProbMap.count(tailNode) == 1);
return utility::one<T>();
}
}
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index 64fa16ca6..2c8927609 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -99,10 +99,10 @@ namespace storm {
private:
storage::SparseMatrix<T> transitionMatrix;
state_t numStates; // includes meta-target, i.e. states in model + 1
- std::unordered_set<state_t> targetSet;
state_t metaTarget;
storage::BitVector initialStates;
state_list_t targets;
+ std::unordered_map<state_t, T> targetProbMap;
std::vector<state_list_t> graphPredecessors;
std::vector<boost::optional<state_t>> shortestPathPredecessors;
From 55599b51e7ffefed077884d4f3e48527aadd6e7d Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 12 Feb 2016 22:32:42 +0100
Subject: [PATCH 04/13] aliased BitVector, used state_t more (cosmetic)
---
src/utility/shortestPaths.cpp | 4 ++--
src/utility/shortestPaths.h | 3 ++-
test/functional/utility/KSPTest.cpp | 18 +++++++++---------
3 files changed, 13 insertions(+), 12 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index 3b6772464..02356d974 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -52,9 +52,9 @@ namespace storm {
}
template <typename T>
- storage::BitVector ShortestPathsGenerator<T>::getStates(unsigned long k) {
+ BitVector ShortestPathsGenerator<T>::getStates(unsigned long k) {
computeKSP(k);
- storage::BitVector stateSet(numStates - 1, false); // no meta-target
+ BitVector stateSet(numStates - 1, false); // no meta-target
Path<T> currentPath = kShortestPaths[metaTarget][k - 1];
boost::optional<state_t> maybePredecessor = currentPath.predecessorNode;
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index 2c8927609..d1219d390 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -26,6 +26,7 @@ namespace storm {
namespace ksp {
typedef storage::sparse::state_type state_t;
typedef std::vector<state_t> state_list_t;
+ using BitVector = storage::BitVector;
template <typename T>
struct Path {
@@ -100,8 +101,8 @@ namespace storm {
storage::SparseMatrix<T> transitionMatrix;
state_t numStates; // includes meta-target, i.e. states in model + 1
state_t metaTarget;
- storage::BitVector initialStates;
state_list_t targets;
+ BitVector initialStates;
std::unordered_map<state_t, T> targetProbMap;
std::vector<state_list_t> graphPredecessors;
diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp
index aba8747c3..746118319 100644
--- a/test/functional/utility/KSPTest.cpp
+++ b/test/functional/utility/KSPTest.cpp
@@ -25,7 +25,7 @@ std::shared_ptr<storm::models::sparse::Model<double>> buildExampleModel() {
TEST(KSPTest, dijkstra) {
auto model = buildExampleModel();
- storm::storage::sparse::state_type testState = 300;
+ storm::utility::ksp::state_t testState = 300;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
double dist = spg.getDistance(1);
@@ -35,7 +35,7 @@ TEST(KSPTest, dijkstra) {
TEST(KSPTest, singleTarget) {
auto model = buildExampleModel();
- storm::storage::sparse::state_type testState = 300;
+ storm::utility::ksp::state_t testState = 300;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
double dist = spg.getDistance(100);
@@ -45,7 +45,7 @@ TEST(KSPTest, singleTarget) {
TEST(KSPTest, reentry) {
auto model = buildExampleModel();
- storm::storage::sparse::state_type testState = 300;
+ storm::utility::ksp::state_t testState = 300;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
double dist = spg.getDistance(100);
@@ -59,7 +59,7 @@ TEST(KSPTest, reentry) {
TEST(KSPTest, groupTarget) {
auto model = buildExampleModel();
- auto groupTarget = storm::utility::ksp::state_list_t{50, 90};
+ auto groupTarget = std::vector<storm::utility::ksp::state_t>{50, 90};
auto spg = storm::utility::ksp::ShortestPathsGenerator<double>(model, groupTarget);
// this path should lead to 90
@@ -78,7 +78,7 @@ TEST(KSPTest, groupTarget) {
TEST(KSPTest, kTooLargeException) {
auto model = buildExampleModel();
- storm::storage::sparse::state_type testState = 1;
+ storm::utility::ksp::state_t testState = 1;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
ASSERT_THROW(spg.getDistance(2), std::invalid_argument);
@@ -87,11 +87,11 @@ TEST(KSPTest, kTooLargeException) {
TEST(KSPTest, kspStateSet) {
auto model = buildExampleModel();
- storm::storage::sparse::state_type testState = 300;
+ storm::utility::ksp::state_t testState = 300;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
storm::storage::BitVector referenceBV(model->getNumberOfStates(), false);
- for (auto s : storm::utility::ksp::state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}) {
+ for (auto s : std::vector<storm::utility::ksp::state_t>{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}) {
referenceBV.set(s, true);
}
@@ -103,11 +103,11 @@ TEST(KSPTest, kspStateSet) {
TEST(KSPTest, kspPathAsList) {
auto model = buildExampleModel();
- storm::storage::sparse::state_type testState = 300;
+ storm::utility::ksp::state_t testState = 300;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
// TODO: use path that actually has a loop or something to make this more interesting
- auto reference = storm::utility::ksp::state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0};
+ auto reference = std::vector<storm::utility::ksp::state_t>{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0};
auto list = spg.getPathAsList(7);
EXPECT_EQ(list, reference);
From 44b3a9108e72137cc2d662e6e5da4048029e9c5e Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 12 Feb 2016 22:39:08 +0100
Subject: [PATCH 05/13] switching from vector<state_t> to BV as authoritative
input
# Conflicts:
# src/utility/shortestPaths.h
---
src/utility/shortestPaths.cpp | 21 +++++++++++++--------
src/utility/shortestPaths.h | 28 +++++++++++++---------------
test/functional/utility/KSPTest.cpp | 2 +-
3 files changed, 27 insertions(+), 24 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index 02356d974..15039a4c3 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -30,20 +30,25 @@ namespace storm {
candidatePaths.resize(numStates);
}
+ // extracts the relevant info from the model and delegates to ctor above
+ template <typename T>
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, BitVector const& targetBV)
+ : ShortestPathsGenerator<T>(model->getTransitionMatrix(), allProbOneMap(targetBV), model->getInitialStates()) {}
+
// several alternative ways to specify the targets are provided,
// each converts the targets and delegates to the ctor above
// I admit it's kind of ugly, but actually pretty convenient (and I've wanted to try C++11 delegation)
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model,
- state_t singleTarget) : ShortestPathsGenerator<T>(model, std::vector<state_t>{singleTarget}) {}
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, state_t singleTarget)
+ : ShortestPathsGenerator<T>(model, std::vector<state_t>{singleTarget}) {}
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model,
- storage::BitVector const& targetBV) : ShortestPathsGenerator<T>(model, bitvectorToList(targetBV)) {}
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::vector<state_t> const& targetList)
+ : ShortestPathsGenerator<T>(model, BitVector(model->getNumberOfStates(), targetList)) {}
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model,
- std::string const& targetLabel) : ShortestPathsGenerator<T>(model, bitvectorToList(model->getStates(targetLabel))) {}
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::string const& targetLabel)
+ : ShortestPathsGenerator<T>(model, model->getStates(targetLabel)) {}
template <typename T>
T ShortestPathsGenerator<T>::getDistance(unsigned long k) {
@@ -72,10 +77,10 @@ namespace storm {
}
template <typename T>
- state_list_t ShortestPathsGenerator<T>::getPathAsList(unsigned long k) {
+ std::vector<state_t> ShortestPathsGenerator<T>::getPathAsList(unsigned long k) {
computeKSP(k);
- state_list_t backToFrontList;
+ std::vector<state_t> backToFrontList;
Path<T> currentPath = kShortestPaths[metaTarget][k - 1];
boost::optional<state_t> maybePredecessor = currentPath.predecessorNode;
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index d1219d390..402fb31f6 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -12,21 +12,20 @@
// for more information about the purpose, design decisions,
// etc., you may consult `shortestPath.md`. - Tom
-/*
- * TODO:
- * - take care of self-loops of target states
- * - implement target group
- * - think about how to get paths with new nodes, rather than different
- * paths over the same set of states (which happens often)
- */
+// TODO: test whether using BitVector instead of vector<state_t> is
+// faster for storing predecessors etc.
+// Now using BitVectors instead of vector<state_t> 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.)
namespace storm {
namespace utility {
namespace ksp {
typedef storage::sparse::state_type state_t;
- typedef std::vector<state_t> state_list_t;
using BitVector = storage::BitVector;
+ typedef std::vector<state_t> ordered_state_list_t;
template <typename T>
struct Path {
@@ -57,13 +56,12 @@ namespace storm {
* Modifications are done locally, `model` remains unchanged.
* Target (group) cannot be changed.
*/
- // FIXME: this shared_ptr-passing business might be a bad idea
- ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, state_list_t const& targets);
+ ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, BitVector const& targetBV);
// allow alternative ways of specifying the target,
- // all of which will be converted to list and delegated to constructor above
+ // all of which will be converted to BitVector and delegated to constructor above
ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, state_t singleTarget);
- ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, storage::BitVector const& targetBV);
+ ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::vector<state_t> const& targetList);
ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::string const& targetLabel = "target");
// a further alternative: use transition matrix of maybe-states
@@ -94,7 +92,7 @@ namespace storm {
* Computes KSP if not yet computed.
* @throws std::invalid_argument if no such k-shortest path exists
*/
- state_list_t getPathAsList(unsigned long k);
+ ordered_state_list_t getPathAsList(unsigned long k);
private:
@@ -105,9 +103,9 @@ namespace storm {
BitVector initialStates;
std::unordered_map<state_t, T> targetProbMap;
- std::vector<state_list_t> graphPredecessors;
+ std::vector<ordered_state_list_t> graphPredecessors; // FIXME is a switch to BitVector a good idea here?
std::vector<boost::optional<state_t>> shortestPathPredecessors;
- std::vector<state_list_t> shortestPathSuccessors;
+ std::vector<ordered_state_list_t> shortestPathSuccessors;
std::vector<T> shortestPathDistances;
std::vector<std::vector<Path<T>>> kShortestPaths;
diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp
index 746118319..d1c9a2f8f 100644
--- a/test/functional/utility/KSPTest.cpp
+++ b/test/functional/utility/KSPTest.cpp
@@ -107,7 +107,7 @@ TEST(KSPTest, kspPathAsList) {
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
// TODO: use path that actually has a loop or something to make this more interesting
- auto reference = std::vector<storm::utility::ksp::state_t>{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0};
+ auto reference = storm::utility::ksp::ordered_state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0};
auto list = spg.getPathAsList(7);
EXPECT_EQ(list, reference);
From 51c44bb7866e29a5541366d3dd440c7c23a63a7f Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 12 Feb 2016 22:42:58 +0100
Subject: [PATCH 06/13] matrix/vector ctor, targetProbMap, TODO: non-1 entries
---
src/utility/shortestPaths.cpp | 29 +++++++++++++++--------------
src/utility/shortestPaths.h | 19 +++++++++++++------
2 files changed, 28 insertions(+), 20 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index 15039a4c3..ffd3730f1 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -7,15 +7,12 @@ namespace storm {
namespace utility {
namespace ksp {
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model,
- state_list_t const& targets) : transitionMatrix(model->getTransitionMatrix()),
- numStates(model->getNumberOfStates() + 1), // one more for meta-target
- metaTarget(model->getNumberOfStates()), // first unused state number
- initialStates(model->getInitialStates()),
- targets(targets) {
- for (state_t target : targets) {
- targetProbMap.emplace(target, one<T>());
- }
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> transitionMatrix, std::unordered_map<state_t, T> targetProbMap, BitVector initialStates) :
+ transitionMatrix(transitionMatrix),
+ numStates(transitionMatrix.getColumnCount() + 1), // one more for meta-target
+ metaTarget(transitionMatrix.getColumnCount()), // first unused state index
+ initialStates(initialStates),
+ targetProbMap(targetProbMap) {
computePredecessors();
@@ -30,6 +27,8 @@ namespace storm {
candidatePaths.resize(numStates);
}
+ // TODO: probTargetVector [!] to probTargetMap ctor
+
// extracts the relevant info from the model and delegates to ctor above
template <typename T>
ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, BitVector const& targetBV)
@@ -108,14 +107,16 @@ namespace storm {
for (auto const& transition : transitionMatrix.getRowGroup(i)) {
// to avoid non-minimal paths, the target states are
// *not* predecessors of any state but the meta-target
- if (std::find(targets.begin(), targets.end(), i) == targets.end()) {
+ if (!isTargetState(i)) {
graphPredecessors[transition.getColumn()].push_back(i);
}
}
}
// meta-target has exactly the target states as predecessors
- graphPredecessors[metaTarget] = targets;
+ for (auto targetProbPair : targetProbMap) { // FIXME
+ graphPredecessors[metaTarget].push_back(targetProbPair.first);
+ }
}
template <typename T>
@@ -141,7 +142,7 @@ namespace storm {
state_t currentNode = (*dijkstraQueue.begin()).second;
dijkstraQueue.erase(dijkstraQueue.begin());
- if (targetProbMap.count(currentNode) == 0) {
+ if (!isTargetState(currentNode)) {
// non-target node, treated normally
for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) {
state_t otherNode = transition.getColumn();
@@ -157,7 +158,7 @@ namespace storm {
} else {
// target node has only "virtual edge" (with prob 1) to meta-target
// no multiplication necessary
- T alternateDistance = shortestPathDistances[currentNode];
+ T alternateDistance = shortestPathDistances[currentNode]; // FIXME
if (alternateDistance > shortestPathDistances[metaTarget]) {
shortestPathDistances[metaTarget] = alternateDistance;
shortestPathPredecessors[metaTarget] = boost::optional<state_t>(currentNode);
@@ -231,7 +232,7 @@ namespace storm {
} else {
// edge must be "virtual edge" from target state to meta-target
assert(targetProbMap.count(tailNode) == 1);
- return utility::one<T>();
+ return one<T>();
}
}
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index 402fb31f6..400485997 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -69,6 +69,7 @@ namespace storm {
// vector from SamplingModel);
// in this case separately specifying a target makes no sense
//ShortestPathsGenerator(storm::storage::SparseMatrix<T> maybeTransitionMatrix, std::vector<T> targetProbVector);
+ ShortestPathsGenerator(storm::storage::SparseMatrix<T> maybeTransitionMatrix, std::unordered_map<state_t, T> targetProbMap, BitVector initialStates);
inline ~ShortestPathsGenerator(){}
@@ -99,7 +100,6 @@ namespace storm {
storage::SparseMatrix<T> transitionMatrix;
state_t numStates; // includes meta-target, i.e. states in model + 1
state_t metaTarget;
- state_list_t targets;
BitVector initialStates;
std::unordered_map<state_t, T> targetProbMap;
@@ -167,12 +167,19 @@ namespace storm {
return find(initialStates.begin(), initialStates.end(), node) != initialStates.end();
}
- inline state_list_t bitvectorToList(storage::BitVector const& bv) const {
- state_list_t list;
- for (state_t state : bv) {
- list.push_back(state);
+ inline bool isTargetState(state_t node) const {
+ return targetProbMap.count(node) == 1;
+ }
+
+ /**
+ * Returns a map where each state of the input BitVector is mapped to 1 (`one<T>`).
+ */
+ inline std::unordered_map<state_t, T> allProbOneMap(BitVector bitVector) const& {
+ std::unordered_map<state_t, T> stateProbMap;
+ for (state_t node : bitVector) {
+ stateProbMap.emplace(node, one<T>());
}
- return list;
+ return stateProbMap;
}
// -----------------------
};
From 5f6637448130e1274111894c2d3b2bf5ef4dd3e1 Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 12 Feb 2016 23:00:21 +0100
Subject: [PATCH 07/13] vector to map conversion
---
src/utility/shortestPaths.cpp | 4 +++-
src/utility/shortestPaths.h | 29 +++++++++++++++++++++++------
2 files changed, 26 insertions(+), 7 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index ffd3730f1..f70799d15 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -27,7 +27,9 @@ namespace storm {
candidatePaths.resize(numStates);
}
- // TODO: probTargetVector [!] to probTargetMap ctor
+ template <typename T>
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> transitionMatrix, std::vector<T> targetProbVector, BitVector initialStates)
+ : ShortestPathsGenerator<T>(transitionMatrix, vectorToMap(targetProbVector), initialStates) {}
// extracts the relevant info from the model and delegates to ctor above
template <typename T>
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index 400485997..b78a0758a 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -65,11 +65,11 @@ namespace storm {
ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::string const& targetLabel = "target");
// a further alternative: use transition matrix of maybe-states
- // combined with target vector (e.g., the instantiated matrix/
- // vector from SamplingModel);
+ // combined with target vector (e.g., the instantiated matrix/vector from SamplingModel);
// in this case separately specifying a target makes no sense
- //ShortestPathsGenerator(storm::storage::SparseMatrix<T> maybeTransitionMatrix, std::vector<T> targetProbVector);
- ShortestPathsGenerator(storm::storage::SparseMatrix<T> maybeTransitionMatrix, std::unordered_map<state_t, T> targetProbMap, BitVector initialStates);
+ ShortestPathsGenerator(storage::SparseMatrix<T> transitionMatrix, std::vector<T> targetProbVector, BitVector initialStates);
+ ShortestPathsGenerator(storage::SparseMatrix<T> maybeTransitionMatrix, std::unordered_map<state_t, T> targetProbMap, BitVector initialStates);
+
inline ~ShortestPathsGenerator(){}
@@ -174,13 +174,30 @@ namespace storm {
/**
* Returns a map where each state of the input BitVector is mapped to 1 (`one<T>`).
*/
- inline std::unordered_map<state_t, T> allProbOneMap(BitVector bitVector) const& {
+ inline std::unordered_map<state_t, T> allProbOneMap(BitVector bitVector) const {
std::unordered_map<state_t, T> stateProbMap;
for (state_t node : bitVector) {
- stateProbMap.emplace(node, one<T>());
+ stateProbMap.emplace(node, one<T>()); // FIXME check rvalue warning (here and below)
}
return stateProbMap;
}
+
+ inline std::unordered_map<state_t, T> vectorToMap(std::vector<T> probVector) const {
+ assert(probVector.size() == numStates);
+
+ std::unordered_map<state_t, T> stateProbMap;
+
+ // non-zero entries (i.e. true transitions) are added to the map
+ for (state_t i = 0; i < probVector.size(); i++) {
+ T probEntry = probVector[i];
+ if (probEntry != 0) {
+ assert(0 < probEntry <= 1);
+ stateProbMap.emplace(i, probEntry);
+ }
+ }
+
+ return stateProbMap;
+ }
// -----------------------
};
}
From b58d48f92dee69634dd1e7c8f378bc4d7beeb1eb Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 12 Feb 2016 23:54:27 +0100
Subject: [PATCH 08/13] use probs from targetProbMap TODO: test
---
src/utility/shortestPaths.cpp | 24 +++++++++++++-----------
src/utility/shortestPaths.h | 4 ++--
src/utility/shortestPaths.md | 12 +++++++-----
3 files changed, 22 insertions(+), 18 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index f70799d15..c9ce0b608 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -107,16 +107,18 @@ namespace storm {
for (state_t i = 0; i < numStates - 1; i++) {
for (auto const& transition : transitionMatrix.getRowGroup(i)) {
- // to avoid non-minimal paths, the target states are
+ // to avoid non-minimal paths, the meta-target-predecessors are
// *not* predecessors of any state but the meta-target
- if (!isTargetState(i)) {
+ if (!isMetaTargetPredecessor(i)) {
graphPredecessors[transition.getColumn()].push_back(i);
}
}
}
- // meta-target has exactly the target states as predecessors
- for (auto targetProbPair : targetProbMap) { // FIXME
+ // meta-target has exactly the meta-target-predecessors as predecessors
+ // (duh. note that the meta-target-predecessors used to be called target,
+ // but that's not necessarily true in the matrix/value invocation case)
+ for (auto targetProbPair : targetProbMap) {
graphPredecessors[metaTarget].push_back(targetProbPair.first);
}
}
@@ -144,7 +146,7 @@ namespace storm {
state_t currentNode = (*dijkstraQueue.begin()).second;
dijkstraQueue.erase(dijkstraQueue.begin());
- if (!isTargetState(currentNode)) {
+ if (!isMetaTargetPredecessor(currentNode)) {
// non-target node, treated normally
for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) {
state_t otherNode = transition.getColumn();
@@ -158,9 +160,9 @@ namespace storm {
}
}
} else {
- // target node has only "virtual edge" (with prob 1) to meta-target
- // no multiplication necessary
- T alternateDistance = shortestPathDistances[currentNode]; // FIXME
+ // 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;
shortestPathPredecessors[metaTarget] = boost::optional<state_t>(currentNode);
@@ -232,9 +234,9 @@ namespace storm {
assert(false);
return utility::zero<T>();
} else {
- // edge must be "virtual edge" from target state to meta-target
- assert(targetProbMap.count(tailNode) == 1);
- return one<T>();
+ // edge must be "virtual edge" to meta-target
+ assert(isMetaTargetPredecessor(tailNode));
+ return targetProbMap.at(tailNode); // FIXME double check
}
}
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index b78a0758a..1cda2eb99 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -103,7 +103,7 @@ namespace storm {
BitVector initialStates;
std::unordered_map<state_t, T> targetProbMap;
- std::vector<ordered_state_list_t> graphPredecessors; // FIXME is a switch to BitVector a good idea here?
+ std::vector<ordered_state_list_t> graphPredecessors;
std::vector<boost::optional<state_t>> shortestPathPredecessors;
std::vector<ordered_state_list_t> shortestPathSuccessors;
std::vector<T> shortestPathDistances;
@@ -167,7 +167,7 @@ namespace storm {
return find(initialStates.begin(), initialStates.end(), node) != initialStates.end();
}
- inline bool isTargetState(state_t node) const {
+ inline bool isMetaTargetPredecessor(state_t node) const {
return targetProbMap.count(node) == 1;
}
diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md
index db5dcc326..f2beb801a 100644
--- a/src/utility/shortestPaths.md
+++ b/src/utility/shortestPaths.md
@@ -52,9 +52,8 @@ implied target state.
This naturally corresponds to having a meta-target, except the probability
of its incoming edges range over $(0,1]$ rather than being $1$.
Thus, applying the term "target group" to the set of states with non-zero
-transitions to the meta-target is now misleading (I suppose the correct term
-would now be "meta-target predecessors"), but nevertheless it should work
-exactly the same. [Right?]
+transitions to the meta-target is now misleading[^1], but nevertheless it
+should work exactly the same. [Right?]
In terms of implementation, in `getEdgeDistance` as well as in the loop of
the Dijkstra, the "virtual" edges to the meta-target were checked for and
@@ -98,11 +97,14 @@ path to some node `u` plus an edge to `t`:
Further, the shortest paths to some node are always computed in order and
without gaps, e.g., the 1, 2, 3-shortest paths to `t` will be computed
before the 4-SP. Thus, we store the SPs in a linked list for each node,
-with the k-th entry[^1] being the k-th SP to that node.
+with the k-th entry[^2] being the k-th SP to that node.
Thus for an SP as shown above we simply store the predecessor node (`u`)
and the `k`, which allows us to look up the tail of the SP.
By recursively looking up the tail (until it's empty), we reconstruct
the entire path back-to-front.
-[^1]: Which due to 0-based indexing has index `k-1`, of course! Damn it.
+[^1]: I suppose the correct term would now be "meta-target predecessors".
+ In fact, I will rename all occurences of `target` in the source to
+ `metaTargetPredecessors` – clumsy but accurate.
+[^2]: Which due to 0-based indexing has index `k-1`, of course! Damn it.
From 67ce5cf18d9db7498fcb69804547e4f0d0aa73cb Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 18 Nov 2016 16:46:48 +0100
Subject: [PATCH 09/13] const& in signatures
---
src/utility/shortestPaths.cpp | 4 ++--
src/utility/shortestPaths.h | 6 +++---
2 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index c9ce0b608..8d1dd079f 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -7,7 +7,7 @@ namespace storm {
namespace utility {
namespace ksp {
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> transitionMatrix, std::unordered_map<state_t, T> targetProbMap, BitVector initialStates) :
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> const& transitionMatrix, std::unordered_map<state_t, T> const& targetProbMap, BitVector const& initialStates) :
transitionMatrix(transitionMatrix),
numStates(transitionMatrix.getColumnCount() + 1), // one more for meta-target
metaTarget(transitionMatrix.getColumnCount()), // first unused state index
@@ -28,7 +28,7 @@ namespace storm {
}
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> transitionMatrix, std::vector<T> targetProbVector, BitVector initialStates)
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> const& transitionMatrix, std::vector<T> const& targetProbVector, BitVector const& initialStates)
: ShortestPathsGenerator<T>(transitionMatrix, vectorToMap(targetProbVector), initialStates) {}
// extracts the relevant info from the model and delegates to ctor above
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index 1cda2eb99..67e857e5d 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -67,8 +67,8 @@ namespace storm {
// a further alternative: use transition matrix of maybe-states
// combined with target vector (e.g., the instantiated matrix/vector from SamplingModel);
// in this case separately specifying a target makes no sense
- ShortestPathsGenerator(storage::SparseMatrix<T> transitionMatrix, std::vector<T> targetProbVector, BitVector initialStates);
- ShortestPathsGenerator(storage::SparseMatrix<T> maybeTransitionMatrix, std::unordered_map<state_t, T> targetProbMap, BitVector initialStates);
+ ShortestPathsGenerator(storage::SparseMatrix<T> const& transitionMatrix, std::vector<T> const& targetProbVector, BitVector const& initialStates);
+ ShortestPathsGenerator(storage::SparseMatrix<T> const& maybeTransitionMatrix, std::unordered_map<state_t, T> const& targetProbMap, BitVector const& initialStates);
inline ~ShortestPathsGenerator(){}
@@ -97,7 +97,7 @@ namespace storm {
private:
- storage::SparseMatrix<T> transitionMatrix;
+ storage::SparseMatrix<T> const& transitionMatrix; // FIXME: store reference instead (?)
state_t numStates; // includes meta-target, i.e. states in model + 1
state_t metaTarget;
BitVector initialStates;
From 4bc92664167fdbc8fa6c3d480889fbe4f04289bf Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 12 Feb 2016 20:29:27 +0100
Subject: [PATCH 10/13] redundant namespace refs rm
---
src/utility/shortestPaths.cpp | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index 8d1dd079f..dda452d5a 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -128,8 +128,8 @@ namespace storm {
// the existing Dijkstra isn't working anyway AND
// doesn't fully meet our requirements, so let's roll our own
- T inftyDistance = utility::zero<T>();
- T zeroDistance = utility::one<T>();
+ T inftyDistance = zero<T>();
+ T zeroDistance = one<T>();
shortestPathDistances.resize(numStates, inftyDistance);
shortestPathPredecessors.resize(numStates, boost::optional<state_t>());
@@ -232,7 +232,7 @@ namespace storm {
// there is no such edge
// let's disallow that for now, because I'm not expecting it to happen
assert(false);
- return utility::zero<T>();
+ return zero<T>();
} else {
// edge must be "virtual edge" to meta-target
assert(isMetaTargetPredecessor(tailNode));
From fe6804e16426e80b9a718f091a24210e7d5ba835 Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 18 Nov 2016 16:52:07 +0100
Subject: [PATCH 11/13] KSP: matrix format conversion & lots of type stuff
# Conflicts:
# src/python/storm-tom.cpp
# src/utility/shortestPaths.cpp
# src/utility/shortestPaths.h
# test/functional/utility/KSPTest.cpp
# test/functional/utility/PdtmcInstantiationTest.cpp
---
src/utility/shortestPaths.cpp | 32 +++++++------
src/utility/shortestPaths.h | 69 ++++++++++++++++++++++-------
test/functional/utility/KSPTest.cpp | 16 +++----
3 files changed, 79 insertions(+), 38 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index dda452d5a..ad25e2616 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -7,12 +7,16 @@ namespace storm {
namespace utility {
namespace ksp {
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> const& transitionMatrix, std::unordered_map<state_t, T> const& targetProbMap, BitVector const& initialStates) :
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> const& transitionMatrix,
+ std::unordered_map<state_t, T> const& targetProbMap,
+ BitVector const& initialStates,
+ MatrixFormat matrixFormat) :
transitionMatrix(transitionMatrix),
numStates(transitionMatrix.getColumnCount() + 1), // one more for meta-target
metaTarget(transitionMatrix.getColumnCount()), // first unused state index
initialStates(initialStates),
- targetProbMap(targetProbMap) {
+ targetProbMap(targetProbMap),
+ matrixFormat(matrixFormat) {
computePredecessors();
@@ -28,28 +32,29 @@ namespace storm {
}
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> const& transitionMatrix, std::vector<T> const& targetProbVector, BitVector const& initialStates)
- : ShortestPathsGenerator<T>(transitionMatrix, vectorToMap(targetProbVector), initialStates) {}
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(storage::SparseMatrix<T> const& transitionMatrix,
+ std::vector<T> const& targetProbVector, BitVector const& initialStates, MatrixFormat matrixFormat)
+ : ShortestPathsGenerator<T>(transitionMatrix, vectorToMap(targetProbVector), initialStates, matrixFormat) {}
// extracts the relevant info from the model and delegates to ctor above
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, BitVector const& targetBV)
- : ShortestPathsGenerator<T>(model->getTransitionMatrix(), allProbOneMap(targetBV), model->getInitialStates()) {}
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(Model const& model, BitVector const& targetBV)
+ : ShortestPathsGenerator<T>(model.getTransitionMatrix(), allProbOneMap(targetBV), model.getInitialStates(), MatrixFormat::straight) {}
// several alternative ways to specify the targets are provided,
// each converts the targets and delegates to the ctor above
// I admit it's kind of ugly, but actually pretty convenient (and I've wanted to try C++11 delegation)
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, state_t singleTarget)
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(Model const& model, state_t singleTarget)
: ShortestPathsGenerator<T>(model, std::vector<state_t>{singleTarget}) {}
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::vector<state_t> const& targetList)
- : ShortestPathsGenerator<T>(model, BitVector(model->getNumberOfStates(), targetList)) {}
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(Model const& model, std::vector<state_t> const& targetList)
+ : ShortestPathsGenerator<T>(model, BitVector(model.getNumberOfStates(), targetList)) {}
template <typename T>
- ShortestPathsGenerator<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::string const& targetLabel)
- : ShortestPathsGenerator<T>(model, model->getStates(targetLabel)) {}
+ ShortestPathsGenerator<T>::ShortestPathsGenerator(Model const& model, std::string const& targetLabel)
+ : ShortestPathsGenerator<T>(model, model.getStates(targetLabel)) {}
template <typename T>
T ShortestPathsGenerator<T>::getDistance(unsigned long k) {
@@ -152,7 +157,8 @@ namespace storm {
state_t otherNode = transition.getColumn();
// note that distances are probabilities, thus they are multiplied and larger is better
- T alternateDistance = shortestPathDistances[currentNode] * transition.getValue();
+ T alternateDistance = shortestPathDistances[currentNode] * convertDistance(currentNode, otherNode, transition.getValue());
+ assert(zero<T>() <= alternateDistance <= one<T>()); // FIXME: there is a negative transition! SM gives us a placeholder!
if (alternateDistance > shortestPathDistances[otherNode]) {
shortestPathDistances[otherNode] = alternateDistance;
shortestPathPredecessors[otherNode] = boost::optional<state_t>(currentNode);
@@ -225,7 +231,7 @@ namespace storm {
for (auto const& transition : transitionMatrix.getRowGroup(tailNode)) {
if (transition.getColumn() == headNode) {
- return transition.getValue();
+ return convertDistance(tailNode, headNode, transition.getValue());
}
}
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index 67e857e5d..fb1e0303c 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -23,9 +23,11 @@
namespace storm {
namespace utility {
namespace ksp {
- typedef storage::sparse::state_type state_t;
+ using state_t = storage::sparse::state_type;
+ using OrderedStateList = std::vector<state_t>;
using BitVector = storage::BitVector;
- typedef std::vector<state_t> ordered_state_list_t;
+
+ // -- helper structs/classes -----------------------------------------------------------------------------
template <typename T>
struct Path {
@@ -46,29 +48,38 @@ namespace storm {
}
};
+ // when using the raw matrix/vector invocation, this enum parameter
+ // forces the caller to declare whether the matrix has the evil I-P
+ // format, which requires back-conversion of the entries
+ enum class MatrixFormat { straight, iMinusP };
+
// -------------------------------------------------------------------------------------------------------
template <typename T>
class ShortestPathsGenerator {
public:
+ using Matrix = storage::SparseMatrix<T>;
+ using StateProbMap = std::unordered_map<state_t, T>;
+ using Model = models::sparse::Model<T>;
+
/*!
* Performs precomputations (including meta-target insertion and Dijkstra).
* Modifications are done locally, `model` remains unchanged.
* Target (group) cannot be changed.
*/
- ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, BitVector const& targetBV);
+ ShortestPathsGenerator(Model const& model, BitVector const& targetBV);
// allow alternative ways of specifying the target,
// all of which will be converted to BitVector and delegated to constructor above
- ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, state_t singleTarget);
- ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::vector<state_t> const& targetList);
- ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model, std::string const& targetLabel = "target");
+ ShortestPathsGenerator(Model const& model, state_t singleTarget);
+ ShortestPathsGenerator(Model const& model, std::vector<state_t> const& targetList);
+ ShortestPathsGenerator(Model const& model, std::string const& targetLabel = "target");
// a further alternative: use transition matrix of maybe-states
// combined with target vector (e.g., the instantiated matrix/vector from SamplingModel);
// in this case separately specifying a target makes no sense
- ShortestPathsGenerator(storage::SparseMatrix<T> const& transitionMatrix, std::vector<T> const& targetProbVector, BitVector const& initialStates);
- ShortestPathsGenerator(storage::SparseMatrix<T> const& maybeTransitionMatrix, std::unordered_map<state_t, T> const& targetProbMap, BitVector const& initialStates);
+ ShortestPathsGenerator(Matrix const& transitionMatrix, std::vector<T> const& targetProbVector, BitVector const& initialStates, MatrixFormat matrixFormat);
+ ShortestPathsGenerator(Matrix const& maybeTransitionMatrix, StateProbMap const& targetProbMap, BitVector const& initialStates, MatrixFormat matrixFormat);
inline ~ShortestPathsGenerator(){}
@@ -93,19 +104,21 @@ namespace storm {
* Computes KSP if not yet computed.
* @throws std::invalid_argument if no such k-shortest path exists
*/
- ordered_state_list_t getPathAsList(unsigned long k);
+ OrderedStateList getPathAsList(unsigned long k);
private:
- storage::SparseMatrix<T> const& transitionMatrix; // FIXME: store reference instead (?)
+ Matrix const& transitionMatrix; // FIXME: store reference instead (?)
state_t numStates; // includes meta-target, i.e. states in model + 1
state_t metaTarget;
BitVector initialStates;
- std::unordered_map<state_t, T> targetProbMap;
+ StateProbMap targetProbMap;
+
+ MatrixFormat matrixFormat;
- std::vector<ordered_state_list_t> graphPredecessors;
+ std::vector<OrderedStateList> graphPredecessors;
std::vector<boost::optional<state_t>> shortestPathPredecessors;
- std::vector<ordered_state_list_t> shortestPathSuccessors;
+ std::vector<OrderedStateList> shortestPathSuccessors;
std::vector<T> shortestPathDistances;
std::vector<std::vector<Path<T>>> kShortestPaths;
@@ -163,6 +176,7 @@ namespace storm {
// --- tiny helper fcts ---
+
inline bool isInitialState(state_t node) const {
return find(initialStates.begin(), initialStates.end(), node) != initialStates.end();
}
@@ -171,25 +185,45 @@ namespace storm {
return targetProbMap.count(node) == 1;
}
- /**
+ // I dislike this. But it is necessary if we want to handle those ugly I-P matrices
+ inline T convertDistance(state_t tailNode, state_t headNode, T distance) const {
+ if (matrixFormat == MatrixFormat::straight) {
+ return distance;
+ } else {
+ if (tailNode == headNode) {
+ // diagonal: 1-p = dist
+ return one<T>() - distance;
+ } else {
+ // non-diag: -p = dist
+ return zero<T>() - distance;
+ }
+ }
+ }
+
+ /*!
* Returns a map where each state of the input BitVector is mapped to 1 (`one<T>`).
*/
- inline std::unordered_map<state_t, T> allProbOneMap(BitVector bitVector) const {
- std::unordered_map<state_t, T> stateProbMap;
+ inline StateProbMap allProbOneMap(BitVector bitVector) const {
+ StateProbMap stateProbMap;
for (state_t node : bitVector) {
stateProbMap.emplace(node, one<T>()); // FIXME check rvalue warning (here and below)
}
return stateProbMap;
}
+ /*!
+ * Given a vector of probabilities so that the `i`th entry corresponds to the
+ * probability of state `i`, returns an equivalent map of only the non-zero entries.
+ */
inline std::unordered_map<state_t, T> vectorToMap(std::vector<T> probVector) const {
assert(probVector.size() == numStates);
std::unordered_map<state_t, T> stateProbMap;
- // non-zero entries (i.e. true transitions) are added to the map
for (state_t i = 0; i < probVector.size(); i++) {
T probEntry = probVector[i];
+
+ // only non-zero entries (i.e. true transitions) are added to the map
if (probEntry != 0) {
assert(0 < probEntry <= 1);
stateProbMap.emplace(i, probEntry);
@@ -198,6 +232,7 @@ namespace storm {
return stateProbMap;
}
+
// -----------------------
};
}
diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp
index d1c9a2f8f..2389f3f1c 100644
--- a/test/functional/utility/KSPTest.cpp
+++ b/test/functional/utility/KSPTest.cpp
@@ -26,7 +26,7 @@ TEST(KSPTest, dijkstra) {
auto model = buildExampleModel();
storm::utility::ksp::state_t testState = 300;
- storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
+ storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
double dist = spg.getDistance(1);
EXPECT_DOUBLE_EQ(0.015859334652581887, dist);
@@ -36,7 +36,7 @@ TEST(KSPTest, singleTarget) {
auto model = buildExampleModel();
storm::utility::ksp::state_t testState = 300;
- storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
+ storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
double dist = spg.getDistance(100);
EXPECT_DOUBLE_EQ(1.5231305000339649e-06, dist);
@@ -46,7 +46,7 @@ TEST(KSPTest, reentry) {
auto model = buildExampleModel();
storm::utility::ksp::state_t testState = 300;
- storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
+ storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
double dist = spg.getDistance(100);
EXPECT_DOUBLE_EQ(1.5231305000339649e-06, dist);
@@ -60,7 +60,7 @@ TEST(KSPTest, groupTarget) {
auto model = buildExampleModel();
auto groupTarget = std::vector<storm::utility::ksp::state_t>{50, 90};
- auto spg = storm::utility::ksp::ShortestPathsGenerator<double>(model, groupTarget);
+ auto spg = storm::utility::ksp::ShortestPathsGenerator<double>(*model, groupTarget);
// this path should lead to 90
double dist1 = spg.getDistance(8);
@@ -79,7 +79,7 @@ TEST(KSPTest, kTooLargeException) {
auto model = buildExampleModel();
storm::utility::ksp::state_t testState = 1;
- storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
+ storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
ASSERT_THROW(spg.getDistance(2), std::invalid_argument);
}
@@ -88,7 +88,7 @@ TEST(KSPTest, kspStateSet) {
auto model = buildExampleModel();
storm::utility::ksp::state_t testState = 300;
- storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
+ storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
storm::storage::BitVector referenceBV(model->getNumberOfStates(), false);
for (auto s : std::vector<storm::utility::ksp::state_t>{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}) {
@@ -104,10 +104,10 @@ TEST(KSPTest, kspPathAsList) {
auto model = buildExampleModel();
storm::utility::ksp::state_t testState = 300;
- storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
+ storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
// TODO: use path that actually has a loop or something to make this more interesting
- auto reference = storm::utility::ksp::ordered_state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0};
+ auto reference = storm::utility::ksp::OrderedStateList{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0};
auto list = spg.getPathAsList(7);
EXPECT_EQ(list, reference);
From 83445f67c319aaadd3bfb7fdc98f9b2a43164856 Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 18 Nov 2016 16:55:05 +0100
Subject: [PATCH 12/13] kSP: a few more comments
---
src/utility/shortestPaths.cpp | 29 ++++++++++++++++++++++++-----
src/utility/shortestPaths.md | 10 +++++++---
2 files changed, 31 insertions(+), 8 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index ad25e2616..2a7c21285 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -1,8 +1,16 @@
#include <queue>
#include <set>
+#include <string>
+
+#include "macros.h"
#include "shortestPaths.h"
#include "graph.h"
+// FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required!
+// Accessing zero should trigger a warning!
+// (Also, did I document this? I think so, somewhere. I went with k>=1 because
+// that's what the KSP paper used, but in retrospect k>=0 seems more intuitive ...)
+
namespace storm {
namespace utility {
namespace ksp {
@@ -249,9 +257,13 @@ namespace storm {
template <typename T>
void ShortestPathsGenerator<T>::computeNextPath(state_t node, unsigned long k) {
+ assert(k >= 2); // Dijkstra is used for k=1
assert(kShortestPaths[node].size() == k - 1); // if not, the previous SP must not exist
+ // TODO: I could extract the candidate generation to make this function more succinct
if (k == 2) {
+ // Step B.1 in J&M paper
+
Path<T> shortestPathToNode = kShortestPaths[node][1 - 1]; // never forget index shift :-|
for (state_t predecessor : graphPredecessors[node]) {
@@ -271,7 +283,9 @@ namespace storm {
}
}
- if (k > 2 || !isInitialState(node)) {
+ if (not (k == 2 && isInitialState(node))) {
+ // Steps B.2-5 in J&M paper
+
// the (k-1)th shortest path (i.e., one better than the one we want to compute)
Path<T> previousShortestPath = kShortestPaths[node][k - 1 - 1]; // oh god, I forgot index shift AGAIN
@@ -297,9 +311,10 @@ namespace storm {
};
candidatePaths[node].insert(pathToPredecessorPlusEdge);
}
- // else there was no path; TODO: does this need handling?
+ // else there was no path; TODO: does this need handling? -- yes, but not here (because the step B.1 may have added candidates)
}
+ // Step B.6 in J&M paper
if (!candidatePaths[node].empty()) {
Path<T> minDistanceCandidate = *(candidatePaths[node].begin());
for (auto path : candidatePaths[node]) {
@@ -310,6 +325,9 @@ namespace storm {
candidatePaths[node].erase(std::find(candidatePaths[node].begin(), candidatePaths[node].end(), minDistanceCandidate));
kShortestPaths[node].push_back(minDistanceCandidate);
+ } else {
+ // TODO: kSP does not exist. this is handled later, but it would be nice to catch it as early as possble, wouldn't it?
+ STORM_LOG_TRACE("KSP: no candidates, this will trigger nonexisting ksp after exiting these recursions. TODO: handle here");
}
}
@@ -320,9 +338,10 @@ namespace storm {
for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) {
computeNextPath(metaTarget, nextK);
if (kShortestPaths[metaTarget].size() < nextK) {
- //std::cout << std::endl << "--> DEBUG: Last path: k=" << (nextK - 1) << ":" << std::endl;
- //printKShortestPath(metaTarget, nextK - 1);
- //std::cout << "---------" << "No other path exists!" << std::endl;
+ unsigned long lastExistingK = nextK - 1;
+ STORM_LOG_DEBUG("KSP throws (as expected) due to nonexistence -- maybe this is unhandled and causes the Python interface to segfault?");
+ STORM_LOG_DEBUG("last existing k-SP has k=" + std::to_string(lastExistingK));
+ STORM_LOG_DEBUG("maybe this is unhandled and causes the Python interface to segfault?");
throw std::invalid_argument("k-SP does not exist for k=" + std::to_string(k));
}
}
diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md
index f2beb801a..13dc96376 100644
--- a/src/utility/shortestPaths.md
+++ b/src/utility/shortestPaths.md
@@ -75,7 +75,7 @@ This is a common feature if the target state is a sink; but we are not
interested in such paths.
(In fact, ideally we'd like to see paths whose node-intersection with all
-shorter paths is non-empty (which is an even stronger statement than
+shorter paths is non-empty [^2] (which is an even stronger statement than
loop-free-ness of paths), because we want to take a union of those node
sets. But that's a different matter.)
@@ -97,7 +97,7 @@ path to some node `u` plus an edge to `t`:
Further, the shortest paths to some node are always computed in order and
without gaps, e.g., the 1, 2, 3-shortest paths to `t` will be computed
before the 4-SP. Thus, we store the SPs in a linked list for each node,
-with the k-th entry[^2] being the k-th SP to that node.
+with the k-th entry[^3] being the k-th SP to that node.
Thus for an SP as shown above we simply store the predecessor node (`u`)
and the `k`, which allows us to look up the tail of the SP.
@@ -107,4 +107,8 @@ the entire path back-to-front.
[^1]: I suppose the correct term would now be "meta-target predecessors".
In fact, I will rename all occurences of `target` in the source to
`metaTargetPredecessors` – clumsy but accurate.
-[^2]: Which due to 0-based indexing has index `k-1`, of course! Damn it.
+[^2]: (2016-08-20:) Is this correct? Didn't I mean that the path should
+ contain new nodes, i.e., non-emptiness of
+ ((nodes in path) set-minus (union(nodes in shorter paths)))?
+ Yeah, I'm pretty sure that's what I meant.
+[^3]: Which due to 0-based indexing has index `k-1`, of course! Damn it.
From 0c6574c740284aff812a7a9d538126202299190a Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 18 Nov 2016 16:58:18 +0100
Subject: [PATCH 13/13] rm questionable assertion
---
src/utility/shortestPaths.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index fb1e0303c..2ffdcc13a 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -216,7 +216,7 @@ namespace storm {
* probability of state `i`, returns an equivalent map of only the non-zero entries.
*/
inline std::unordered_map<state_t, T> vectorToMap(std::vector<T> probVector) const {
- assert(probVector.size() == numStates);
+ //assert(probVector.size() == numStates); // numStates may not yet be initialized! // still true?
std::unordered_map<state_t, T> stateProbMap;