Added prob 0/1 precomputation for bounded-until model checking for DTMCs. The version for MDPs seems to perform worse: needs to be investigated.

src/modelchecker/SparseDtmcPrctlModelChecker.h

@@ -88,19 +88,28 @@ public:
 		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
 		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
 
-		// Copy the matrix before we make any changes.
-		storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
-
-		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
-		tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
+        // 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 maybeStates = storm::utility::graph::performProbGreater0(this->getModel(), *leftStates, *rightStates);
+        
+        // Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0.
+        storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
+        
+		// Make all rows absorbing that satisfy the second sub-formula.
+		submatrix.makeRowsAbsorbing(maybeStates % *rightStates);
 
 		// Create the vector with which to multiply.
-		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
-		storm::utility::vector::setVectorValues(*result, *rightStates, storm::utility::constGetOne<Type>());
+        std::vector<Type> subresult(maybeStates.getNumberOfSetBits());
+		storm::utility::vector::setVectorValues(subresult, *rightStates, storm::utility::constGetOne<Type>());
 
 		// Perform the matrix vector multiplication as often as required by the formula bound.
-		this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound());
+		this->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound());
 
+        // Create result vector and set its values accordingly.
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+        storm::utility::vector::setVectorValues(*result, maybeStates, subresult);
+        storm::utility::vector::setVectorValues<Type>(*result, ~maybeStates, storm::utility::constGetZero<Type>());
+        
 		// Delete obsolete intermediates and return result.
 		delete leftStates;
 		delete rightStates;

src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h

@@ -67,9 +67,9 @@ private:
 		bool relative = s->get<bool>("relative");
 
 		// Now, we need to determine the SCCs of the MDP and a topological sort.
-        std::vector<std::vector<uint_fast64_t>> stronglyConnectedComponents = storm::utility::GraphAnalyzer::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph);
+        std::vector<std::vector<uint_fast64_t>> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph);
         storm::storage::SparseMatrix<bool> stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents);
-		std::vector<uint_fast64_t> topologicalSort = storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph);
+		std::vector<uint_fast64_t> topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph);
 
 		// Set up the environment for the power method.
 		std::vector<Type> multiplyResult(matrix.getRowCount());

src/models/AbstractModel.h

@@ -85,55 +85,53 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		virtual ModelType getType() const = 0;
 
         /*!
-         * Extracts the SCC dependency graph from the model according to the given SCC decomposition.
+         * Extracts the dependency graph from the model according to the given partition.
          *
-         * @param stronglyConnectedComponents A vector containing the SCCs of the system.
-         * @param stateToSccMap A mapping from state indices to
+         * @param partition A vector containing the blocks of the partition of the system.
+         * @return A sparse matrix with bool entries that represents the dependency graph of the blocks of the partition.
          */
-        storm::storage::SparseMatrix<bool> extractSccDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& stronglyConnectedComponents) const {
-            uint_fast64_t numberOfStates = stronglyConnectedComponents.size();
+        storm::storage::SparseMatrix<bool> extractPartitionDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& partition) const {
+            uint_fast64_t numberOfStates = partition.size();
             
             // First, we need to create a mapping of states to their SCC index, to ease the computation
             // of dependency transitions later.
-            std::vector<uint_fast64_t> stateToSccMap(this->getNumberOfStates());
+            std::vector<uint_fast64_t> stateToBlockMap(this->getNumberOfStates());
             for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
-                for (uint_fast64_t j = 0; j < stronglyConnectedComponents[i].size(); ++j) {
-                    stateToSccMap[stronglyConnectedComponents[i][j]] = i;
+                for (uint_fast64_t j = 0; j < partition[i].size(); ++j) {
+                    stateToBlockMap[partition[i][j]] = i;
                 }
             }
             
-            // The resulting sparse matrix will have as many rows/columns as there are SCCs.
-
-            storm::storage::SparseMatrix<bool> sccDependencyGraph(numberOfStates);
-            sccDependencyGraph.initialize();
+            // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition.
+            storm::storage::SparseMatrix<bool> dependencyGraph(numberOfStates);
+            dependencyGraph.initialize();
             
-            for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) {
-                // Get the actual SCC.
-                std::vector<uint_fast64_t> const& scc = stronglyConnectedComponents[currentSccIndex];
+            for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < partition.size(); ++currentBlockIndex) {
+                // Get the next block.
+                std::vector<uint_fast64_t> const& block = partition[currentBlockIndex];
                 
-                // Now, we determine the SCCs which are reachable (in one step) from the current SCC.
-                std::set<uint_fast64_t> allTargetSccs;
-                for (auto state : scc) {
+                // Now, we determine the blocks which are reachable (in one step) from the current block.
+                std::set<uint_fast64_t> allTargetBlocks;
+                for (auto state : block) {
                     for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator succIt = this->constStateSuccessorIteratorBegin(state), succIte = this->constStateSuccessorIteratorEnd(state); succIt != succIte; ++succIt) {
-                        uint_fast64_t targetScc = stateToSccMap[*succIt];
+                        uint_fast64_t targetBlock = stateToBlockMap[*succIt];
                         
                         // We only need to consider transitions that are actually leaving the SCC.
-                        if (targetScc != currentSccIndex) {
-                            allTargetSccs.insert(targetScc);
+                        if (targetBlock != currentBlockIndex) {
+                            allTargetBlocks.insert(targetBlock);
                         }
                     }
                 }
                 
                 // Now we can just enumerate all the target SCCs and insert the corresponding transitions.
-                for (auto targetScc : allTargetSccs) {
-                    sccDependencyGraph.insertNextValue(currentSccIndex, targetScc, true);
+                for (auto targetBlock : allTargetBlocks) {
+                    dependencyGraph.insertNextValue(currentBlockIndex, targetBlock, true);
                 }
             }
             
-            // Finalize the matrix.
-            sccDependencyGraph.finalize(true);
-            
-            return sccDependencyGraph;
+            // Finalize the matrix and return result.
+            dependencyGraph.finalize(true);
+            return dependencyGraph;
         }
     
         /*!
@@ -332,7 +330,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 				<< std::endl;
 		}
 
-	protected:
+protected:
 		/*! A matrix representing the likelihoods of moving between states. */
 		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix;
 

src/storage/BitVector.h

@@ -469,6 +469,41 @@ public:
 		}
 		return true;
 	}
