diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 6ec1e6d86..0b520c168 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -260,10 +260,10 @@ namespace storm { std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. - FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix); - flexibleMatrix.filter(maybeStates, maybeStates); - FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions); - flexibleBackwardTransitions.filter(maybeStates, maybeStates); + storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix); + flexibleMatrix.createSubmatrix(maybeStates, maybeStates); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions); + flexibleBackwardTransitions.createSubmatrix(maybeStates, maybeStates); auto conversionEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); @@ -345,11 +345,11 @@ namespace storm { stateValues[*representativeIt] = bsccValue; } - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type& representativeForwardRow = flexibleMatrix.getRow(*representativeIt); + FlexibleRowType& representativeForwardRow = flexibleMatrix.getRow(*representativeIt); representativeForwardRow.clear(); representativeForwardRow.shrink_to_fit(); - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type& representativeBackwardRow = flexibleBackwardTransitions.getRow(*representativeIt); + FlexibleRowType& representativeBackwardRow = flexibleBackwardTransitions.getRow(*representativeIt); auto it = representativeBackwardRow.begin(), ite = representativeBackwardRow.end(); for (; it != ite; ++it) { if (it->getColumn() == *representativeIt) { @@ -739,8 +739,8 @@ namespace storm { } std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); - FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix); - FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrixTransposed, true); + storm::storage::FlexibleSparseMatrix flexibleMatrix(submatrix); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(submatrixTransposed, true); std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now(); std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); @@ -791,7 +791,7 @@ namespace storm { for (auto const& element : currentRow) { // If any of the successors is a phi state, we eliminate it (wrt. all its phi predecessors). if (!psiStates.get(element.getColumn())) { - typename FlexibleSparseMatrix::row_type const& successorRow = flexibleMatrix.getRow(element.getColumn()); + FlexibleRowType const& successorRow = flexibleMatrix.getRow(element.getColumn()); // Eliminate the successor only if there possibly is a psi state reachable through it. if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) { STORM_LOG_TRACE("Found non-psi successor " << element.getColumn() << " that needs to be eliminated."); @@ -821,7 +821,7 @@ namespace storm { for (auto const& element : currentRow) { // If any of the successors is a psi state, we eliminate it (wrt. all its psi predecessors). if (!phiStates.get(element.getColumn())) { - typename FlexibleSparseMatrix::row_type const& successorRow = flexibleMatrix.getRow(element.getColumn()); + FlexibleRowType const& successorRow = flexibleMatrix.getRow(element.getColumn()); if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) { STORM_LOG_TRACE("Found non-phi successor " << element.getColumn() << " that needs to be eliminated."); eliminateState(element.getColumn(), flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorUpdateCallback, boost::none, psiFilterCallback, false); @@ -890,7 +890,7 @@ namespace storm { } template - std::unique_ptr::StatePriorityQueue> SparseDtmcEliminationModelChecker::createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states) { + std::unique_ptr::StatePriorityQueue> SparseDtmcEliminationModelChecker::createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states) { STORM_LOG_TRACE("Creating state priority queue for states " << states); @@ -940,7 +940,7 @@ namespace storm { } template - void SparseDtmcEliminationModelChecker::performPrioritizedStateElimination(std::unique_ptr& priorityQueue, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) { + void SparseDtmcEliminationModelChecker::performPrioritizedStateElimination(std::unique_ptr& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) { ValueUpdateCallback valueUpdateCallback = [&values] (storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { values[state] = storm::utility::simplify(loopProbability * values[state]); }; PredecessorUpdateCallback predecessorCallback = [&values] (storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { values[predecessor] = storm::utility::simplify(values[predecessor] + storm::utility::simplify(probability * values[state])); }; @@ -959,7 +959,7 @@ namespace storm { } template - void SparseDtmcEliminationModelChecker::performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { + void SparseDtmcEliminationModelChecker::performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); std::size_t numberOfStatesToEliminate = statePriorities->size(); @@ -969,7 +969,7 @@ namespace storm { } template - uint_fast64_t SparseDtmcEliminationModelChecker::performHybridStateElimination(storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { + uint_fast64_t SparseDtmcEliminationModelChecker::performHybridStateElimination(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { // When using the hybrid technique, we recursively treat the SCCs up to some size. std::vector entryStateQueue; STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); @@ -992,8 +992,8 @@ namespace storm { std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. - FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix); - FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions); + storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions); auto conversionEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); @@ -1052,7 +1052,7 @@ namespace storm { } template - uint_fast64_t SparseDtmcEliminationModelChecker::treatScc(FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional> const& distanceBasedPriorities) { + uint_fast64_t SparseDtmcEliminationModelChecker::treatScc(storm::storage::FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional> const& distanceBasedPriorities) { uint_fast64_t maximalDepth = level; // If the SCCs are large enough, we try to split them further. @@ -1068,7 +1068,7 @@ namespace storm { storm::storage::BitVector remainingSccs(decomposition.size(), true); // First, get rid of the trivial SCCs. - storm::storage::BitVector statesInTrivialSccs(matrix.getNumberOfRows()); + storm::storage::BitVector statesInTrivialSccs(matrix.getRowCount()); for (uint_fast64_t sccIndex = 0; sccIndex < decomposition.size(); ++sccIndex) { storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex); if (scc.isTrivial()) { @@ -1130,17 +1130,14 @@ namespace storm { } template - void SparseDtmcEliminationModelChecker::eliminateState(storm::storage::sparse::state_type state, FlexibleSparseMatrix& matrix, FlexibleSparseMatrix& backwardTransitions, - ValueUpdateCallback const& callback, PredecessorUpdateCallback const& predecessorCallback, - boost::optional const& priorityUpdateCallback, - boost::optional const& predecessorFilterCallback, bool removeForwardTransitions) { + void SparseDtmcEliminationModelChecker::eliminateState(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix& matrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, ValueUpdateCallback const& callback, PredecessorUpdateCallback const& predecessorCallback, boost::optional const& priorityUpdateCallback, boost::optional const& predecessorFilterCallback, bool removeForwardTransitions) { STORM_LOG_TRACE("Eliminating state " << state << "."); // Start by finding loop probability. bool hasSelfLoop = false; ValueType loopProbability = storm::utility::zero(); - typename FlexibleSparseMatrix::row_type& currentStateSuccessors = matrix.getRow(state); + FlexibleRowType& currentStateSuccessors = matrix.getRow(state); for (auto entryIt = currentStateSuccessors.begin(), entryIte = currentStateSuccessors.end(); entryIt != entryIte; ++entryIt) { if (entryIt->getColumn() >= state) { if (entryIt->getColumn() == state) { @@ -1172,12 +1169,12 @@ namespace storm { } // Now connect the predecessors of the state being eliminated with its successors. - typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state); + FlexibleRowType& currentStatePredecessors = backwardTransitions.getRow(state); // In case we have a constrained elimination, we need to keep track of the new predecessors. - typename FlexibleSparseMatrix::row_type newCurrentStatePredecessors; + FlexibleRowType newCurrentStatePredecessors; - std::vector newBackwardProbabilities(currentStateSuccessors.size()); + std::vector newBackwardProbabilities(currentStateSuccessors.size()); for (auto& backwardProbabilities : newBackwardProbabilities) { backwardProbabilities.reserve(currentStatePredecessors.size()); } @@ -1203,8 +1200,8 @@ namespace storm { // First, find the probability with which the predecessor can move to the current state, because // the forward probabilities of the state to be eliminated need to be scaled with this factor. - typename FlexibleSparseMatrix::row_type& predecessorForwardTransitions = matrix.getRow(predecessor); - typename FlexibleSparseMatrix::row_type::iterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry const& a) { return a.getColumn() == state; }); + FlexibleRowType& predecessorForwardTransitions = matrix.getRow(predecessor); + FlexibleRowIterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry::index_type, typename storm::storage::FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() == state; }); // Make sure we have found the probability and set it to zero. STORM_LOG_THROW(multiplyElement != predecessorForwardTransitions.end(), storm::exceptions::InvalidStateException, "No probability for successor found."); @@ -1212,14 +1209,14 @@ namespace storm { multiplyElement->setValue(storm::utility::zero()); // At this point, we need to update the (forward) transitions of the predecessor. - typename FlexibleSparseMatrix::row_type::iterator first1 = predecessorForwardTransitions.begin(); - typename FlexibleSparseMatrix::row_type::iterator last1 = predecessorForwardTransitions.end(); - typename FlexibleSparseMatrix::row_type::iterator first2 = currentStateSuccessors.begin(); - typename FlexibleSparseMatrix::row_type::iterator last2 = currentStateSuccessors.end(); + FlexibleRowIterator first1 = predecessorForwardTransitions.begin(); + FlexibleRowIterator last1 = predecessorForwardTransitions.end(); + FlexibleRowIterator first2 = currentStateSuccessors.begin(); + FlexibleRowIterator last2 = currentStateSuccessors.end(); - typename FlexibleSparseMatrix::row_type newSuccessors; + FlexibleRowType newSuccessors; newSuccessors.reserve((last1 - first1) + (last2 - first2)); - std::insert_iterator result(newSuccessors, newSuccessors.end()); + std::insert_iterator result(newSuccessors, newSuccessors.end()); uint_fast64_t successorOffsetInNewBackwardTransitions = 0; // Now we merge the two successor lists. (Code taken from std::set_union and modified to suit our needs). @@ -1236,7 +1233,7 @@ namespace storm { } if (first2 == last2) { - std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry const& a) { return a.getColumn() != state; } ); + std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry::index_type, typename storm::storage::FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; } ); break; } if (first2->getColumn() < first1->getColumn()) { @@ -1251,7 +1248,7 @@ namespace storm { ++first1; } else { auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue())); - *result = storm::storage::MatrixEntry(first1->getColumn(), probability); + *result = storm::storage::MatrixEntry::index_type, typename storm::storage::FlexibleSparseMatrix::value_type>(first1->getColumn(), probability); newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability); // std::cout << "(2) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; ++first1; @@ -1288,7 +1285,7 @@ namespace storm { continue; } - typename FlexibleSparseMatrix::row_type& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn()); + FlexibleRowType& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn()); // std::cout << "old backward trans of " << successorEntry.getColumn() << std::endl; // for (auto const& trans : successorBackwardTransitions) { // std::cout << trans << std::endl; @@ -1297,24 +1294,24 @@ namespace storm { // Delete the current state as a predecessor of the successor state only if we are going to remove the // current state's forward transitions. if (removeForwardTransitions) { - typename FlexibleSparseMatrix::row_type::iterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry const& a) { return a.getColumn() == state; }); + FlexibleRowIterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry::index_type, typename storm::storage::FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() == state; }); STORM_LOG_ASSERT(elimIt != successorBackwardTransitions.end(), "Expected a proper backward transition from " << successorEntry.getColumn() << " to " << state << ", but found none."); successorBackwardTransitions.erase(elimIt); } - typename FlexibleSparseMatrix::row_type::iterator first1 = successorBackwardTransitions.begin(); - typename FlexibleSparseMatrix::row_type::iterator last1 = successorBackwardTransitions.end(); - typename FlexibleSparseMatrix::row_type::iterator first2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].begin(); - typename FlexibleSparseMatrix::row_type::iterator last2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].end(); + FlexibleRowIterator first1 = successorBackwardTransitions.begin(); + FlexibleRowIterator last1 = successorBackwardTransitions.end(); + FlexibleRowIterator first2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].begin(); + FlexibleRowIterator last2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].end(); // std::cout << "adding backward trans " << successorEntry.getColumn() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; // for (auto const& trans : newBackwardProbabilities[successorOffsetInNewBackwardTransitions]) { // std::cout << trans << std::endl; // } - typename FlexibleSparseMatrix::row_type newPredecessors; + FlexibleRowType newPredecessors; newPredecessors.reserve((last1 - first1) + (last2 - first2)); - std::insert_iterator result(newPredecessors, newPredecessors.end()); + std::insert_iterator result(newPredecessors, newPredecessors.end()); for (; first1 != last1; ++result) { if (first2 == last2) { @@ -1340,9 +1337,9 @@ namespace storm { } } if (predecessorFilterCallback) { - std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry const& a) { return a.getColumn() != state && predecessorFilterCallback.get()(a.getColumn()); }); + std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry::index_type, typename storm::storage::FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state && predecessorFilterCallback.get()(a.getColumn()); }); } else { - std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry const& a) { return a.getColumn() != state; }); + std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry::index_type, typename storm::storage::FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; }); } // Now move the new predecessors in place. @@ -1416,111 +1413,7 @@ namespace storm { } template - SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) { - // Intentionally left empty. - } - - template - void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::reserveInRow(index_type row, index_type numberOfElements) { - this->data[row].reserve(numberOfElements); - } - - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type& SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getRow(index_type index) { - return this->data[index]; - } - - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type const& SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getRow(index_type index) const { - return this->data[index]; - } - - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::index_type SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getNumberOfRows() const { - return this->data.size(); - } - - template - bool SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::hasSelfLoop(storm::storage::sparse::state_type state) { - for (auto const& entry : this->getRow(state)) { - if (entry.getColumn() < state) { - continue; - } else if (entry.getColumn() > state) { - return false; - } else if (entry.getColumn() == state) { - return true; - } - } - return false; - } - - template - void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::print() const { - for (uint_fast64_t index = 0; index < this->data.size(); ++index) { - std::cout << index << " - "; - for (auto const& element : this->getRow(index)) { - std::cout << "(" << element.getColumn() << ", " << element.getValue() << ") "; - } - std::cout << std::endl; - } - } - - template - bool SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::empty() const { - for (auto const& row : this->data) { - if (!row.empty()) { - return false; - } - } - return true; - } - - template - void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::filter(storm::storage::BitVector const& rowFilter, storm::storage::BitVector const& columnFilter) { - for (uint_fast64_t rowIndex = 0; rowIndex < this->data.size(); ++rowIndex) { - auto& row = this->data[rowIndex]; - if (!rowFilter.get(rowIndex)) { - row.clear(); - row.shrink_to_fit(); - continue; - } - row_type newRow; - for (auto const& element : row) { - if (columnFilter.get(element.getColumn())) { - newRow.push_back(element); - } - } - row = std::move(newRow); - } - } - - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix SparseDtmcEliminationModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) { - FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); - - 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) { - // If the probability is zero, we skip this entry. - if (storm::utility::isZero(element.getValue())) { - continue; - } - - if (setAllValuesToOne) { - flexibleMatrix.getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::one()); - } else { - flexibleMatrix.getRow(rowIndex).emplace_back(element); - } - } - } - - return flexibleMatrix; - } - - template - uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenalty(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { uint_fast64_t penalty = 0; bool hasParametricSelfLoop = false; @@ -1547,12 +1440,12 @@ namespace storm { } template - uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size(); } template - void SparseDtmcEliminationModelChecker::StatePriorityQueue::update(storm::storage::sparse::state_type, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + void SparseDtmcEliminationModelChecker::StatePriorityQueue::update(storm::storage::sparse::state_type, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { // Intentionally left empty. } @@ -1605,7 +1498,7 @@ namespace storm { } template - void SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::update(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + void SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { // First, we need to find the priority until now. auto priorityIt = stateToPriorityMapping.find(state); @@ -1634,8 +1527,8 @@ namespace storm { } template - bool SparseDtmcEliminationModelChecker::checkConsistent(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions) { - for (uint_fast64_t forwardIndex = 0; forwardIndex < transitionMatrix.getNumberOfRows(); ++forwardIndex) { + bool SparseDtmcEliminationModelChecker::checkConsistent(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions) { + for (uint_fast64_t forwardIndex = 0; forwardIndex < transitionMatrix.getRowCount(); ++forwardIndex) { for (auto const& forwardEntry : transitionMatrix.getRow(forwardIndex)) { if (forwardEntry.getColumn() == forwardIndex) { continue; diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 692a6be57..30c8e528a 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -2,6 +2,7 @@ #define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_ #include "src/storage/sparse/StateType.h" +#include "src/storage/FlexibleSparseMatrix.h" #include "src/models/sparse/Dtmc.h" #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/utility/constants.h" @@ -14,7 +15,9 @@ namespace storm { public: typedef typename SparseDtmcModelType::ValueType ValueType; typedef typename SparseDtmcModelType::RewardModelType RewardModelType; - + typedef typename storm::storage::FlexibleSparseMatrix::row_type FlexibleRowType; + typedef typename FlexibleRowType::iterator FlexibleRowIterator; + /*! * Creates an elimination-based model checker for the given model. * @@ -33,47 +36,12 @@ namespace storm { virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: - class FlexibleSparseMatrix { - public: - 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); - - void reserveInRow(index_type row, index_type numberOfElements); - - row_type& getRow(index_type); - row_type const& getRow(index_type) const; - - index_type getNumberOfRows() const; - - void print() const; - - bool empty() const; - - void filter(storm::storage::BitVector const& rowFilter, storm::storage::BitVector const& columnFilter); - - /*! - * Checks whether the given state has a self-loop with an arbitrary probability in the probability matrix. - * - * @param state The state for which to check whether it possesses a self-loop. - * @return True iff the given state has a self-loop with an arbitrary probability in the probability matrix. - */ - bool hasSelfLoop(storm::storage::sparse::state_type state); - - private: - std::vector data; - }; - + class StatePriorityQueue { public: virtual bool hasNextState() const = 0; virtual storm::storage::sparse::state_type popNextState() = 0; - virtual void update(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + virtual void update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); virtual std::size_t size() const = 0; }; @@ -96,7 +64,7 @@ namespace storm { } }; - typedef std::function const& oneStepProbabilities)> PenaltyFunctionType; + typedef std::function const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities)> PenaltyFunctionType; class DynamicPenaltyStatePriorityQueue : public StatePriorityQueue { public: @@ -104,7 +72,7 @@ namespace storm { virtual bool hasNextState() const override; virtual storm::storage::sparse::state_type popNextState() override; - virtual void update(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) override; + virtual void update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) override; virtual std::size_t size() const override; private: @@ -117,38 +85,36 @@ namespace storm { static std::vector computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& oneStepProbabilitiesToTarget); - static std::unique_ptr createStatePriorityQueue(boost::optional> const& stateDistances, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); + static std::unique_ptr createStatePriorityQueue(boost::optional> const& stateDistances, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); static std::unique_ptr createNaivePriorityQueue(storm::storage::BitVector const& states); - static void performPrioritizedStateElimination(std::unique_ptr& priorityQueue, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly); + static void performPrioritizedStateElimination(std::unique_ptr& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly); - static void performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional>& additionalStateValues, boost::optional> const& distanceBasedPriorities); + static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional>& additionalStateValues, boost::optional> const& distanceBasedPriorities); - static void performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); + static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); - static uint_fast64_t performHybridStateElimination(storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); + static uint_fast64_t performHybridStateElimination(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); - static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional> const& distanceBasedPriorities = boost::none); + static uint_fast64_t treatScc(storm::storage::FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional> const& distanceBasedPriorities = boost::none); - static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); - typedef std::function ValueUpdateCallback; typedef std::function PredecessorUpdateCallback; typedef std::function PriorityUpdateCallback; typedef std::function PredecessorFilterCallback; - static void eliminateState(storm::storage::sparse::state_type state, FlexibleSparseMatrix& matrix, FlexibleSparseMatrix& backwardTransitions, ValueUpdateCallback const& valueUpdateCallback, PredecessorUpdateCallback const& predecessorCallback, boost::optional const& priorityUpdateCallback = boost::none, boost::optional const& predecessorFilterCallback = boost::none, bool removeForwardTransitions = true); + static void eliminateState(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix& matrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, ValueUpdateCallback const& valueUpdateCallback, PredecessorUpdateCallback const& predecessorCallback, boost::optional const& priorityUpdateCallback = boost::none, boost::optional const& predecessorFilterCallback = boost::none, bool removeForwardTransitions = true); static std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); static std::vector getStateDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward); - static uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + static uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); - static uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + static uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); - static bool checkConsistent(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions); + static bool checkConsistent(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions); // A flag that indicates whether this model checker is supposed to produce results for all states or just for the initial states. bool computeResultsForInitialStatesOnly; diff --git a/src/storage/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp index b77f59736..10cda2ab2 100644 --- a/src/storage/FlexibleSparseMatrix.cpp +++ b/src/storage/FlexibleSparseMatrix.cpp @@ -2,14 +2,35 @@ #include "src/storage/SparseMatrix.h" #include "src/storage/BitVector.h" +#include "src/adapters/CarlAdapter.h" +#include "src/utility/constants.h" namespace storm { namespace storage { template - FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) { + FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows), columnCount(0), nonzeroEntryCount(0) { // Intentionally left empty. } + template + FlexibleSparseMatrix::FlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) : data(matrix.getRowCount()), columnCount(matrix.getColumnCount()), nonzeroEntryCount(matrix.getNonzeroEntryCount()) { + for (index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) { + typename storm::storage::SparseMatrix::const_rows row = matrix.getRow(rowIndex); + reserveInRow(rowIndex, row.getNumberOfEntries()); + for (auto const& element : row) { + // If the probability is zero, we skip this entry. + if (storm::utility::isZero(element.getValue())) { + continue; + } + if (setAllValuesToOne) { + getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::one()); + } else { + getRow(rowIndex).emplace_back(element); + } + } + } + } + template void FlexibleSparseMatrix::reserveInRow(index_type row, index_type numberOfElements) { this->data[row].reserve(numberOfElements); @@ -26,35 +47,33 @@ namespace storm { } template - typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getNumberOfRows() const { + typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getRowCount() const { return this->data.size(); } template - bool FlexibleSparseMatrix::hasSelfLoop(storm::storage::sparse::state_type state) { - for (auto const& entry : this->getRow(state)) { - if (entry.getColumn() < state) { - continue; - } else if (entry.getColumn() > state) { - return false; - } else if (entry.getColumn() == state) { - return true; - } - } - return false; + typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getColumnCount() const { + return columnCount; } template - void FlexibleSparseMatrix::print() const { - for (uint_fast64_t index = 0; index < this->data.size(); ++index) { - std::cout << index << " - "; - for (auto const& element : this->getRow(index)) { - std::cout << "(" << element.getColumn() << ", " << element.getValue() << ") "; + typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getNonzeroEntryCount() const { + return nonzeroEntryCount; + } + + template + void FlexibleSparseMatrix::updateDimensions() { + this->nonzeroEntryCount = 0; + this->columnCount = 0; + for (auto const& row : this->data) { + for (auto const& element : row) { + assert(!storm::utility::isZero(element.getValue())); + ++this->nonzeroEntryCount; + this->columnCount = std::max(element.getColumn() + 1, this->columnCount); } - std::cout << std::endl; } } - + template bool FlexibleSparseMatrix::empty() const { for (auto const& row : this->data) { @@ -64,25 +83,68 @@ namespace storm { } return true; } - + template - void FlexibleSparseMatrix::filter(storm::storage::BitVector const& rowFilter, storm::storage::BitVector const& columnFilter) { + void FlexibleSparseMatrix::createSubmatrix(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) { for (uint_fast64_t rowIndex = 0; rowIndex < this->data.size(); ++rowIndex) { auto& row = this->data[rowIndex]; - if (!rowFilter.get(rowIndex)) { + if (!rowConstraint.get(rowIndex)) { row.clear(); row.shrink_to_fit(); continue; } row_type newRow; for (auto const& element : row) { - if (columnFilter.get(element.getColumn())) { + if (columnConstraint.get(element.getColumn())) { newRow.push_back(element); } } row = std::move(newRow); } } + + template + storm::storage::SparseMatrix FlexibleSparseMatrix::createSparseMatrix() { + storm::storage::SparseMatrixBuilder matrixBuilder(getRowCount(), getColumnCount()); + for (uint_fast64_t rowIndex = 0; rowIndex < getRowCount(); ++rowIndex) { + auto& row = this->data[rowIndex]; + for (auto const& entry : row) { + matrixBuilder.addNextValue(rowIndex, entry.getColumn(), entry.getValue()); + } + } + return matrixBuilder.build(); + } + + template + bool FlexibleSparseMatrix::rowHasDiagonalElement(storm::storage::sparse::state_type state) { + for (auto const& entry : this->getRow(state)) { + if (entry.getColumn() < state) { + continue; + } else if (entry.getColumn() > state) { + return false; + } else if (entry.getColumn() == state) { + return true; + } + } + return false; + } + + template + std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix) { + for (uint_fast64_t index = 0; index < matrix->data.size(); ++index) { + out << index << " - "; + for (auto const& element : matrix->getRow(index)) { + out << "(" << element.getColumn() << ", " << element.getValue() << ") "; + } + return out; + } + } + + // Explicitly instantiate the matrix. + template class FlexibleSparseMatrix; +#ifdef STORM_HAVE_CARL + template class FlexibleSparseMatrix; +#endif - } -} \ No newline at end of file + } // namespace storage +} // namespace storm \ No newline at end of file diff --git a/src/storage/FlexibleSparseMatrix.h b/src/storage/FlexibleSparseMatrix.h index 6a30109ac..e6ac6c97d 100644 --- a/src/storage/FlexibleSparseMatrix.h +++ b/src/storage/FlexibleSparseMatrix.h @@ -5,6 +5,7 @@ #include #include "src/storage/sparse/StateType.h" +#include "src/storage/SparseMatrix.h" namespace storm { namespace storage { @@ -13,17 +14,14 @@ namespace storm { class BitVector; + /*! + * The flexible sparse matrix is used during state elimination. + */ template class FlexibleSparseMatrix { public: // TODO: make this class a bit more consistent with the big sparse matrix and improve it: - // * rename getNumberOfRows -> getRowCount - // * store number of columns to also provide getColumnCount - // * rename hasSelfLoop -> rowHasDiagonalElement // * add output iterator and improve the way the matrix is printed - // * add conversion functionality from/to sparse matrix - // * add documentation - // * rename filter to something more appropriate (getSubmatrix?) // * add stuff like clearRow, multiplyRowWithScalar typedef uint_fast64_t index_type; @@ -32,32 +30,113 @@ namespace storm { typedef typename row_type::iterator iterator; typedef typename row_type::const_iterator const_iterator; + /*! + * Constructs an empty flexible sparse matrix. + */ FlexibleSparseMatrix() = default; + + /*! + * Constructs a flexible sparse matrix with rows many rows. + * @param rows number of rows. + */ FlexibleSparseMatrix(index_type rows); - + + /*! + * Constructs a flexible sparse matrix from a sparse matrix. + * @param matrix Sparse matrix to construct from. + * @param setAllValuesToOne If true, all set entries are set to one. Default is false. + */ + FlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); + + /*! + * Reserves space for elements in row. + * @param row Row to reserve in. + * @param numberOfElements Number of elements to reserve space for. + */ void reserveInRow(index_type row, index_type numberOfElements); - + + /*! + * Returns an object representing the given row. + * + * @param row The row to get. + * @return An object representing the given row. + */ row_type& getRow(index_type); + + /*! + * Returns an object representing the given row. + * + * @param row The row to get. + * @return An object representing the given row. + */ row_type const& getRow(index_type) const; - - index_type getNumberOfRows() const; - - void print() const; - + + /*! + * Returns the number of rows of the matrix. + * + * @return The number of rows of the matrix. + */ + index_type getRowCount() const; + + /*! + * Returns the number of columns of the matrix. + * + * @return The number of columns of the matrix. + */ + index_type getColumnCount() const; + + /*! + * Returns the cached number of nonzero entries in the matrix. + * + * @return The number of nonzero entries in the matrix. + */ + index_type getNonzeroEntryCount() const; + + /*! + * Recomputes the number of columns and the number of non-zero entries. + */ + void updateDimensions(); + + /*! + * Checks if the matrix has no elements. + * @return True, if the matrix is empty. + */ bool empty() const; - - void filter(storm::storage::BitVector const& rowFilter, storm::storage::BitVector const& columnFilter); - + + /*! + * Creates a submatrix of the current matrix in place by dropping all rows and columns whose bits are not + * set to one in the given bit vector. + * + * @param rowConstraint A bit vector indicating which rows to keep. + * @param columnConstraint A bit vector indicating which columns to keep. + */ + void createSubmatrix(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint); + + /*! + * Creates a sparse matrix from the flexible sparse matrix. + * @return The sparse matrix. + */ + storm::storage::SparseMatrix createSparseMatrix(); + /*! * Checks whether the given state has a self-loop with an arbitrary probability in the probability matrix. * * @param state The state for which to check whether it possesses a self-loop. * @return True iff the given state has a self-loop with an arbitrary probability in the probability matrix. */ - bool hasSelfLoop(storm::storage::sparse::state_type state); - + bool rowHasDiagonalElement(storm::storage::sparse::state_type state); + + template + friend std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix); + private: std::vector data; + + // The number of columns of the matrix. + index_type columnCount; + + // The number of entries in the matrix. + index_type nonzeroEntryCount; }; } }