diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index ac868070d..2a7c21285 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -1,20 +1,30 @@ #include #include +#include + +#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 { template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> 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 - targetSet = std::unordered_set(targets.begin(), targets.end()); + ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix const& transitionMatrix, + std::unordered_map 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), + matrixFormat(matrixFormat) { computePredecessors(); @@ -29,20 +39,30 @@ namespace storm { candidatePaths.resize(numStates); } + template + ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix const& transitionMatrix, + std::vector const& targetProbVector, BitVector const& initialStates, MatrixFormat matrixFormat) + : ShortestPathsGenerator(transitionMatrix, vectorToMap(targetProbVector), initialStates, matrixFormat) {} + + // extracts the relevant info from the model and delegates to ctor above + template + ShortestPathsGenerator::ShortestPathsGenerator(Model const& model, BitVector const& targetBV) + : ShortestPathsGenerator(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 - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, - state_t singleTarget) : ShortestPathsGenerator(model, std::vector{singleTarget}) {} + ShortestPathsGenerator::ShortestPathsGenerator(Model const& model, state_t singleTarget) + : ShortestPathsGenerator(model, std::vector{singleTarget}) {} template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, - storage::BitVector const& targetBV) : ShortestPathsGenerator(model, bitvectorToList(targetBV)) {} + ShortestPathsGenerator::ShortestPathsGenerator(Model const& model, std::vector const& targetList) + : ShortestPathsGenerator(model, BitVector(model.getNumberOfStates(), targetList)) {} template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, - std::string const& targetLabel) : ShortestPathsGenerator(model, bitvectorToList(model->getStates(targetLabel))) {} + ShortestPathsGenerator::ShortestPathsGenerator(Model const& model, std::string const& targetLabel) + : ShortestPathsGenerator(model, model.getStates(targetLabel)) {} template T ShortestPathsGenerator::getDistance(unsigned long k) { @@ -51,9 +71,9 @@ namespace storm { } template - storage::BitVector ShortestPathsGenerator::getStates(unsigned long k) { + BitVector ShortestPathsGenerator::getStates(unsigned long k) { computeKSP(k); - storage::BitVector stateSet(numStates - 1, false); // no meta-target + BitVector stateSet(numStates - 1, false); // no meta-target Path currentPath = kShortestPaths[metaTarget][k - 1]; boost::optional maybePredecessor = currentPath.predecessorNode; @@ -71,10 +91,10 @@ namespace storm { } template - state_list_t ShortestPathsGenerator::getPathAsList(unsigned long k) { + std::vector ShortestPathsGenerator::getPathAsList(unsigned long k) { computeKSP(k); - state_list_t backToFrontList; + std::vector backToFrontList; Path currentPath = kShortestPaths[metaTarget][k - 1]; boost::optional maybePredecessor = currentPath.predecessorNode; @@ -100,16 +120,20 @@ 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 (std::find(targets.begin(), targets.end(), i) == targets.end()) { + if (!isMetaTargetPredecessor(i)) { graphPredecessors[transition.getColumn()].push_back(i); } } } - // meta-target has exactly the target states as predecessors - graphPredecessors[metaTarget] = targets; + // 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); + } } template @@ -117,8 +141,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 zeroDistance = utility::one(); + T inftyDistance = zero(); + T zeroDistance = one(); shortestPathDistances.resize(numStates, inftyDistance); shortestPathPredecessors.resize(numStates, boost::optional()); @@ -126,7 +150,7 @@ namespace storm { // default comparison on pair actually works fine if distance is the first entry std::set, std::greater>> dijkstraQueue; - for (state_t initialState : model->getInitialStates()) { + for (state_t initialState : initialStates) { shortestPathDistances[initialState] = zeroDistance; dijkstraQueue.emplace(zeroDistance, initialState); } @@ -135,13 +159,14 @@ namespace storm { state_t currentNode = (*dijkstraQueue.begin()).second; dijkstraQueue.erase(dijkstraQueue.begin()); - if (targetSet.count(currentNode) == 0) { + if (!isMetaTargetPredecessor(currentNode)) { // non-target node, treated normally for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) { 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() <= alternateDistance <= one()); // FIXME: there is a negative transition! SM gives us a placeholder! if (alternateDistance > shortestPathDistances[otherNode]) { shortestPathDistances[otherNode] = alternateDistance; shortestPathPredecessors[otherNode] = boost::optional(currentNode); @@ -149,9 +174,9 @@ namespace storm { } } } else { - // target node has only "virtual edge" (with prob 1) to meta-target - // no multiplication necessary - T alternateDistance = shortestPathDistances[currentNode]; + // 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(currentNode); @@ -179,7 +204,7 @@ namespace storm { // BFS in Dijkstra-SP order std::queue bfsQueue; - for (state_t initialState : model->getInitialStates()) { + for (state_t initialState : initialStates) { bfsQueue.push(initialState); } @@ -214,27 +239,31 @@ namespace storm { for (auto const& transition : transitionMatrix.getRowGroup(tailNode)) { if (transition.getColumn() == headNode) { - return transition.getValue(); + return convertDistance(tailNode, headNode, transition.getValue()); } } // there is no such edge // let's disallow that for now, because I'm not expecting it to happen assert(false); - return utility::zero(); + return zero(); } else { - // edge must be "virtual edge" from target state to meta-target - assert(targetSet.count(tailNode) == 1); - return utility::one(); + // edge must be "virtual edge" to meta-target + assert(isMetaTargetPredecessor(tailNode)); + return targetProbMap.at(tailNode); // FIXME double check } } template void ShortestPathsGenerator::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 shortestPathToNode = kShortestPaths[node][1 - 1]; // never forget index shift :-| for (state_t predecessor : graphPredecessors[node]) { @@ -254,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 previousShortestPath = kShortestPaths[node][k - 1 - 1]; // oh god, I forgot index shift AGAIN @@ -280,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 minDistanceCandidate = *(candidatePaths[node].begin()); for (auto path : candidatePaths[node]) { @@ -293,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"); } } @@ -303,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.h b/src/utility/shortestPaths.h index 8139f1c91..2ffdcc13a 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -12,20 +12,22 @@ // 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 is +// faster for storing predecessors etc. +// 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.) namespace storm { namespace utility { namespace ksp { - typedef storage::sparse::state_type state_t; - typedef std::vector state_list_t; + using state_t = storage::sparse::state_type; + using OrderedStateList = std::vector; + using BitVector = storage::BitVector; + + // -- helper structs/classes ----------------------------------------------------------------------------- template struct Path { @@ -46,24 +48,39 @@ 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 class ShortestPathsGenerator { public: + using Matrix = storage::SparseMatrix; + using StateProbMap = std::unordered_map; + using Model = models::sparse::Model; + /*! * Performs precomputations (including meta-target insertion and Dijkstra). * 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> model, state_list_t const& targets); + ShortestPathsGenerator(Model const& model, BitVector const& targetBV); // allow alternative ways of specifying the target, - // all of which will be converted to list and delegated to constructor above - ShortestPathsGenerator(std::shared_ptr> model, state_t singleTarget); - ShortestPathsGenerator(std::shared_ptr> model, storage::BitVector const& targetBV); - ShortestPathsGenerator(std::shared_ptr> model, std::string const& targetLabel); + // all of which will be converted to BitVector and delegated to constructor above + ShortestPathsGenerator(Model const& model, state_t singleTarget); + ShortestPathsGenerator(Model const& model, std::vector 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(Matrix const& transitionMatrix, std::vector const& targetProbVector, BitVector const& initialStates, MatrixFormat matrixFormat); + ShortestPathsGenerator(Matrix const& maybeTransitionMatrix, StateProbMap const& targetProbMap, BitVector const& initialStates, MatrixFormat matrixFormat); + inline ~ShortestPathsGenerator(){} @@ -87,21 +104,21 @@ 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); + OrderedStateList getPathAsList(unsigned long k); private: - std::shared_ptr> model; - storage::SparseMatrix transitionMatrix; + Matrix const& transitionMatrix; // FIXME: store reference instead (?) state_t numStates; // includes meta-target, i.e. states in model + 1 - - state_list_t targets; - std::unordered_set targetSet; state_t metaTarget; + BitVector initialStates; + StateProbMap targetProbMap; + + MatrixFormat matrixFormat; - std::vector graphPredecessors; + std::vector graphPredecessors; std::vector> shortestPathPredecessors; - std::vector shortestPathSuccessors; + std::vector shortestPathSuccessors; std::vector shortestPathDistances; std::vector>> kShortestPaths; @@ -159,18 +176,63 @@ 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(); } - 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 isMetaTargetPredecessor(state_t node) const { + 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() - distance; + } else { + // non-diag: -p = dist + return zero() - distance; + } } - return list; } + + /*! + * Returns a map where each state of the input BitVector is mapped to 1 (`one`). + */ + inline StateProbMap allProbOneMap(BitVector bitVector) const { + StateProbMap stateProbMap; + for (state_t node : bitVector) { + stateProbMap.emplace(node, one()); // 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 vectorToMap(std::vector probVector) const { + //assert(probVector.size() == numStates); // numStates may not yet be initialized! // still true? + + std::unordered_map stateProbMap; + + 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); + } + } + + return stateProbMap; + } + // ----------------------- }; } diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md index 61f6fe1e3..13dc96376 100644 --- a/src/utility/shortestPaths.md +++ b/src/utility/shortestPaths.md @@ -39,6 +39,27 @@ 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[^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 +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 @@ -54,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.) @@ -76,11 +97,18 @@ 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[^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. 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]: (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. diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index aba8747c3..2389f3f1c 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -25,8 +25,8 @@ std::shared_ptr> buildExampleModel() { TEST(KSPTest, dijkstra) { auto model = buildExampleModel(); - storm::storage::sparse::state_type testState = 300; - storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::state_t testState = 300; + storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); double dist = spg.getDistance(1); EXPECT_DOUBLE_EQ(0.015859334652581887, dist); @@ -35,8 +35,8 @@ TEST(KSPTest, dijkstra) { TEST(KSPTest, singleTarget) { auto model = buildExampleModel(); - storm::storage::sparse::state_type testState = 300; - storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::state_t testState = 300; + storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); double dist = spg.getDistance(100); EXPECT_DOUBLE_EQ(1.5231305000339649e-06, dist); @@ -45,8 +45,8 @@ TEST(KSPTest, singleTarget) { TEST(KSPTest, reentry) { auto model = buildExampleModel(); - storm::storage::sparse::state_type testState = 300; - storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::state_t testState = 300; + storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); double dist = spg.getDistance(100); EXPECT_DOUBLE_EQ(1.5231305000339649e-06, dist); @@ -59,8 +59,8 @@ TEST(KSPTest, reentry) { TEST(KSPTest, groupTarget) { auto model = buildExampleModel(); - auto groupTarget = storm::utility::ksp::state_list_t{50, 90}; - auto spg = storm::utility::ksp::ShortestPathsGenerator(model, groupTarget); + auto groupTarget = std::vector{50, 90}; + auto spg = storm::utility::ksp::ShortestPathsGenerator(*model, groupTarget); // this path should lead to 90 double dist1 = spg.getDistance(8); @@ -78,8 +78,8 @@ TEST(KSPTest, groupTarget) { TEST(KSPTest, kTooLargeException) { auto model = buildExampleModel(); - storm::storage::sparse::state_type testState = 1; - storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::state_t testState = 1; + storm::utility::ksp::ShortestPathsGenerator 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::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::state_t testState = 300; + storm::utility::ksp::ShortestPathsGenerator 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{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::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::state_t testState = 300; + storm::utility::ksp::ShortestPathsGenerator 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 = 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);