Started implementing the state elimination procedure.

Former-commit-id: c548a2ec06

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.");

src/modelchecker/reachability/SparseSccModelChecker.cpp

@@ -1,4 +1,7 @@
 #include "src/modelchecker/reachability/SparseSccModelChecker.h"
+
+#include <algorithm>
+
 #include "src/storage/StronglyConnectedComponentDecomposition.h"
 #include "src/utility/graph.h"
 #include "src/exceptions/ExceptionMacros.h"
@@ -40,17 +43,17 @@ namespace storm {
                 std::vector<ValueType> 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<typename ValueType>
-            void SparseSccModelChecker<ValueType>::treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& targetStates, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) {
+            void SparseSccModelChecker<ValueType>::treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& targetStates, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) {
                 if (level <= 2) {
                     // Here, we further decompose the SCC into sub-SCCs.
-                    storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(dtmc, scc, true, false);
+                    storm::storage::StronglyConnectedComponentDecomposition<ValueType> 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<typename ValueType>
+            void SparseSccModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
+
+                ValueType loopProbability = storm::utility::constantZero<ValueType>();
+                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<ValueType>::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<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a, storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& b){ return a.getColumn() < b.getColumn(); });
                     
+                    // Now we can eliminate entries with the same column by simple addition.
+                    for () {
+                        // TODO
+                    }
                 }
             }
             

src/modelchecker/reachability/SparseSccModelChecker.h

@@ -10,6 +10,8 @@ namespace storm {
                 typedef uint_fast64_t index_type;
                 typedef ValueType value_type;
                 typedef std::vector<storm::storage::MatrixEntry<index_type, value_type>> 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<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
                 
             private:
-                static void treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& targetStates, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level);
+                static void treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& targetStates, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level);
                 static FlexibleSparseMatrix<ValueType> getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix);
+                static void eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
+
             };
         }
     }

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<T>() && !reachableStates.get(successor.getColumn())) {
@@ -198,8 +198,8 @@ namespace storm {
             static std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
                 std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
                 storm::storage::SparseMatrix<T> 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;
             }