diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 3592983e6..31a94c605 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -1,4 +1,7 @@ #include "src/modelchecker/reachability/SparseSccModelChecker.h" +#include "src/storage/StronglyConnectedComponentDecomposition.h" +#include "src/utility/graph.h" +#include "src/exceptions/ExceptionMacros.h" namespace storm { namespace modelchecker { @@ -6,23 +9,88 @@ namespace storm { template ValueType SparseSccModelChecker::computeReachabilityProbability(storm::models::Dtmc const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + // First, do some sanity checks to establish some required properties. + LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + typename FlexibleSparseMatrix::index_type initialStateIndex = *dtmc.getInitialStates().begin(); + storm::storage::BitVector relevantStates = storm::utility::graph::getReachableStates(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), phiStates, psiStates); + std::pair statesWithProbability01 = storm::utility::graph::performProb01(dtmc, phiStates, psiStates); + storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); + storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); + storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - return 0; + // If the initial state is known to have either probability 0 or 1, we can directly return the result. + if (!maybeStates.get(initialStateIndex)) { + return statesWithProbability0.get(initialStateIndex) ? 0 : 1; + } + + + // Otherwise, we build the submatrix that only has maybe states + + submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + + // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. + FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(dtmc.getTransitionMatrix()); + + // Then, we recursively treat all SCCs. + treatScc(dtmc, flexibleMatrix, storm::storage::BitVector(dtmc.getNumberOfStates(), true), 0); + + // Now, we return the value for the only initial state. + return flexibleMatrix.getRow(initialStateIndex)[0].getValue(); + } + + template + void SparseSccModelChecker::treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, storm::storage::BitVector const& scc, uint_fast64_t level) { + if (level < 2) { + // Here, we further decompose the SCC into sub-SCCs. + storm::storage::StronglyConnectedComponentDecomposition decomposition(dtmc, scc, true, false); + + // And then recursively treat all sub-SCCs. + for (auto const& newScc : decomposition) { + treatScc(dtmc, matrix, scc, level + 1); + } + + + + } else { + // In this case, we perform simple state elimination in the current SCC. + + } + } + + template + FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) { + // Intentionally left empty. + } + + template + void FlexibleSparseMatrix::reserveInRow(index_type row, index_type numberOfElements) { + this->data[row].reserve(numberOfElements); + } + + template + typename FlexibleSparseMatrix::row_type& FlexibleSparseMatrix::getRow(index_type index) { + return this->data[index]; } template - typename SparseSccModelChecker::FlexibleSparseMatrix SparseSccModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix) { - FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); + FlexibleSparseMatrix SparseSccModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix) { + FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); - for (SparseSccModelChecker::FlexibleMatrix::index_type row = 0; row < matrix.getRowCount(); ++row) { + for (typename FlexibleSparseMatrix::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) { + typename storm::storage::SparseMatrix::const_rows row = matrix.getRow(rowIndex); + flexibleMatrix.reserveInRow(rowIndex, row.getNumberOfEntries()); + for (auto const& element : row) { + flexibleMatrix.getRow(rowIndex).emplace_back(element); + } } return flexibleMatrix; } + template class FlexibleSparseMatrix; template class SparseSccModelChecker; } // namespace reachability diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index 7e6d89ead..e32f99f04 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -3,33 +3,36 @@ namespace storm { namespace modelchecker { namespace reachability { + + template + class FlexibleSparseMatrix { + public: + typedef uint_fast64_t index_type; + typedef ValueType value_type; + typedef std::vector> row_type; + + FlexibleSparseMatrix() = default; + FlexibleSparseMatrix(index_type rows); + + void reserveInRow(index_type row, index_type numberOfElements); + + row_type& getRow(index_type); + + private: + std::vector data; + }; template class SparseSccModelChecker { private: - class FlexibleSparseMatrix { - public: - typedef uint_fast64_t index_type; - typedef ValueType value_type; - typedef std::vector> row_type; - - FlexibleSparseMatrix(index_type rows); - - void reserveInRow(index_type row, index_type numberOfElements); - - row_type& getRow(index_type); - - private: - std::vector data; - }; + public: static ValueType computeReachabilityProbability(storm::models::Dtmc const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); private: - void treatScc(storm::storage::SparseMatrix& matrix, storm::storage::BitVector const& scc, uint_fast64_t level) const; - - FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix); + static void treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, storm::storage::BitVector const& scc, uint_fast64_t level); + static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix); }; } } diff --git a/src/storm.cpp b/src/storm.cpp index e708d6c70..ff2e4da47 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -232,7 +232,8 @@ int main(const int argc, const char* argv[]) { storm::storage::BitVector trueStates(model->getNumberOfStates(), true); storm::storage::BitVector oneStates = model->getLabeledStates("one"); - modelChecker.computeReachabilityProbability(*model->as>(), trueStates, oneStates); + double value = modelChecker.computeReachabilityProbability(*model->as>(), trueStates, oneStates); + std::cout << "computed value " << value << std::endl; if (s->isSet("mincmd")) { if (model->getType() != storm::models::MDP) { diff --git a/src/utility/graph.h b/src/utility/graph.h index 3d0d95fb1..79be321a1 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -33,11 +33,41 @@ namespace storm { namespace graph { /*! - * Performs a backwards breadt-first search trough the underlying graph structure + * Performs a forward depth-first search through the underlying graph structure to identify the states that + * are reachable from the given set only passing through a constrained set of states until some target + * have been reached. + * + * @param transitionMatrix The transition relation of the graph structure to search. + * @param initialStates The set of states from which to start the search. + * @param constraintStates The set of states that must not be left. + * @param targetStates The target states that may not be passed. + */ + template + storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) { + storm::storage::BitVector reachableStates(initialStates); + storm::storage::BitVector visitedStates(initialStates); + + // Initialize the stack used for the DFS with the states. + std::vector stack(initialStates.begin(), initialStates.end()); + + // Perform the actual DFS. + uint_fast64_t currentState = 0; + while (!stack.empty()) { + currentState = stack.back(); + stack.pop_back(); + + // TODO: actually search + } + + return reachableStates; + } + + /*! + * Performs a backward depth-first search trough the underlying graph structure * of the given model to determine which states of the model have a positive probability * of satisfying phi until psi. The resulting states are written to the given bit vector. * - * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the graph structure to search. * @param phiStates A bit vector of all states satisfying phi. * @param psiStates A bit vector of all states satisfying psi. * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. @@ -45,9 +75,10 @@ namespace storm { * @return A bit vector with all indices of states that have a probability greater than 0. */ template - storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { + storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { // Prepare the resulting bit vector. - storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); + uint_fast64_t numberOfStates = phiStates.size(); + storm::storage::BitVector statesWithProbabilityGreater0(numberOfStates); // Add all psi states as the already satisfy the condition. statesWithProbabilityGreater0 |= psiStates; @@ -59,9 +90,9 @@ namespace storm { std::vector stepStack; std::vector remainingSteps; if (useStepBound) { - stepStack.reserve(model.getNumberOfStates()); + stepStack.reserve(numberOfStates); stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps); - remainingSteps.resize(model.getNumberOfStates()); + remainingSteps.resize(numberOfStates); for (auto state : psiStates) { remainingSteps[state] = maximalSteps; } @@ -106,7 +137,7 @@ namespace storm { * characterizes the states that possess at least one path to a target state. * The results are written to the given bit vector. * - * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the graph structure to search. * @param phiStates A bit vector of all states satisfying phi. * @param psiStates A bit vector of all states satisfying psi. * @param statesWithProbabilityGreater0 A reference to a bit vector of states that possess a positive @@ -114,8 +145,8 @@ namespace storm { * @return A bit vector with all indices of states that have a probability greater than 1. */ template - storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { - storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, backwardTransitions, ~psiStates, ~statesWithProbabilityGreater0); + storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { + storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~statesWithProbabilityGreater0); statesWithProbability1.complement(); return statesWithProbability1; } @@ -127,15 +158,15 @@ namespace storm { * characterizes the states that possess at least one path to a target state. * The results are written to the given bit vector. * - * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the graph structure to search. * @param phiStates A bit vector of all states satisfying phi. * @param psiStates A bit vector of all states satisfying psi. * @return A bit vector with all indices of states that have a probability greater than 1. */ template - storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(model, backwardTransitions, phiStates, psiStates); - storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, backwardTransitions, ~psiStates, ~(statesWithProbabilityGreater0)); + storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(backwardTransitions, phiStates, psiStates); + storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~(statesWithProbabilityGreater0)); statesWithProbability1.complement(); return statesWithProbability1; }