+    
+    /*!
+	 * Computes a bit vector such that bit i is set iff the i-th set bit of the current bit vector is also contained
+     * in the given bit vector.
+     *
+	 * @param bv A reference the bit vector to be used.
+	 * @return A bit vector whose i-th bit is set iff the i-th set bit of the current bit vector is also contained
+     * in the given bit vector.
+	 */
+	BitVector operator%(BitVector const& bv) const {
+		// Create resulting bit vector.
+		BitVector result(this->getNumberOfSetBits());
+        
+        // If the current bit vector has not too many elements compared to the given bit vector we prefer iterating
+        // over its elements.
+        if (this->getNumberOfSetBits() / 10 < bv.getNumberOfSetBits()) {
+            uint_fast64_t position = 0;
+            for (auto bit : *this) {
+                if (bv.get(bit)) {
+                    result.set(position, true);
+                }
+                ++position;
+            }
+        } else {
+            // If the given bit vector had much less elements, we iterate over its elements and accept calling the more
+            // costly operation getNumberOfSetBitsBeforeIndex on the current bit vector.
+            for (auto bit : bv) {
+                if (this->get(bit)) {
+                    result.set(this->getNumberOfSetBitsBeforeIndex(bit), true);
+                }
+            }
+        }
+        
+		return result;
+	}
 
 	/*!
 	 * Adds all indices of bits set to one to the provided list.

src/storage/SparseMatrix.h

@@ -592,7 +592,7 @@ public:
 		// Check whether the accessed state exists.
 		if (row > rowCount) {
 			LOG4CPLUS_ERROR(logger, "Trying to make an illegal row " << row << " absorbing.");
-			throw storm::exceptions::OutOfRangeException("Trying to make an illegal row absorbing.");
+			throw storm::exceptions::OutOfRangeException() << "Trying to make an illegal row " << row << " absorbing.";
 			return false;
 		}
 

test/performance/graph/GraphTest.cpp

@@ -93,7 +93,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
     ASSERT_EQ(sccDecomposition.size(), 1290297u);
     
     LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of crowds/crowds20_5...");
-    storm::storage::SparseMatrix<bool> sccDependencyGraph = dtmc->extractSccDependencyGraph(sccDecomposition);
+    storm::storage::SparseMatrix<bool> sccDependencyGraph = dtmc->extractPartitionDependencyGraph(sccDecomposition);
     LOG4CPLUS_WARN(logger, "Done.");
     
     ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1371253u);
@@ -110,7 +110,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
     ASSERT_EQ(sccDecomposition.size(), 1279673u);
     
     LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of synchronous_leader/leader6_8...");
-    sccDependencyGraph = dtmc2->extractSccDependencyGraph(sccDecomposition);
+    sccDependencyGraph = dtmc2->extractPartitionDependencyGraph(sccDecomposition);
     LOG4CPLUS_WARN(logger, "Done.");
     
     ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1535367u);
@@ -127,7 +127,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
     ASSERT_EQ(sccDecomposition.size(), 214675);
     
     LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6...");
-    sccDependencyGraph = mdp->extractSccDependencyGraph(sccDecomposition);
+    sccDependencyGraph = mdp->extractPartitionDependencyGraph(sccDecomposition);
     LOG4CPLUS_WARN(logger, "Done.");
     
     ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 684093u);
@@ -144,7 +144,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
     ASSERT_EQ(sccDecomposition.size(), 63611u);
     
     LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6...");
-    sccDependencyGraph = mdp2->extractSccDependencyGraph(sccDecomposition);
+    sccDependencyGraph = mdp2->extractPartitionDependencyGraph(sccDecomposition);
     LOG4CPLUS_WARN(logger, "Done.");
     
     ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 213400u);