From 102f38322d6a65922d38bd68f79dd2a441523681 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 17 Mar 2013 17:42:45 +0100 Subject: [PATCH] Fixed several bugs in several modules (bit vector, parser, etc.). Topological value iteration now works for the consensus protocol and the two dice example. --- ...ogicalValueIterationMdpPrctlModelChecker.h | 47 +++++++----- src/models/GraphTransitions.h | 28 ++++--- ...NondeterministicSparseTransitionParser.cpp | 4 +- src/storage/BitVector.h | 2 +- src/storage/SparseMatrix.h | 6 -- src/utility/GraphAnalyzer.h | 75 +++++++++++++++++-- src/utility/Vector.h | 48 ++++++++++++ 7 files changed, 164 insertions(+), 46 deletions(-) diff --git a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h index 80a4e2049..23b1ac6fc 100644 --- a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h @@ -67,47 +67,56 @@ private: storm::models::GraphTransitions stronglyConnectedComponentsDependencyGraph; storm::utility::GraphAnalyzer::performSccDecomposition(matrix, nondeterministicChoiceIndices, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + std::vector topologicalSort; + storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph, topologicalSort); + // Set up the environment for the power method. std::vector multiplyResult(matrix.getRowCount()); std::vector* currentX = &x; std::vector* newX = new std::vector(x.size()); std::vector* swap = nullptr; - uint_fast64_t iterations = 0; - bool converged = false; + uint_fast64_t currentMaxLocalIterations = 0; + uint_fast64_t localIterations = 0; + uint_fast64_t globalIterations = 0; + bool converged = true; - /* - for (auto sccIt = stronglyConnectedComponents.rbegin(), sccIte = stronglyConnectedComponents.rend(); sccIt != sccIte; ++sccIt) { - converged = false; + for (auto sccIndexIt = topologicalSort.begin(); sccIndexIt != topologicalSort.end() && converged; ++sccIndexIt) { + std::vector const& scc = stronglyConnectedComponents[*sccIndexIt]; - std::cout << "for scc! " << *sccIt << std::endl; - while (!converged && iterations < maxIterations) { - std::cout << "first line " << std::endl; + localIterations = 0; + converged = false; + while (!converged && localIterations < maxIterations) { // Compute x' = A*x + b. - matrix.multiplyWithVector(**sccIt, nondeterministicChoiceIndices, *currentX, multiplyResult); - std::cout << "after mult" << std::endl; - storm::utility::addVectors(**sccIt, nondeterministicChoiceIndices, multiplyResult, b); - std::cout << "after add " << std::endl; + matrix.multiplyWithVector(scc, nondeterministicChoiceIndices, *currentX, multiplyResult); + storm::utility::addVectors(scc, nondeterministicChoiceIndices, multiplyResult, b); // Reduce the vector x' by applying min/max for all non-deterministic choices. if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(multiplyResult, newX, nondeterministicChoiceIndices); + storm::utility::reduceVectorMin(multiplyResult, newX, scc, nondeterministicChoiceIndices); } else { - storm::utility::reduceVectorMax(multiplyResult, newX, nondeterministicChoiceIndices); + storm::utility::reduceVectorMax(multiplyResult, newX, scc, nondeterministicChoiceIndices); } - std::cout << "comp" << std::endl; // Determine whether the method converged. + // converged = storm::utility::equalModuloPrecision(*currentX, *newX, scc, precision, relative); converged = storm::utility::equalModuloPrecision(*currentX, *newX, precision, relative); // Update environment variables. swap = currentX; currentX = newX; newX = swap; - ++iterations; + ++localIterations; + ++globalIterations; + } + + std::cout << "converged locally for scc of size " << scc.size() << std::endl; + + if (localIterations > currentMaxLocalIterations) { + currentMaxLocalIterations = localIterations; } } - if (iterations % 2 == 1) { + if (globalIterations % 2 == 1) { std::swap(x, *currentX); delete currentX; } else { @@ -116,12 +125,10 @@ private: // Check if the solver converged and issue a warning otherwise. if (converged) { - LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations."); + LOG4CPLUS_INFO(logger, "Iterative solver converged after " << currentMaxLocalIterations << " iterations."); } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); } - - */ } }; diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 359fcfcf2..ec8bb2bfd 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -99,13 +99,21 @@ public: return result; } + uint_fast64_t getNumberOfStates() const { + return numberOfStates; + } + + uint_fast64_t getNumberOfTransitions() const { + return numberOfTransitions; + } + /*! * Returns an iterator to the successors of the given state. * @param state The state for which to get the successor iterator. * @return An iterator to the predecessors of the given states. */ stateSuccessorIterator beginStateSuccessorsIterator(uint_fast64_t state) const { - return &this->successorList[this->stateIndications[state]]; + return &(this->successorList[0]) + this->stateIndications[state]; } /*! @@ -116,12 +124,7 @@ public: * the given state. */ stateSuccessorIterator endStateSuccessorsIterator(uint_fast64_t state) const { - std::cout << "size: " << this->stateIndications.size() << std::endl; - std::cout << "idx accessed " << state << std::endl; - std::cout << this->stateIndications[state + 1] << std::endl; - std::cout << "other size: " << this->successorList.size() << std::endl; - std::cout << this->successorList[this->stateIndications[state + 1]] << std::endl; - return &this->successorList[this->stateIndications[state + 1]]; + return &(this->successorList[0]) + this->stateIndications[state + 1]; } /*! @@ -130,8 +133,11 @@ public: */ std::string toString() const { std::stringstream stream; - stream << successorList << std::endl; - stream << stateIndications << std::endl; + for (uint_fast64_t state = 0; state < numberOfStates; ++state) { + for (auto succIt = this->beginStateSuccessorsIterator(state), succIte = this->endStateSuccessorsIterator(state); succIt != succIte; ++succIt) { + stream << state << " -> " << *succIt << std::endl; + } + } return stream.str(); } @@ -147,7 +153,7 @@ private: // Now, we determine the SCCs which are reachable (in one step) from the current SCC. std::set allTargetSccs; for (auto state : scc) { - for (stateSuccessorIterator succIt = beginStateSuccessorsIterator(state), succIte = endStateSuccessorsIterator(state); succIt != succIte; ++succIt) { + for (stateSuccessorIterator succIt = transitions.beginStateSuccessorsIterator(state), succIte = transitions.endStateSuccessorsIterator(state); succIt != succIte; ++succIt) { uint_fast64_t targetScc = stateToSccMap.find(*succIt)->second; // We only need to consider transitions that are actually leaving the SCC. @@ -166,8 +172,6 @@ private: // Put the sentinel element at the end and initialize the number of transitions. stateIndications[numberOfStates] = successorList.size(); numberOfTransitions = successorList.size(); - - std::cout << this->toString() << std::endl; } /*! diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 4d9491ce1..c0bf308b9 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -337,7 +337,9 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s buf = trimWhitespaces(buf); } - this->rowMapping->at(maxnode+1) = curRow + 1; + for (int_fast64_t node = lastsource + 1; node <= maxnode + 1; node++) { + this->rowMapping->at(node) = curRow + 1; + } if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 0080fa2af..570283c4d 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -137,7 +137,7 @@ public: * @param bv A reference to the bit vector to be copied. */ BitVector(BitVector const& bv) : bucketCount(bv.bucketCount), bitCount(bv.bitCount), endIterator(*this, bitCount, bitCount, false), truncateMask((1ll << (bitCount & mod64mask)) - 1ll) { - LOG4CPLUS_WARN(logger, "Invoking copy constructor."); + LOG4CPLUS_DEBUG(logger, "Invoking copy constructor."); bucketArray = new uint64_t[bucketCount]; std::copy(bv.bucketArray, bv.bucketArray + this->bucketCount, this->bucketArray); } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 5cab2deb3..afdb0ea5b 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -834,13 +834,7 @@ public: constRowsIterator rowsIt = this->constRowsIteratorBegin(); uint_fast64_t nextRow = 1; - std::cout << nondeterministicChoiceIndices << std::endl; - std::cout << rowCount << std::endl; - for (auto stateIt = states.cbegin(), stateIte = states.cend(); stateIt != stateIte; ++stateIt) { - std::cout << "stateIt " << *stateIt << std::endl; - std::cout << nondeterministicChoiceIndices[*stateIt] << std::endl; - std::cout << this->rowIndications[nondeterministicChoiceIndices[*stateIt]] << std::endl; rowsIt.setOffset(this->rowIndications[nondeterministicChoiceIndices[*stateIt]]); nextRow = nondeterministicChoiceIndices[*stateIt] + 1; for (auto rowIt = nondeterministicChoiceIndices[*stateIt], rowIte = nondeterministicChoiceIndices[*stateIt + 1]; rowIt != rowIte; ++rowIt, ++nextRow) { diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 7321926cf..f99c3e319 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -424,11 +424,72 @@ public: storm::models::GraphTransitions forwardTransitions(matrix, nondeterministicChoiceIndices, true); // Perform the actual SCC decomposition based on the graph-transitions of the system. - performSccDecomposition(nondeterministicChoiceIndices.size(), forwardTransitions, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + performSccDecomposition(nondeterministicChoiceIndices.size() - 1, forwardTransitions, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); LOG4CPLUS_INFO(logger, "Done computing SCC decomposition."); } + template + static void getTopologicalSort(storm::models::GraphTransitions const& transitions, std::vector& topologicalSort) { + topologicalSort.reserve(transitions.getNumberOfStates()); + + std::vector recursionStack; + recursionStack.reserve(transitions.getNumberOfStates()); + + std::vector::stateSuccessorIterator> iteratorRecursionStack; + iteratorRecursionStack.reserve(transitions.getNumberOfStates()); + + storm::storage::BitVector visitedStates(transitions.getNumberOfStates()); + for (uint_fast64_t state = 0; state < transitions.getNumberOfStates(); ++state) { + if (!visitedStates.get(state)) { + recursionStack.push_back(state); + iteratorRecursionStack.push_back(transitions.beginStateSuccessorsIterator(state)); + + recursionStepForward: + while (!recursionStack.empty()) { + uint_fast64_t currentState = recursionStack.back(); + typename storm::models::GraphTransitions::stateSuccessorIterator currentIt = iteratorRecursionStack.back(); + + visitedStates.set(currentState, true); + + recursionStepBackward: + for (; currentIt != transitions.endStateSuccessorsIterator(currentState); ++currentIt) { + if (!visitedStates.get(*currentIt)) { + // Put unvisited successor on top of our recursion stack and remember that. + recursionStack.push_back(*currentIt); + + // Save current iterator position so we can continue where we left off later. + iteratorRecursionStack.pop_back(); + iteratorRecursionStack.push_back(currentIt + 1); + + // Also, put initial value for iterator on corresponding recursion stack. + iteratorRecursionStack.push_back(transitions.beginStateSuccessorsIterator(*currentIt)); + + goto recursionStepForward; + } + } + + topologicalSort.push_back(currentState); + + // If we reach this point, we have completed the recursive descent for the current state. + // That is, we need to pop it from the recursion stacks. + recursionStack.pop_back(); + iteratorRecursionStack.pop_back(); + + // If there is at least one state under the current one in our recursion stack, we need + // to restore the topmost state as the current state and jump to the part after the + // original recursive call. + if (recursionStack.size() > 0) { + currentState = recursionStack.back(); + currentIt = iteratorRecursionStack.back(); + + goto recursionStepBackward; + } + } + } + } + } + private: template static void performSccDecomposition(uint_fast64_t numberOfStates, storm::models::GraphTransitions const& forwardTransitions, std::vector>& stronglyConnectedComponents, storm::models::GraphTransitions& stronglyConnectedComponentsDependencyGraph) { @@ -482,24 +543,26 @@ private: tarjanStackStates.set(currentState, true); // Now, traverse all successors of the current state. - recursionStepBackward: for(; currentIt != forwardTransitions.endStateSuccessorsIterator(currentState); ++currentIt) { // If we have not visited the successor already, we need to perform the procedure // recursively on the newly found state. if (!visitedStates.get(*currentIt)) { + // Save current iterator position so we can continue where we left off later. + recursionIteratorStack.pop_back(); + recursionIteratorStack.push_back(currentIt); + // Put unvisited successor on top of our recursion stack and remember that. recursionStateStack.push_back(*currentIt); statesInStack[*currentIt] = true; - // Save current iterator position so we can continue where we left off later. - recursionIteratorStack.pop_back(); - recursionIteratorStack.push_back(currentIt + 1); - // Also, put initial value for iterator on corresponding recursion stack. recursionIteratorStack.push_back(forwardTransitions.beginStateSuccessorsIterator(*currentIt)); // Perform the actual recursion step in an iterative way. goto recursionStepForward; + + recursionStepBackward: + lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*currentIt]); } else if (tarjanStackStates.get(*currentIt)) { // Update the lowlink of the current state. lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*currentIt]); diff --git a/src/utility/Vector.h b/src/utility/Vector.h index cdc7cd318..ab1fc461a 100644 --- a/src/utility/Vector.h +++ b/src/utility/Vector.h @@ -107,6 +107,21 @@ void reduceVectorMin(std::vector const& source, std::vector* target, std:: } } +template +void reduceVectorMin(std::vector const& source, std::vector* target, std::vector const& scc, std::vector const& filter) { + for (auto stateIt = scc.cbegin(); stateIt != scc.cend(); ++stateIt) { + (*target)[*stateIt] = source[filter[*stateIt]]; + + for (auto row = filter[*stateIt] + 1; row < filter[*stateIt + 1]; ++row) { + // We have to minimize the value, so only overwrite the current value if the + // value is actually lower. + if (source[row] < (*target)[*stateIt]) { + (*target)[*stateIt] = source[row]; + } + } + } +} + template void reduceVectorMax(std::vector const& source, std::vector* target, std::vector const& filter) { uint_fast64_t currentSourceRow = 0; @@ -127,6 +142,21 @@ void reduceVectorMax(std::vector const& source, std::vector* target, std:: } } +template +void reduceVectorMax(std::vector const& source, std::vector* target, std::vector const& scc, std::vector const& filter) { + for (auto stateIt = scc.cbegin(); stateIt != scc.cend(); ++stateIt) { + (*target)[*stateIt] = source[filter[*stateIt]]; + + for (auto row = filter[*stateIt] + 1; row < filter[*stateIt + 1]; ++row) { + // We have to maximize the value, so only overwrite the current value if the + // value is actually lower. + if (source[row] > (*target)[*stateIt]) { + (*target)[*stateIt] = source[row]; + } + } + } +} + template bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T precision, bool relativeError) { if (vectorLeft.size() != vectorRight.size()) { @@ -145,6 +175,24 @@ bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const return true; } +template +bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector const& scc, T precision, bool relativeError) { + if (vectorLeft.size() != vectorRight.size()) { + LOG4CPLUS_ERROR(logger, "Lengths of vectors does not match and makes comparison impossible."); + throw storm::exceptions::InvalidArgumentException() << "Length of vectors does not match and makes comparison impossible."; + } + + for (uint_fast64_t state : scc) { + if (relativeError) { + if (std::abs(vectorLeft[state] - vectorRight[state])/vectorRight[state] > precision) return false; + } else { + if (std::abs(vectorLeft[state] - vectorRight[state]) > precision) return false; + } + } + + return true; +} + } //namespace utility } //namespace storm