sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

FlexibleSparseMatrix is in own class now 

Former-commit-id: fdc569e443
tempestpy_adaptions
Mavo 9 years ago
parent
4eaf8f8443
commit
f67c92b526
4 changed files with 252 additions and 252 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 205
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  2. 70
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
  3. 114
      src/storage/FlexibleSparseMatrix.cpp
  4. 115
      src/storage/FlexibleSparseMatrix.h

205
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -260,10 +260,10 @@ namespace storm {
std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); 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. // 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<ValueType> flexibleMatrix(transitionMatrix);
flexibleMatrix.createSubmatrix(maybeStates, maybeStates);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardTransitions);
flexibleBackwardTransitions.createSubmatrix(maybeStates, maybeStates);
auto conversionEnd = std::chrono::high_resolution_clock::now(); auto conversionEnd = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point modelCheckingStart = 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; stateValues[*representativeIt] = bsccValue;
} }
typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::row_type& representativeForwardRow = flexibleMatrix.getRow(*representativeIt);
FlexibleRowType& representativeForwardRow = flexibleMatrix.getRow(*representativeIt);
representativeForwardRow.clear(); representativeForwardRow.clear();
representativeForwardRow.shrink_to_fit(); representativeForwardRow.shrink_to_fit();
typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::row_type& representativeBackwardRow = flexibleBackwardTransitions.getRow(*representativeIt);
FlexibleRowType& representativeBackwardRow = flexibleBackwardTransitions.getRow(*representativeIt);
auto it = representativeBackwardRow.begin(), ite = representativeBackwardRow.end(); auto it = representativeBackwardRow.begin(), ite = representativeBackwardRow.end();
for (; it != ite; ++it) { for (; it != ite; ++it) {
if (it->getColumn() == *representativeIt) { if (it->getColumn() == *representativeIt) {
@ -739,8 +739,8 @@ namespace storm {
} }
std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); 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<ValueType> flexibleMatrix(submatrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(submatrixTransposed, true);
std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now();
std::unique_ptr<StatePriorityQueue> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); std::unique_ptr<StatePriorityQueue> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate);
@ -791,7 +791,7 @@ namespace storm {
for (auto const& element : currentRow) { for (auto const& element : currentRow) {
// If any of the successors is a phi state, we eliminate it (wrt. all its phi predecessors). // If any of the successors is a phi state, we eliminate it (wrt. all its phi predecessors).
if (!psiStates.get(element.getColumn())) { 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. // 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())) { 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."); 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) { for (auto const& element : currentRow) {
// If any of the successors is a psi state, we eliminate it (wrt. all its psi predecessors). // If any of the successors is a psi state, we eliminate it (wrt. all its psi predecessors).
if (!phiStates.get(element.getColumn())) { 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())) { 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."); 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); eliminateState(element.getColumn(), flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorUpdateCallback, boost::none, psiFilterCallback, false);
@ -890,7 +890,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
std::unique_ptr<typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::StatePriorityQueue> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector<typename SparseDtmcModelType::ValueType>& oneStepProbabilities, storm::storage::BitVector const& states) {
std::unique_ptr<typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::StatePriorityQueue> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& states) {
STORM_LOG_TRACE("Creating state priority queue for states " << states); STORM_LOG_TRACE("Creating state priority queue for states " << states);
@ -940,7 +940,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performPrioritizedStateElimination(std::unique_ptr<StatePriorityQueue>& priorityQueue, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, std::vector<ValueType>& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) {
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performPrioritizedStateElimination(std::unique_ptr<StatePriorityQueue>& priorityQueue, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& 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]); }; 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])); }; 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<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities) {
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities) {
std::unique_ptr<StatePriorityQueue> statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); std::unique_ptr<StatePriorityQueue> statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem);
std::size_t numberOfStatesToEliminate = statePriorities->size(); std::size_t numberOfStatesToEliminate = statePriorities->size();
@ -969,7 +969,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
uint_fast64_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performHybridStateElimination(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities) {
uint_fast64_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performHybridStateElimination(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities) {
// When using the hybrid technique, we recursively treat the SCCs up to some size. // When using the hybrid technique, we recursively treat the SCCs up to some size.
std::vector<storm::storage::sparse::state_type> entryStateQueue; std::vector<storm::storage::sparse::state_type> entryStateQueue;
STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); 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(); 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. // 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<ValueType> flexibleMatrix(transitionMatrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardTransitions);
auto conversionEnd = std::chrono::high_resolution_clock::now(); auto conversionEnd = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point modelCheckingStart = 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<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
uint_fast64_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::treatScc(FlexibleSparseMatrix& matrix, std::vector<ValueType>& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities) {
uint_fast64_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::treatScc(storm::storage::FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities) {
uint_fast64_t maximalDepth = level; uint_fast64_t maximalDepth = level;
// If the SCCs are large enough, we try to split them further. // 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); storm::storage::BitVector remainingSccs(decomposition.size(), true);
// First, get rid of the trivial SCCs. // 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) { for (uint_fast64_t sccIndex = 0; sccIndex < decomposition.size(); ++sccIndex) {
storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex); storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex);
if (scc.isTrivial()) { if (scc.isTrivial()) {
@ -1130,17 +1130,14 @@ namespace storm {
} }
template<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::eliminateState(storm::storage::sparse::state_type state, FlexibleSparseMatrix& matrix, FlexibleSparseMatrix& backwardTransitions,
ValueUpdateCallback const& callback, PredecessorUpdateCallback const& predecessorCallback,
boost::optional<PriorityUpdateCallback> const& priorityUpdateCallback,
boost::optional<PredecessorFilterCallback> const& predecessorFilterCallback, bool removeForwardTransitions) {
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::eliminateState(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix<ValueType>& matrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, ValueUpdateCallback const& callback, PredecessorUpdateCallback const& predecessorCallback, boost::optional<PriorityUpdateCallback> const& priorityUpdateCallback, boost::optional<PredecessorFilterCallback> const& predecessorFilterCallback, bool removeForwardTransitions) {
STORM_LOG_TRACE("Eliminating state " << state << "."); STORM_LOG_TRACE("Eliminating state " << state << ".");
// Start by finding loop probability. // Start by finding loop probability.
bool hasSelfLoop = false; bool hasSelfLoop = false;
ValueType loopProbability = storm::utility::zero<ValueType>(); ValueType loopProbability = storm::utility::zero<ValueType>();
typename FlexibleSparseMatrix::row_type& currentStateSuccessors = matrix.getRow(state);
FlexibleRowType& currentStateSuccessors = matrix.getRow(state);
for (auto entryIt = currentStateSuccessors.begin(), entryIte = currentStateSuccessors.end(); entryIt != entryIte; ++entryIt) { for (auto entryIt = currentStateSuccessors.begin(), entryIte = currentStateSuccessors.end(); entryIt != entryIte; ++entryIt) {
if (entryIt->getColumn() >= state) { if (entryIt->getColumn() >= state) {
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. // 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. // 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<typename FlexibleSparseMatrix::row_type> newBackwardProbabilities(currentStateSuccessors.size());
std::vector<FlexibleRowType> newBackwardProbabilities(currentStateSuccessors.size());
for (auto& backwardProbabilities : newBackwardProbabilities) { for (auto& backwardProbabilities : newBackwardProbabilities) {
backwardProbabilities.reserve(currentStatePredecessors.size()); 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 // 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. // 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<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() == state; });
FlexibleRowType& predecessorForwardTransitions = matrix.getRow(predecessor);
FlexibleRowIterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
// Make sure we have found the probability and set it to zero. // 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."); 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<ValueType>()); multiplyElement->setValue(storm::utility::zero<ValueType>());
// At this point, we need to update the (forward) transitions of the predecessor. // 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)); newSuccessors.reserve((last1 - first1) + (last2 - first2));
std::insert_iterator<typename FlexibleSparseMatrix::row_type> result(newSuccessors, newSuccessors.end());
std::insert_iterator<FlexibleRowType> result(newSuccessors, newSuccessors.end());
uint_fast64_t successorOffsetInNewBackwardTransitions = 0; uint_fast64_t successorOffsetInNewBackwardTransitions = 0;
// Now we merge the two successor lists. (Code taken from std::set_union and modified to suit our needs). // 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) { if (first2 == last2) {
std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; } );
std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; } );
break; break;
} }
if (first2->getColumn() < first1->getColumn()) { if (first2->getColumn() < first1->getColumn()) {
@ -1251,7 +1248,7 @@ namespace storm {
++first1; ++first1;
} else { } else {
auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue())); auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue()));
*result = storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type>(first1->getColumn(), probability);
*result = storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type>(first1->getColumn(), probability);
newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability); newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability);
// std::cout << "(2) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; // std::cout << "(2) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl;
++first1; ++first1;
@ -1288,7 +1285,7 @@ namespace storm {
continue; 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; // std::cout << "old backward trans of " << successorEntry.getColumn() << std::endl;
// for (auto const& trans : successorBackwardTransitions) { // for (auto const& trans : successorBackwardTransitions) {
// std::cout << trans << std::endl; // 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 // Delete the current state as a predecessor of the successor state only if we are going to remove the
// current state's forward transitions. // current state's forward transitions.
if (removeForwardTransitions) { if (removeForwardTransitions) {
typename FlexibleSparseMatrix::row_type::iterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() == state; });
FlexibleRowIterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::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."); STORM_LOG_ASSERT(elimIt != successorBackwardTransitions.end(), "Expected a proper backward transition from " << successorEntry.getColumn() << " to " << state << ", but found none.");
successorBackwardTransitions.erase(elimIt); 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; // std::cout << "adding backward trans " << successorEntry.getColumn() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl;
// for (auto const& trans : newBackwardProbabilities[successorOffsetInNewBackwardTransitions]) { // for (auto const& trans : newBackwardProbabilities[successorOffsetInNewBackwardTransitions]) {
// std::cout << trans << std::endl; // std::cout << trans << std::endl;
// } // }
typename FlexibleSparseMatrix::row_type newPredecessors;
FlexibleRowType newPredecessors;
newPredecessors.reserve((last1 - first1) + (last2 - first2)); newPredecessors.reserve((last1 - first1) + (last2 - first2));
std::insert_iterator<typename FlexibleSparseMatrix::row_type> result(newPredecessors, newPredecessors.end());
std::insert_iterator<FlexibleRowType> result(newPredecessors, newPredecessors.end());
for (; first1 != last1; ++result) { for (; first1 != last1; ++result) {
if (first2 == last2) { if (first2 == last2) {
@ -1340,9 +1337,9 @@ namespace storm {
} }
} }
if (predecessorFilterCallback) { if (predecessorFilterCallback) {
std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state && predecessorFilterCallback.get()(a.getColumn()); });
std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state && predecessorFilterCallback.get()(a.getColumn()); });
} else { } else {
std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; });
std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; });
} }
// Now move the new predecessors in place. // Now move the new predecessors in place.
@ -1416,111 +1413,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) {
// Intentionally left empty.
}
template<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::reserveInRow(index_type row, index_type numberOfElements) {
this->data[row].reserve(numberOfElements);
}
template<typename SparseDtmcModelType>
typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::row_type& SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::getRow(index_type index) {
return this->data[index];
}
template<typename SparseDtmcModelType>
typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::row_type const& SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::getRow(index_type index) const {
return this->data[index];
}
template<typename SparseDtmcModelType>
typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::index_type SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::getNumberOfRows() const {
return this->data.size();
}
template<typename SparseDtmcModelType>
bool SparseDtmcEliminationModelChecker<SparseDtmcModelType>::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<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::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<typename SparseDtmcModelType>
bool SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix::empty() const {
for (auto const& row : this->data) {
if (!row.empty()) {
return false;
}
}
return true;
}
template<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::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 SparseDtmcModelType>
typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::FlexibleSparseMatrix SparseDtmcEliminationModelChecker<SparseDtmcModelType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne) {
FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount());
for (typename FlexibleSparseMatrix::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) {
typename storm::storage::SparseMatrix<ValueType>::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<ValueType>());
} else {
flexibleMatrix.getRow(rowIndex).emplace_back(element);
}
}
}
return flexibleMatrix;
}
template<typename SparseDtmcModelType>
uint_fast64_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeStatePenalty(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
uint_fast64_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
uint_fast64_t penalty = 0; uint_fast64_t penalty = 0;
bool hasParametricSelfLoop = false; bool hasParametricSelfLoop = false;
@ -1547,12 +1440,12 @@ namespace storm {
} }
template<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
uint_fast64_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
uint_fast64_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size(); return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size();
} }
template<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::StatePriorityQueue::update(storm::storage::sparse::state_type, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::StatePriorityQueue::update(storm::storage::sparse::state_type, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -1605,7 +1498,7 @@ namespace storm {
} }
template<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::DynamicPenaltyStatePriorityQueue::update(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::DynamicPenaltyStatePriorityQueue::update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
// First, we need to find the priority until now. // First, we need to find the priority until now.
auto priorityIt = stateToPriorityMapping.find(state); auto priorityIt = stateToPriorityMapping.find(state);
@ -1634,8 +1527,8 @@ namespace storm {
} }
template<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
bool SparseDtmcEliminationModelChecker<SparseDtmcModelType>::checkConsistent(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions) {
for (uint_fast64_t forwardIndex = 0; forwardIndex < transitionMatrix.getNumberOfRows(); ++forwardIndex) {
bool SparseDtmcEliminationModelChecker<SparseDtmcModelType>::checkConsistent(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions) {
for (uint_fast64_t forwardIndex = 0; forwardIndex < transitionMatrix.getRowCount(); ++forwardIndex) {
for (auto const& forwardEntry : transitionMatrix.getRow(forwardIndex)) { for (auto const& forwardEntry : transitionMatrix.getRow(forwardIndex)) {
if (forwardEntry.getColumn() == forwardIndex) { if (forwardEntry.getColumn() == forwardIndex) {
continue; continue;

70
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
View File

@ -2,6 +2,7 @@
#define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_ #define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_
#include "src/storage/sparse/StateType.h" #include "src/storage/sparse/StateType.h"
#include "src/storage/FlexibleSparseMatrix.h"
#include "src/models/sparse/Dtmc.h" #include "src/models/sparse/Dtmc.h"
#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "src/utility/constants.h" #include "src/utility/constants.h"
@ -14,7 +15,9 @@ namespace storm {
public: public:
typedef typename SparseDtmcModelType::ValueType ValueType; typedef typename SparseDtmcModelType::ValueType ValueType;
typedef typename SparseDtmcModelType::RewardModelType RewardModelType; typedef typename SparseDtmcModelType::RewardModelType RewardModelType;
typedef typename storm::storage::FlexibleSparseMatrix<ValueType>::row_type FlexibleRowType;
typedef typename FlexibleRowType::iterator FlexibleRowIterator;
/*! /*!
* Creates an elimination-based model checker for the given model. * Creates an elimination-based model checker for the given model.
* *
@ -33,47 +36,12 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override; virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
private: private:
class FlexibleSparseMatrix {
public:
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);
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<row_type> data;
};
class StatePriorityQueue { class StatePriorityQueue {
public: public:
virtual bool hasNextState() const = 0; virtual bool hasNextState() const = 0;
virtual storm::storage::sparse::state_type popNextState() = 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<ValueType> const& oneStepProbabilities);
virtual void update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities);
virtual std::size_t size() const = 0; virtual std::size_t size() const = 0;
}; };
@ -96,7 +64,7 @@ namespace storm {
} }
}; };
typedef std::function<uint_fast64_t (storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities)> PenaltyFunctionType;
typedef std::function<uint_fast64_t (storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities)> PenaltyFunctionType;
class DynamicPenaltyStatePriorityQueue : public StatePriorityQueue { class DynamicPenaltyStatePriorityQueue : public StatePriorityQueue {
public: public:
@ -104,7 +72,7 @@ namespace storm {
virtual bool hasNextState() const override; virtual bool hasNextState() const override;
virtual storm::storage::sparse::state_type popNextState() 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<ValueType> const& oneStepProbabilities) override;
virtual void update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) override;
virtual std::size_t size() const override; virtual std::size_t size() const override;
private: private:
@ -117,38 +85,36 @@ namespace storm {
static std::vector<ValueType> computeReachabilityValues(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& values, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& oneStepProbabilitiesToTarget); static std::vector<ValueType> computeReachabilityValues(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& values, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& oneStepProbabilitiesToTarget);
static std::unique_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& stateDistances, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& states);
static std::unique_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& stateDistances, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& states);
static std::unique_ptr<StatePriorityQueue> createNaivePriorityQueue(storm::storage::BitVector const& states); static std::unique_ptr<StatePriorityQueue> createNaivePriorityQueue(storm::storage::BitVector const& states);
static void performPrioritizedStateElimination(std::unique_ptr<StatePriorityQueue>& priorityQueue, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, std::vector<ValueType>& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly);
static void performPrioritizedStateElimination(std::unique_ptr<StatePriorityQueue>& priorityQueue, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& 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<ValueType>& values, boost::optional<std::vector<ValueType>>& additionalStateValues, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities);
static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<ValueType>>& additionalStateValues, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities);
static void performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities);
static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities);
static uint_fast64_t performHybridStateElimination(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities);
static uint_fast64_t performHybridStateElimination(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities);
static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector<ValueType>& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities = boost::none);
static uint_fast64_t treatScc(storm::storage::FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities = boost::none);
static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne = false);
typedef std::function<void (storm::storage::sparse::state_type const& state, ValueType const& loopProbability)> ValueUpdateCallback; typedef std::function<void (storm::storage::sparse::state_type const& state, ValueType const& loopProbability)> ValueUpdateCallback;
typedef std::function<void (storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state)> PredecessorUpdateCallback; typedef std::function<void (storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state)> PredecessorUpdateCallback;
typedef std::function<void (storm::storage::sparse::state_type const& state)> PriorityUpdateCallback; typedef std::function<void (storm::storage::sparse::state_type const& state)> PriorityUpdateCallback;
typedef std::function<bool (storm::storage::sparse::state_type const& state)> PredecessorFilterCallback; typedef std::function<bool (storm::storage::sparse::state_type const& state)> PredecessorFilterCallback;
static void eliminateState(storm::storage::sparse::state_type state, FlexibleSparseMatrix& matrix, FlexibleSparseMatrix& backwardTransitions, ValueUpdateCallback const& valueUpdateCallback, PredecessorUpdateCallback const& predecessorCallback, boost::optional<PriorityUpdateCallback> const& priorityUpdateCallback = boost::none, boost::optional<PredecessorFilterCallback> const& predecessorFilterCallback = boost::none, bool removeForwardTransitions = true);
static void eliminateState(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix<ValueType>& matrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, ValueUpdateCallback const& valueUpdateCallback, PredecessorUpdateCallback const& predecessorCallback, boost::optional<PriorityUpdateCallback> const& priorityUpdateCallback = boost::none, boost::optional<PredecessorFilterCallback> const& predecessorFilterCallback = boost::none, bool removeForwardTransitions = true);
static std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities, bool forward, bool reverse); static std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities, bool forward, bool reverse);
static std::vector<std::size_t> getStateDistances(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities, bool forward); static std::vector<std::size_t> getStateDistances(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities, bool forward);
static uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities);
static uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities);
static uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities);
static uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities);
static bool checkConsistent(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions);
static bool checkConsistent(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions);
// A flag that indicates whether this model checker is supposed to produce results for all states or just for the initial states. // A flag that indicates whether this model checker is supposed to produce results for all states or just for the initial states.
bool computeResultsForInitialStatesOnly; bool computeResultsForInitialStatesOnly;

114
src/storage/FlexibleSparseMatrix.cpp
View File

@ -2,14 +2,35 @@
#include "src/storage/SparseMatrix.h" #include "src/storage/SparseMatrix.h"
#include "src/storage/BitVector.h" #include "src/storage/BitVector.h"
#include "src/adapters/CarlAdapter.h"
#include "src/utility/constants.h"
namespace storm { namespace storm {
namespace storage { namespace storage {
template<typename ValueType> template<typename ValueType>
FlexibleSparseMatrix<ValueType>::FlexibleSparseMatrix(index_type rows) : data(rows) {
FlexibleSparseMatrix<ValueType>::FlexibleSparseMatrix(index_type rows) : data(rows), columnCount(0), nonzeroEntryCount(0) {
// Intentionally left empty. // Intentionally left empty.
} }
template<typename ValueType>
FlexibleSparseMatrix<ValueType>::FlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> 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<ValueType>::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<ValueType>());
} else {
getRow(rowIndex).emplace_back(element);
}
}
}
}
template<typename ValueType> template<typename ValueType>
void FlexibleSparseMatrix<ValueType>::reserveInRow(index_type row, index_type numberOfElements) { void FlexibleSparseMatrix<ValueType>::reserveInRow(index_type row, index_type numberOfElements) {
this->data[row].reserve(numberOfElements); this->data[row].reserve(numberOfElements);
@ -26,35 +47,33 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
typename FlexibleSparseMatrix<ValueType>::index_type FlexibleSparseMatrix<ValueType>::getNumberOfRows() const {
typename FlexibleSparseMatrix<ValueType>::index_type FlexibleSparseMatrix<ValueType>::getRowCount() const {
return this->data.size(); return this->data.size();
} }
template<typename ValueType> template<typename ValueType>
bool FlexibleSparseMatrix<ValueType>::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<ValueType>::index_type FlexibleSparseMatrix<ValueType>::getColumnCount() const {
return columnCount;
} }
template<typename ValueType> template<typename ValueType>
void FlexibleSparseMatrix<ValueType>::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<ValueType>::index_type FlexibleSparseMatrix<ValueType>::getNonzeroEntryCount() const {
return nonzeroEntryCount;
}
template<typename ValueType>
void FlexibleSparseMatrix<ValueType>::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<typename ValueType> template<typename ValueType>
bool FlexibleSparseMatrix<ValueType>::empty() const { bool FlexibleSparseMatrix<ValueType>::empty() const {
for (auto const& row : this->data) { for (auto const& row : this->data) {
@ -64,25 +83,68 @@ namespace storm {
} }
return true; return true;
} }
template<typename ValueType> template<typename ValueType>
void FlexibleSparseMatrix<ValueType>::filter(storm::storage::BitVector const& rowFilter, storm::storage::BitVector const& columnFilter) {
void FlexibleSparseMatrix<ValueType>::createSubmatrix(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) {
for (uint_fast64_t rowIndex = 0; rowIndex < this->data.size(); ++rowIndex) { for (uint_fast64_t rowIndex = 0; rowIndex < this->data.size(); ++rowIndex) {
auto& row = this->data[rowIndex]; auto& row = this->data[rowIndex];
if (!rowFilter.get(rowIndex)) {
if (!rowConstraint.get(rowIndex)) {
row.clear(); row.clear();
row.shrink_to_fit(); row.shrink_to_fit();
continue; continue;
} }
row_type newRow; row_type newRow;
for (auto const& element : row) { for (auto const& element : row) {
if (columnFilter.get(element.getColumn())) {
if (columnConstraint.get(element.getColumn())) {
newRow.push_back(element); newRow.push_back(element);
} }
} }
row = std::move(newRow); row = std::move(newRow);
} }
} }
template<typename ValueType>
storm::storage::SparseMatrix<ValueType> FlexibleSparseMatrix<ValueType>::createSparseMatrix() {
storm::storage::SparseMatrixBuilder<ValueType> 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<typename ValueType>
bool FlexibleSparseMatrix<ValueType>::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<typename ValueType>
std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<ValueType> 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<double>;
#ifdef STORM_HAVE_CARL
template class FlexibleSparseMatrix<storm::RationalFunction>;
#endif
}
}
} // namespace storage
} // namespace storm

115
src/storage/FlexibleSparseMatrix.h
View File

@ -5,6 +5,7 @@
#include <vector> #include <vector>
#include "src/storage/sparse/StateType.h" #include "src/storage/sparse/StateType.h"
#include "src/storage/SparseMatrix.h"
namespace storm { namespace storm {
namespace storage { namespace storage {
@ -13,17 +14,14 @@ namespace storm {
class BitVector; class BitVector;
/*!
* The flexible sparse matrix is used during state elimination.
*/
template<typename ValueType> template<typename ValueType>
class FlexibleSparseMatrix { class FlexibleSparseMatrix {
public: public:
// TODO: make this class a bit more consistent with the big sparse matrix and improve it: // 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 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 // * add stuff like clearRow, multiplyRowWithScalar
typedef uint_fast64_t index_type; typedef uint_fast64_t index_type;
@ -32,32 +30,113 @@ namespace storm {
typedef typename row_type::iterator iterator; typedef typename row_type::iterator iterator;
typedef typename row_type::const_iterator const_iterator; typedef typename row_type::const_iterator const_iterator;
/*!
* Constructs an empty flexible sparse matrix.
*/
FlexibleSparseMatrix() = default; FlexibleSparseMatrix() = default;
/*!
* Constructs a flexible sparse matrix with rows many rows.
* @param rows number of rows.
*/
FlexibleSparseMatrix(index_type 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<ValueType> 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); 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); 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; 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; 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<ValueType> createSparseMatrix();
/*! /*!
* Checks whether the given state has a self-loop with an arbitrary probability in the probability matrix. * 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. * @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. * @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<typename TPrime>
friend std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<TPrime> const& matrix);
private: private:
std::vector<row_type> data; std::vector<row_type> data;
// The number of columns of the matrix.
index_type columnCount;
// The number of entries in the matrix.
index_type nonzeroEntryCount;
}; };
} }
} }

Write Preview
Loading…
Cancel
Save