From 79dcfc16c702d80fee5f87356002831881d545af Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 25 Sep 2014 23:19:25 +0200 Subject: [PATCH] Started adding some optimizations to SCC-based model checker. Former-commit-id: d60a8703bb958b9b6e4bd9125b0b50c5aa6b6fb9 --- .../reachability/SparseSccModelChecker.cpp | 133 +++++++++++++++--- .../reachability/SparseSccModelChecker.h | 1 + src/storage/sparse/StateType.h | 2 + 3 files changed, 120 insertions(+), 16 deletions(-) diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index fe8cb821b..100f2cbc3 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -54,18 +54,39 @@ namespace storm { // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). maybeStates &= reachableStates; - // Otherwise, we build the submatrix that only has the transitions of the maybe states. + // Create a vector for the probabilities to go to a state with probability 1 in one step. + std::vector oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); + + // Determine the set of initial states of the sub-DTMC. + storm::storage::BitVector newInitialStates = dtmc.getInitialStates() % maybeStates; + + // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + // Create a bit vector that represents the subsystem of states we still have to eliminate. + storm::storage::BitVector subsystem = storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true); + + // Now eliminate chains. +// { +// storm::storage::SparseMatrix backwardTransitions = submatrix.transpose(); +// +// // As a preprocessing step, we eliminate all states in place that have exactly one outgoing transition, +// // because we can eliminate them in-place. +// for (auto state : maybeStates & ~newInitialStates) { +// if (submatrix.getRow(state).getNumberOfEntries() == 1 && backwardTransitions.getRow(state).getNumberOfEntries() == 1) { +// if (eliminateStateInPlace(submatrix, oneStepProbabilities, state, backwardTransitions)) { +// subsystem.set(state, false); +// } +// } +// } +// } + // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix); - - // Create a vector for the probabilities to go to a state with probability 1 in one step. - std::vector oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); + FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrix.transpose(), true); // Then, we recursively treat all SCCs. - FlexibleSparseMatrix backwardTransitions = getFlexibleSparseMatrix(submatrix.transpose(), true); - treatScc(dtmc, flexibleMatrix, oneStepProbabilities, dtmc.getInitialStates() % maybeStates, storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true), submatrix, backwardTransitions, false, 0); + treatScc(dtmc, flexibleMatrix, oneStepProbabilities, newInitialStates, subsystem, submatrix, flexibleBackwardTransitions, false, 0); // Now, we return the value for the only initial state. return oneStepProbabilities[initialStateIndex]; @@ -76,10 +97,10 @@ namespace storm { // If the SCCs are large enough, we try to split them further. if (scc.getNumberOfSetBits() > SparseSccModelChecker::maximalSccSize) { // Here, we further decompose the SCC into sub-SCCs. - storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, scc & ~entryStates, true, false); + storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, scc & ~entryStates, false, false); // To eliminate the remaining one-state SCCs, we need to keep track of them. - storm::storage::BitVector remainingStates(scc); + // storm::storage::BitVector remainingStates(scc); // Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which // we eliminate the SCCs. @@ -106,7 +127,7 @@ namespace storm { // Rewrite SCC into bit vector and subtract it from the remaining states. storm::storage::BitVector newSccAsBitVector(forwardTransitions.getRowCount(), newScc.begin(), newScc.end()); - remainingStates &= ~newSccAsBitVector; + // remainingStates &= ~newSccAsBitVector; // Determine the set of entry states of the SCC. storm::storage::BitVector entryStates(dtmc.getNumberOfStates()); @@ -124,15 +145,15 @@ namespace storm { // If we are not supposed to eliminate the entry states, we need to take them out of the set of // remaining states. - if (!eliminateEntryStates) { - remainingStates &= ~entryStates; - } - + // if (!eliminateEntryStates) { + // remainingStates &= ~entryStates; + // } + // // Now that we eliminated all non-trivial sub-SCCs, we need to take care of trivial sub-SCCs. // Therefore, we need to eliminate all states. - for (auto const& state : remainingStates) { - eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); - } + // for (auto const& state : remainingStates) { + // eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); + // } } else { // In this case, we perform simple state elimination in the current SCC. storm::storage::BitVector remainingStates(scc); @@ -301,6 +322,86 @@ namespace storm { currentStateSuccessors.shrink_to_fit(); } + template + bool SparseSccModelChecker::eliminateStateInPlace(storm::storage::SparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix& backwardTransitions) { + typename storm::storage::SparseMatrix::iterator forwardElement = matrix.getRow(state).begin(); + typename storm::storage::SparseMatrix::iterator backwardElement = backwardTransitions.getRow(state).begin(); + + if (forwardElement->getValue() != storm::utility::constantOne() || backwardElement->getValue() != storm::utility::constantOne()) { + return false; + } + + std::cout << "eliminating " << state << std::endl; + std::cout << "fwd element: " << *forwardElement << " and bwd element: " << *backwardElement << std::endl; + + // Find the element of the predecessor that moves to the state that we want to eliminate. + typename storm::storage::SparseMatrix::rows forwardRow = matrix.getRow(backwardElement->getColumn()); + typename storm::storage::SparseMatrix::iterator multiplyElement = std::find_if(forwardRow.begin(), forwardRow.end(), [&](storm::storage::MatrixEntry::index_type, typename storm::storage::SparseMatrix::value_type> const& a) { return a.getColumn() == state; }); + + std::cout << "before fwd: " << std::endl; + for (auto element : matrix.getRow(backwardElement->getColumn())) { + std::cout << element << ", " << std::endl; + } + + // Modify the forward probability entry of the predecessor. + multiplyElement->setValue(multiplyElement->getValue() * forwardElement->getValue()); + multiplyElement->setColumn(forwardElement->getColumn()); + + // Modify the one-step probability for the predecessor if necessary. + if (oneStepProbabilities[state] != storm::utility::constantZero()) { + oneStepProbabilities[backwardElement->getColumn()] += multiplyElement->getValue() * oneStepProbabilities[state]; + } + + // If the forward entry is not at the right position, we need to move it there. + if (multiplyElement != forwardRow.begin() && multiplyElement->getColumn() < (multiplyElement - 1)->getColumn()) { + while (multiplyElement != forwardRow.begin() && multiplyElement->getColumn() < (multiplyElement - 1)->getColumn()) { + std::swap(*multiplyElement, *(multiplyElement - 1)); + --multiplyElement; + } + } else if ((multiplyElement + 1) != forwardRow.end() && multiplyElement->getColumn() > (multiplyElement + 1)->getColumn()) { + while ((multiplyElement + 1) != forwardRow.end() && multiplyElement->getColumn() > (multiplyElement + 1)->getColumn()) { + std::swap(*multiplyElement, *(multiplyElement + 1)); + ++multiplyElement; + } + } + + std::cout << "after fwd: " << std::endl; + for (auto element : matrix.getRow(backwardElement->getColumn())) { + std::cout << element << ", " << std::endl; + } + + // Find the backward element of the successor that moves to the state that we want to eliminate. + typename storm::storage::SparseMatrix::rows backwardRow = backwardTransitions.getRow(forwardElement->getColumn()); + typename storm::storage::SparseMatrix::iterator backwardEntry = std::find_if(backwardRow.begin(), backwardRow.end(), [&](storm::storage::MatrixEntry::index_type, typename storm::storage::SparseMatrix::value_type> const& a) { return a.getColumn() == state; }); + + std::cout << "before bwd" << std::endl; + for (auto element : backwardTransitions.getRow(forwardElement->getColumn())) { + std::cout << element << ", " << std::endl; + } + + // Modify the predecessor list of the successor and add the predecessor of the state we eliminate. + backwardEntry->setColumn(backwardElement->getColumn()); + + // If the backward entry is not at the right position, we need to move it there. + if (backwardEntry != backwardRow.begin() && backwardEntry->getColumn() < (backwardEntry - 1)->getColumn()) { + while (backwardEntry != backwardRow.begin() && backwardEntry->getColumn() < (backwardEntry - 1)->getColumn()) { + std::swap(*backwardEntry, *(backwardEntry - 1)); + --backwardEntry; + } + } else if ((backwardEntry + 1) != backwardRow.end() && backwardEntry->getColumn() > (backwardEntry + 1)->getColumn()) { + while ((backwardEntry + 1) != backwardRow.end() && backwardEntry->getColumn() > (backwardEntry + 1)->getColumn()) { + std::swap(*backwardEntry, *(backwardEntry + 1)); + ++backwardEntry; + } + } + + std::cout << "after bwd" << std::endl; + for (auto element : backwardTransitions.getRow(forwardElement->getColumn())) { + std::cout << element << ", " << std::endl; + } + return true; + } + template FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) { // Intentionally left empty. diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index 775c7b3ca..b3b9367eb 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -33,6 +33,7 @@ namespace storm { static void treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level); static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions); + static bool void eliminateStateInPlace(storm::storage::SparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix& backwardTransitions); static const uint_fast64_t maximalSccSize = 1000; diff --git a/src/storage/sparse/StateType.h b/src/storage/sparse/StateType.h index a067c37e9..b20ead153 100644 --- a/src/storage/sparse/StateType.h +++ b/src/storage/sparse/StateType.h @@ -1,6 +1,8 @@ #ifndef STORM_STORAGE_SPARSE_STATETYPE_H_ #define STORM_STORAGE_SPARSE_STATETYPE_H_ +#include + namespace storm { namespace storage { namespace sparse {