diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index f3d226ac0..40cec5558 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -92,7 +92,7 @@ public: // 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 statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound); + storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound); LOG4CPLUS_INFO(logger, "Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states."); // Check if we already know the result (i.e. probability 0) for all initial states and @@ -409,7 +409,7 @@ public: // Determine which states have a reward of infinity by definition. storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, targetStates); + storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel().getBackwardTransitions(), trueStates, targetStates); infinityStates.complement(); storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 2bc58df7d..ee61275eb 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -1,4 +1,7 @@ #include "src/modelchecker/reachability/SparseSccModelChecker.h" + +#include + #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/utility/graph.h" #include "src/exceptions/ExceptionMacros.h" @@ -40,17 +43,17 @@ namespace storm { std::vector oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); // Then, we recursively treat all SCCs. - treatScc(dtmc, flexibleMatrix, dtmc.getInitialStates(), maybeStates, statesWithProbability1, dtmc.getBackwardTransitions(), false, 0); + treatScc(dtmc, flexibleMatrix, oneStepProbabilities, dtmc.getInitialStates(), maybeStates, statesWithProbability1, dtmc.getBackwardTransitions(), false, 0); // Now, we return the value for the only initial state. - return flexibleMatrix.getRow(initialStateIndex)[0].getValue(); + return oneStepProbabilities[initialStateIndex]; } template - void SparseSccModelChecker::treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& targetStates, storm::storage::SparseMatrix const& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) { + void SparseSccModelChecker::treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& targetStates, storm::storage::SparseMatrix const& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) { if (level <= 2) { // Here, we further decompose the SCC into sub-SCCs. - storm::storage::StronglyConnectedComponentDecomposition decomposition(dtmc, scc, true, false); + storm::storage::StronglyConnectedComponentDecomposition decomposition(dtmc, scc & ~entryStates, true, false); // To eliminate the remaining one-state SCCs, we need to keep track of them. storm::storage::BitVector remainingStates(scc); @@ -78,7 +81,7 @@ namespace storm { } // Recursively descend in SCC-hierarchy. - treatScc(dtmc, matrix, entryStates, scc, targetStates, backwardTransitions, true, level + 1); + treatScc(dtmc, matrix, oneStepProbabilities, entryStates, scc, targetStates, backwardTransitions, true, level + 1); } // If we are not supposed to eliminate the entry states, we need to take them out of the set of @@ -91,12 +94,61 @@ namespace storm { // Therefore, we need to eliminate all states. for (auto const& state : remainingStates) { if (!targetStates.get(state)) { - eliminateState(matrix, state, backwardTransitions); + eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); } } } else { // In this case, we perform simple state elimination in the current SCC. + storm::storage::BitVector remainingStates(scc); + + // 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; + } + + // Eliminate the remaining states. + for (auto const& state : remainingStates) { + if (!targetStates.get(state)) { + eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); + } + } + } + } + + template + void SparseSccModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix const& backwardTransitions) { + + ValueType loopProbability = storm::utility::constantZero(); + for (auto const& entry : matrix.getRow(state)) { + if (entry.getColumn() == state) { + loopProbability = entry.getValue(); + break; + } + } + + // Scale all entries in this row with (1 / (1 - loopProbability)). + loopProbability = 1 / (1 - loopProbability); + for (auto& entry : matrix.getRow(state)) { + entry.setValue(entry.getValue() * loopProbability); + } + oneStepProbabilities[state] *= loopProbability; + + // Now connect the predecessors of the state to eliminate with its successors. + std::size_t newEntries = matrix.getRow(state).size(); + for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { + // First, add all entries of the successor to the list of outgoing transitions of the predecessor. + typename FlexibleSparseMatrix::row_type row = matrix.getRow(predecessorEntry.getColumn()); + row.reserve(row.size() + newEntries); + row.insert(row.end(), matrix.getRow(state).begin(), matrix.getRow(state).end()); + + // 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(); }); + // Now we can eliminate entries with the same column by simple addition. + for () { + // TODO + } } } diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index 889d6835a..057fdaf6d 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -10,6 +10,8 @@ namespace storm { typedef uint_fast64_t index_type; typedef ValueType value_type; typedef std::vector> row_type; + typedef typename row_type::iterator iterator; + typedef typename row_type::const_iterator const_iterator; FlexibleSparseMatrix() = default; FlexibleSparseMatrix(index_type rows); @@ -31,8 +33,10 @@ namespace storm { static ValueType computeReachabilityProbability(storm::models::Dtmc const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); private: - static void treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& targetStates, storm::storage::SparseMatrix const& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level); + 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::BitVector const& targetStates, storm::storage::SparseMatrix const& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level); static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix); + static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix const& backwardTransitions); + }; } } diff --git a/src/utility/graph.h b/src/utility/graph.h index 39bbc2980..21972adbc 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -55,7 +55,7 @@ namespace storm { currentState = stack.back(); stack.pop_back(); - for (auto const& successor : transitionMatrix.begin(currentState)) { + for (auto const& successor : transitionMatrix.getRow(currentState)) { // Only explore the state if the transition was actually there and the successor has not yet // been visited. if (successor.getValue() > storm::utility::constantZero() && !reachableStates.get(successor.getColumn())) { @@ -198,8 +198,8 @@ namespace storm { static std::pair performProb01(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - result.first = performProbGreater0(model, backwardTransitions, phiStates, psiStates); - result.second = performProb1(model, backwardTransitions, phiStates, psiStates, result.first); + result.first = performProbGreater0(backwardTransitions, phiStates, psiStates); + result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first); result.first.complement(); return result; }