From 8f7c9d5c257195be3346c1f990b38b20c26cb471 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 16 Sep 2014 00:39:10 +0200 Subject: [PATCH] Adapted SCC-interface such that it can also be given a matrix instead of a model. More work on SCC-based mc. Former-commit-id: 21d2482e4cd7f3fe095aca32119928330e34124e --- .../reachability/SparseSccModelChecker.cpp | 14 +++++++---- ...tronglyConnectedComponentDecomposition.cpp | 25 +++++++++++-------- .../StronglyConnectedComponentDecomposition.h | 22 +++++++++++++--- 3 files changed, 42 insertions(+), 19 deletions(-) diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 01c2df7f0..d9226ad66 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -58,7 +58,7 @@ namespace storm { if (level <= 2) { std::cout << "1" << std::endl; // Here, we further decompose the SCC into sub-SCCs. - storm::storage::StronglyConnectedComponentDecomposition decomposition(dtmc, scc & ~entryStates, true, false); + storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, scc & ~entryStates, true, false); std::cout << decomposition << std::endl; // To eliminate the remaining one-state SCCs, we need to keep track of them. @@ -147,13 +147,17 @@ namespace storm { typename FlexibleSparseMatrix::row_type row = matrix.getRow(predecessorEntry.getColumn()); typename FlexibleSparseMatrix::row_type::iterator multiplyElement = std::find_if(row.begin(), row.end(), [=](storm::storage::MatrixEntry::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() == state; }); + ValueType multiplyFactor = storm::utility::constantOne(); + if (multiplyElement != row.end()) { + // Remove the transition to the state that is to be eliminated. + multiplyElement->setValue(0); + multiplyFactor = multiplyElement->getValue(); + } + // Now scale all the entries in the current row and insert them in the transitions of the predecessor. row.reserve(row.size() + newEntries); - std::for_each(matrix.getRow(state).begin(), matrix.getRow(state).end(), [&] (storm::storage::MatrixEntry::index_type, typename FlexibleSparseMatrix::value_type> const& a) { row.emplace_back(a.getColumn(), multiplyElement->getValue() * a.getValue()); }); + std::for_each(matrix.getRow(state).begin(), matrix.getRow(state).end(), [&] (storm::storage::MatrixEntry::index_type, typename FlexibleSparseMatrix::value_type> const& a) { row.emplace_back(a.getColumn(), multiplyFactor * a.getValue()); }); - // Remove the transition to the state that is to be eliminated. - multiplyElement->setValue(0); - // Then sort the vector according to their column indices. std::sort(row.begin(), row.end(), [](storm::storage::MatrixEntry::index_type, typename FlexibleSparseMatrix::value_type> const& a, storm::storage::MatrixEntry::index_type, typename FlexibleSparseMatrix::value_type> const& b){ return a.getColumn() < b.getColumn(); }); diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index b97094279..f519fc8ae 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -16,12 +16,17 @@ namespace storm { template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { storm::storage::BitVector subsystem(model.getNumberOfStates(), block.begin(), block.end()); - performSccDecomposition(model, subsystem, dropNaiveSccs, onlyBottomSccs); + performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs); } template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(model, subsystem, dropNaiveSccs, onlyBottomSccs); + performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs); + } + + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { + performSccDecomposition(transitionMatrix, subsystem, dropNaiveSccs, onlyBottomSccs); } template @@ -47,8 +52,8 @@ namespace storm { } template - void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { - uint_fast64_t numberOfStates = model.getNumberOfStates(); + void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // Set up the environment of the algorithm. // Start with the two stacks it maintains. @@ -71,7 +76,7 @@ namespace storm { uint_fast64_t currentIndex = 0; for (auto state : subsystem) { if (!hasPreorderNumber.get(state)) { - performSccDecompositionGCM(model, state, statesWithSelfLoop, subsystem, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount); + performSccDecompositionGCM(transitionMatrix, state, statesWithSelfLoop, subsystem, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount); } } @@ -103,7 +108,7 @@ namespace storm { for (uint_fast64_t state = 0; state < numberOfStates; ++state) { // If the block of the state is already known to be dropped, we don't need to check the transitions. if (!blocksToDrop.get(stateToSccMapping[state])) { - for (typename storm::storage::SparseMatrix::const_iterator successorIt = model.getRows(state).begin(), successorIte = model.getRows(state).end(); successorIt != successorIte; ++successorIt) { + for (typename storm::storage::SparseMatrix::const_iterator successorIt = transitionMatrix.getRowGroup(state).begin(), successorIte = transitionMatrix.getRowGroup(state).end(); successorIt != successorIte; ++successorIt) { if (subsystem.get(successorIt->getColumn()) && stateToSccMapping[state] != stateToSccMapping[successorIt->getColumn()]) { blocksToDrop.set(stateToSccMapping[state]); break; @@ -134,15 +139,15 @@ namespace storm { storm::storage::BitVector fullSystem(model.getNumberOfStates(), true); // Call the overloaded function. - performSccDecomposition(model, fullSystem, dropNaiveSccs, onlyBottomSccs); + performSccDecomposition(model.getTransitionMatrix(), fullSystem, dropNaiveSccs, onlyBottomSccs); } template - void StronglyConnectedComponentDecomposition::performSccDecompositionGCM(storm::models::AbstractModel const& model, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount) { + void StronglyConnectedComponentDecomposition::performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount) { // Prepare the stack used for turning the recursive procedure into an iterative one. std::vector recursionStateStack; - recursionStateStack.reserve(model.getNumberOfStates()); + recursionStateStack.reserve(transitionMatrix.getRowGroupCount()); recursionStateStack.push_back(startState); while (!recursionStateStack.empty()) { @@ -157,7 +162,7 @@ namespace storm { s.push_back(currentState); p.push_back(currentState); - for (auto const& successor : model.getRows(currentState)) { + for (auto const& successor : transitionMatrix.getRowGroup(currentState)) { if (subsystem.get(successor.getColumn()) && successor.getValue() != storm::utility::constantZero()) { if (currentState == successor.getColumn()) { statesWithSelfLoop.set(currentState); diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h index 0409c11a1..a83f6fe17 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storage/StronglyConnectedComponentDecomposition.h @@ -1,6 +1,7 @@ #ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ #define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ +#include "src/storage/SparseMatrix.h" #include "src/storage/Decomposition.h" #include "src/storage/BitVector.h" @@ -57,6 +58,19 @@ namespace storm { * leaving the SCC), are kept. */ StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + + /* + * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is + * given by a sparse matrix). + * + * @param transitionMatrix The transition matrix of the system to decompose. + * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. + * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state + * without a self-loop) are to be kept in the decomposition. + * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of + * leaving the SCC), are kept. + */ + StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false); /*! * Creates an SCC decomposition by copying the given SCC decomposition. @@ -103,21 +117,21 @@ namespace storm { * Performs the SCC decomposition of the given block in the given model. As a side-effect this fills * the vector of blocks of the decomposition. * - * @param model The model that contains the block. + * @param transitionMatrix The transition matrix of the system to decompose. * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state * without a self-loop) are to be kept in the decomposition. * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of * leaving the SCC), are kept. */ - void performSccDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); + void performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); /*! * Uses the algorithm by Gabow/Cheriyan/Mehlhorn ("Path-based strongly connected component algorithm") to * compute a mapping of states to their SCCs. All arguments given by (non-const) reference are modified by * the function as a side-effect. * - * @param model The model to decompose into SCCs. + * @param transitionMatrix The transition matrix of the system to decompose. * @param startState The starting state for the search of Tarjan's algorithm. * @param statesWithSelfLoop A bit vector that is to be filled with all states that have a self-loop. This * is later needed for identification of the naive SCCs. @@ -133,7 +147,7 @@ namespace storm { * @param sccCount The number of SCCs that have been computed. As a side effect of this function, this count * is increased. */ - void performSccDecompositionGCM(storm::models::AbstractModel const& model, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount); + void performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount); }; } }