From 14fae4883a99a42ee62c62f38c6b205a61363ddf Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 30 May 2013 23:54:43 +0200 Subject: [PATCH] Added prob 0/1 precomputation for bounded-until model checking for DTMCs. The version for MDPs seems to perform worse: needs to be investigated. --- .../SparseDtmcPrctlModelChecker.h | 25 ++++++--- ...ogicalValueIterationMdpPrctlModelChecker.h | 4 +- src/models/AbstractModel.h | 54 +++++++++---------- src/storage/BitVector.h | 35 ++++++++++++ src/storage/SparseMatrix.h | 2 +- test/performance/graph/GraphTest.cpp | 8 +-- 6 files changed, 85 insertions(+), 43 deletions(-) diff --git a/src/modelchecker/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h index d22831618..feb77a88d 100644 --- a/src/modelchecker/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/SparseDtmcPrctlModelChecker.h @@ -88,19 +88,28 @@ public: storm::storage::BitVector* leftStates = formula.getLeft().check(*this); storm::storage::BitVector* rightStates = formula.getRight().check(*this); - // Copy the matrix before we make any changes. - storm::storage::SparseMatrix tmpMatrix(*this->getModel().getTransitionMatrix()); - - // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. - tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); + // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the + // further analysis. + storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(this->getModel(), *leftStates, *rightStates); + + // Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0. + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); + + // Make all rows absorbing that satisfy the second sub-formula. + submatrix.makeRowsAbsorbing(maybeStates % *rightStates); // Create the vector with which to multiply. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::vector::setVectorValues(*result, *rightStates, storm::utility::constGetOne()); + std::vector subresult(maybeStates.getNumberOfSetBits()); + storm::utility::vector::setVectorValues(subresult, *rightStates, storm::utility::constGetOne()); // Perform the matrix vector multiplication as often as required by the formula bound. - this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound()); + this->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound()); + // Create result vector and set its values accordingly. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + storm::utility::vector::setVectorValues(*result, maybeStates, subresult); + storm::utility::vector::setVectorValues(*result, ~maybeStates, storm::utility::constGetZero()); + // Delete obsolete intermediates and return result. delete leftStates; delete rightStates; diff --git a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h index 7368a91bf..d533dc3b1 100644 --- a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h @@ -67,9 +67,9 @@ private: bool relative = s->get("relative"); // Now, we need to determine the SCCs of the MDP and a topological sort. - std::vector> stronglyConnectedComponents = storm::utility::GraphAnalyzer::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + std::vector> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); - std::vector topologicalSort = storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); + std::vector topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); // Set up the environment for the power method. std::vector multiplyResult(matrix.getRowCount()); diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index d4fb10fcd..5d99b0f8f 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -85,55 +85,53 @@ class AbstractModel: public std::enable_shared_from_this> { virtual ModelType getType() const = 0; /*! - * Extracts the SCC dependency graph from the model according to the given SCC decomposition. + * Extracts the dependency graph from the model according to the given partition. * - * @param stronglyConnectedComponents A vector containing the SCCs of the system. - * @param stateToSccMap A mapping from state indices to + * @param partition A vector containing the blocks of the partition of the system. + * @return A sparse matrix with bool entries that represents the dependency graph of the blocks of the partition. */ - storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents) const { - uint_fast64_t numberOfStates = stronglyConnectedComponents.size(); + storm::storage::SparseMatrix extractPartitionDependencyGraph(std::vector> const& partition) const { + uint_fast64_t numberOfStates = partition.size(); // First, we need to create a mapping of states to their SCC index, to ease the computation // of dependency transitions later. - std::vector stateToSccMap(this->getNumberOfStates()); + std::vector stateToBlockMap(this->getNumberOfStates()); for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (uint_fast64_t j = 0; j < stronglyConnectedComponents[i].size(); ++j) { - stateToSccMap[stronglyConnectedComponents[i][j]] = i; + for (uint_fast64_t j = 0; j < partition[i].size(); ++j) { + stateToBlockMap[partition[i][j]] = i; } } - // The resulting sparse matrix will have as many rows/columns as there are SCCs. - - storm::storage::SparseMatrix sccDependencyGraph(numberOfStates); - sccDependencyGraph.initialize(); + // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition. + storm::storage::SparseMatrix dependencyGraph(numberOfStates); + dependencyGraph.initialize(); - for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) { - // Get the actual SCC. - std::vector const& scc = stronglyConnectedComponents[currentSccIndex]; + for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < partition.size(); ++currentBlockIndex) { + // Get the next block. + std::vector const& block = partition[currentBlockIndex]; - // Now, we determine the SCCs which are reachable (in one step) from the current SCC. - std::set allTargetSccs; - for (auto state : scc) { + // Now, we determine the blocks which are reachable (in one step) from the current block. + std::set allTargetBlocks; + for (auto state : block) { for (typename storm::storage::SparseMatrix::ConstIndexIterator succIt = this->constStateSuccessorIteratorBegin(state), succIte = this->constStateSuccessorIteratorEnd(state); succIt != succIte; ++succIt) { - uint_fast64_t targetScc = stateToSccMap[*succIt]; + uint_fast64_t targetBlock = stateToBlockMap[*succIt]; // We only need to consider transitions that are actually leaving the SCC. - if (targetScc != currentSccIndex) { - allTargetSccs.insert(targetScc); + if (targetBlock != currentBlockIndex) { + allTargetBlocks.insert(targetBlock); } } } // Now we can just enumerate all the target SCCs and insert the corresponding transitions. - for (auto targetScc : allTargetSccs) { - sccDependencyGraph.insertNextValue(currentSccIndex, targetScc, true); + for (auto targetBlock : allTargetBlocks) { + dependencyGraph.insertNextValue(currentBlockIndex, targetBlock, true); } } - // Finalize the matrix. - sccDependencyGraph.finalize(true); - - return sccDependencyGraph; + // Finalize the matrix and return result. + dependencyGraph.finalize(true); + return dependencyGraph; } /*! @@ -332,7 +330,7 @@ class AbstractModel: public std::enable_shared_from_this> { << std::endl; } - protected: +protected: /*! A matrix representing the likelihoods of moving between states. */ std::shared_ptr> transitionMatrix; diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index fe5cb5a30..7295f29bf 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -469,6 +469,41 @@ public: } return true; } + + /*! + * Computes a bit vector such that bit i is set iff the i-th set bit of the current bit vector is also contained + * in the given bit vector. + * + * @param bv A reference the bit vector to be used. + * @return A bit vector whose i-th bit is set iff the i-th set bit of the current bit vector is also contained + * in the given bit vector. + */ + BitVector operator%(BitVector const& bv) const { + // Create resulting bit vector. + BitVector result(this->getNumberOfSetBits()); + + // If the current bit vector has not too many elements compared to the given bit vector we prefer iterating + // over its elements. + if (this->getNumberOfSetBits() / 10 < bv.getNumberOfSetBits()) { + uint_fast64_t position = 0; + for (auto bit : *this) { + if (bv.get(bit)) { + result.set(position, true); + } + ++position; + } + } else { + // If the given bit vector had much less elements, we iterate over its elements and accept calling the more + // costly operation getNumberOfSetBitsBeforeIndex on the current bit vector. + for (auto bit : bv) { + if (this->get(bit)) { + result.set(this->getNumberOfSetBitsBeforeIndex(bit), true); + } + } + } + + return result; + } /*! * Adds all indices of bits set to one to the provided list. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 566629f3c..5e2019142 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -592,7 +592,7 @@ public: // Check whether the accessed state exists. if (row > rowCount) { LOG4CPLUS_ERROR(logger, "Trying to make an illegal row " << row << " absorbing."); - throw storm::exceptions::OutOfRangeException("Trying to make an illegal row absorbing."); + throw storm::exceptions::OutOfRangeException() << "Trying to make an illegal row " << row << " absorbing."; return false; } diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 4696ad8e5..5f56136b3 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -93,7 +93,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { ASSERT_EQ(sccDecomposition.size(), 1290297u); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of crowds/crowds20_5..."); - storm::storage::SparseMatrix sccDependencyGraph = dtmc->extractSccDependencyGraph(sccDecomposition); + storm::storage::SparseMatrix sccDependencyGraph = dtmc->extractPartitionDependencyGraph(sccDecomposition); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1371253u); @@ -110,7 +110,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { ASSERT_EQ(sccDecomposition.size(), 1279673u); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of synchronous_leader/leader6_8..."); - sccDependencyGraph = dtmc2->extractSccDependencyGraph(sccDecomposition); + sccDependencyGraph = dtmc2->extractPartitionDependencyGraph(sccDecomposition); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1535367u); @@ -127,7 +127,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { ASSERT_EQ(sccDecomposition.size(), 214675); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6..."); - sccDependencyGraph = mdp->extractSccDependencyGraph(sccDecomposition); + sccDependencyGraph = mdp->extractPartitionDependencyGraph(sccDecomposition); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 684093u); @@ -144,7 +144,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { ASSERT_EQ(sccDecomposition.size(), 63611u); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6..."); - sccDependencyGraph = mdp2->extractSccDependencyGraph(sccDecomposition); + sccDependencyGraph = mdp2->extractPartitionDependencyGraph(sccDecomposition); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 213400u);