From 7a10a04cde5e8a9f8ada836449b08ae4462eff2a Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 12 Feb 2016 13:18:04 +0100 Subject: [PATCH] Created StateEliminator with specialized subclasses Former-commit-id: 991e3fcfcdb061fbd1f9689692ea60faf48a1958 --- .../SparseDtmcEliminationModelChecker.cpp | 326 ++---------------- .../SparseDtmcEliminationModelChecker.h | 41 +-- .../ConditionalEliminator.cpp | 53 +++ .../stateelimination/ConditionalEliminator.h | 53 +++ .../LongRunAverageEliminator.cpp | 47 +++ .../LongRunAverageEliminator.h | 36 ++ .../PrioritizedEliminator.cpp | 45 +++ .../stateelimination/PrioritizedEliminator.h | 34 ++ .../stateelimination/StateEliminator.cpp | 259 ++++++++++++++ src/solver/stateelimination/StateEliminator.h | 42 +++ 10 files changed, 626 insertions(+), 310 deletions(-) create mode 100644 src/solver/stateelimination/ConditionalEliminator.cpp create mode 100644 src/solver/stateelimination/ConditionalEliminator.h create mode 100644 src/solver/stateelimination/LongRunAverageEliminator.cpp create mode 100644 src/solver/stateelimination/LongRunAverageEliminator.h create mode 100644 src/solver/stateelimination/PrioritizedEliminator.cpp create mode 100644 src/solver/stateelimination/PrioritizedEliminator.h create mode 100644 src/solver/stateelimination/StateEliminator.cpp create mode 100644 src/solver/stateelimination/StateEliminator.h diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 0b520c168..e01987f3f 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -25,6 +25,10 @@ #include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/IllegalArgumentException.h" +#include "src/solver/stateelimination/LongRunAverageEliminator.h" +#include "src/solver/stateelimination/ConditionalEliminator.h" +#include "src/solver/stateelimination/PrioritizedEliminator.h" + namespace storm { namespace modelchecker { @@ -300,30 +304,13 @@ namespace storm { std::vector averageTimeInStates(stateValues.size(), storm::utility::one()); // First, we eliminate all states in BSCCs (except for the representative states). - { - std::unique_ptr priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs); - - ValueUpdateCallback valueUpdateCallback = [&stateValues,&averageTimeInStates] (storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { - stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]); - averageTimeInStates[state] = storm::utility::simplify(loopProbability * averageTimeInStates[state]); - }; - - PredecessorUpdateCallback predecessorCallback = [&stateValues,&averageTimeInStates] (storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { - stateValues[predecessor] = storm::utility::simplify(stateValues[predecessor] + storm::utility::simplify(probability * stateValues[state])); - averageTimeInStates[predecessor] = storm::utility::simplify(averageTimeInStates[predecessor] + storm::utility::simplify(probability * averageTimeInStates[state])); - }; - - boost::optional priorityUpdateCallback = PriorityUpdateCallback([&flexibleMatrix,&flexibleBackwardTransitions,&stateValues,&priorityQueue] (storm::storage::sparse::state_type const& state) { - priorityQueue->update(state, flexibleMatrix, flexibleBackwardTransitions, stateValues); - }); - - boost::optional predecessorFilterCallback = boost::none; - - while (priorityQueue->hasNextState()) { - storm::storage::sparse::state_type state = priorityQueue->popNextState(); - eliminateState(state, flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorCallback, priorityUpdateCallback, predecessorFilterCallback, true); - STORM_LOG_ASSERT(checkConsistent(flexibleMatrix, flexibleBackwardTransitions), "The forward and backward transition matrices became inconsistent."); - } + std::unique_ptr> priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs); + storm::solver::stateelimination::LongRunAverageEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, *priorityQueue, stateValues, averageTimeInStates); + + while (priorityQueue->hasNextState()) { + storm::storage::sparse::state_type state = priorityQueue->popNextState(); + stateEliminator.eliminateState(state, true); + STORM_LOG_ASSERT(checkConsistent(flexibleMatrix, flexibleBackwardTransitions), "The forward and backward transition matrices became inconsistent."); } // Now, we set the values of all states in BSCCs to that of the representative value (and clear the @@ -743,7 +730,7 @@ namespace storm { 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); + std::unique_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); STORM_LOG_INFO("Computing conditional probilities." << std::endl); std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); @@ -752,15 +739,11 @@ namespace storm { performPrioritizedStateElimination(statePriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, this->getModel().getInitialStates(), true); STORM_LOG_INFO("Eliminated " << numberOfStatesToEliminate << " states." << std::endl); - // Prepare some callbacks for the elimination procedure. - ValueUpdateCallback valueUpdateCallback = [&oneStepProbabilities] (storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { oneStepProbabilities[state] = storm::utility::simplify(loopProbability * oneStepProbabilities[state]); }; - PredecessorUpdateCallback predecessorUpdateCallback = [&oneStepProbabilities] (storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { oneStepProbabilities[predecessor] = storm::utility::simplify(oneStepProbabilities[predecessor] * storm::utility::simplify(probability * oneStepProbabilities[state])); }; - boost::optional phiFilterCallback = PredecessorFilterCallback([&phiStates] (storm::storage::sparse::state_type const& state) { return phiStates.get(state); }); - boost::optional psiFilterCallback = PredecessorFilterCallback([&psiStates] (storm::storage::sparse::state_type const& state) { return psiStates.get(state); }); + storm::solver::stateelimination::ConditionalEliminator stateEliminator = storm::solver::stateelimination::ConditionalEliminator(flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, phiStates, psiStates); // Eliminate the transitions going into the initial state (if there are any). if (!flexibleBackwardTransitions.getRow(*newInitialStates.begin()).empty()) { - eliminateState(*newInitialStates.begin(), flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorUpdateCallback, boost::none, boost::none, false); + stateEliminator.eliminateState(*newInitialStates.begin(), false); } // Now we need to basically eliminate all chains of not-psi states after phi states and chains of not-phi @@ -795,7 +778,9 @@ namespace storm { // 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."); - eliminateState(element.getColumn(), flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorUpdateCallback, boost::none, phiFilterCallback, false); + stateEliminator.setStatePhi(); + stateEliminator.eliminateState(element.getColumn(), false); + stateEliminator.clearState(); hasNonPsiSuccessor = true; } } @@ -824,7 +809,9 @@ namespace storm { 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); + stateEliminator.setStatePsi(); + stateEliminator.eliminateState(element.getColumn(), false); + stateEliminator.clearState(); hasNonPhiSuccessor = true; } } @@ -890,7 +877,7 @@ namespace storm { } template - 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) { + std::unique_ptr> 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); @@ -934,23 +921,20 @@ namespace storm { } template - std::unique_ptr::StatePriorityQueue> SparseDtmcEliminationModelChecker::createNaivePriorityQueue(storm::storage::BitVector const& states) { + std::unique_ptr> SparseDtmcEliminationModelChecker::createNaivePriorityQueue(storm::storage::BitVector const& states) { std::vector sortedStates(states.begin(), states.end()); - return std::unique_ptr(new StaticStatePriorityQueue(sortedStates)); + return std::unique_ptr>(new StaticStatePriorityQueue(sortedStates)); } template - 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) { + 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])); }; - boost::optional priorityUpdateCallback = PriorityUpdateCallback([&transitionMatrix,&backwardTransitions,&values,&priorityQueue] (storm::storage::sparse::state_type const& state) { priorityQueue->update(state, transitionMatrix, backwardTransitions, values); }); - boost::optional predecessorFilterCallback = boost::none; + storm::solver::stateelimination::PrioritizedEliminator stateEliminator(transitionMatrix, backwardTransitions, *priorityQueue, values); while (priorityQueue->hasNextState()) { storm::storage::sparse::state_type state = priorityQueue->popNextState(); bool removeForwardTransitions = computeResultsForInitialStatesOnly && !initialStates.get(state); - eliminateState(state, transitionMatrix, backwardTransitions, valueUpdateCallback, predecessorCallback, priorityUpdateCallback, predecessorFilterCallback, removeForwardTransitions); + stateEliminator.eliminateState(state, removeForwardTransitions); if (removeForwardTransitions) { values[state] = storm::utility::zero(); } @@ -960,7 +944,7 @@ namespace storm { template 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::unique_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); std::size_t numberOfStatesToEliminate = statePriorities->size(); STORM_LOG_DEBUG("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl); @@ -979,7 +963,7 @@ namespace storm { if (storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet()) { STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); std::vector sortedStates(entryStateQueue.begin(), entryStateQueue.end()); - std::unique_ptr queuePriorities = std::unique_ptr(new StaticStatePriorityQueue(sortedStates)); + std::unique_ptr> queuePriorities = std::unique_ptr>(new StaticStatePriorityQueue(sortedStates)); performPrioritizedStateElimination(queuePriorities, transitionMatrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); } STORM_LOG_DEBUG("Eliminated " << subsystem.size() << " states." << std::endl); @@ -1078,7 +1062,7 @@ namespace storm { } } - std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs); + std::unique_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs); STORM_LOG_TRACE("Eliminating " << statePriorities->size() << " trivial SCCs."); performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated all trivial SCCs."); @@ -1108,7 +1092,7 @@ namespace storm { } else { // In this case, we perform simple state elimination in the current SCC. STORM_LOG_TRACE("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly."); - std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates); + std::unique_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates); performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated all states of SCC."); } @@ -1116,7 +1100,7 @@ namespace storm { // Finally, eliminate the entry states (if we are required to do so). if (eliminateEntryStates) { STORM_LOG_TRACE("Finally, eliminating entry states."); - std::unique_ptr naivePriorities = createNaivePriorityQueue(entryStates); + std::unique_ptr> naivePriorities = createNaivePriorityQueue(entryStates); performPrioritizedStateElimination(naivePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated/added entry states."); } else { @@ -1129,242 +1113,6 @@ namespace storm { return maximalDepth; } - template - 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(); - FlexibleRowType& currentStateSuccessors = matrix.getRow(state); - for (auto entryIt = currentStateSuccessors.begin(), entryIte = currentStateSuccessors.end(); entryIt != entryIte; ++entryIt) { - if (entryIt->getColumn() >= state) { - if (entryIt->getColumn() == state) { - loopProbability = entryIt->getValue(); - hasSelfLoop = true; - - // If we do not clear the forward transitions completely, we need to remove the self-loop, - // because we scale all the other outgoing transitions with it anyway. - if (!removeForwardTransitions) { - currentStateSuccessors.erase(entryIt); - } - } - break; - } - } - - // Scale all entries in this row with (1 / (1 - loopProbability)) only in case there was a self-loop. - STORM_LOG_TRACE((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop.")); - if (hasSelfLoop) { - STORM_LOG_ASSERT(loopProbability != storm::utility::one(), "Must not eliminate state with probability 1 self-loop."); - loopProbability = storm::utility::simplify(storm::utility::one() / (storm::utility::one() - loopProbability)); - for (auto& entry : matrix.getRow(state)) { - // Only scale the non-diagonal entries. - if (entry.getColumn() != state) { - entry.setValue(storm::utility::simplify(entry.getValue() * loopProbability)); - } - } - callback(state, loopProbability); - } - - // Now connect the predecessors of the state being eliminated with its successors. - FlexibleRowType& currentStatePredecessors = backwardTransitions.getRow(state); - - // In case we have a constrained elimination, we need to keep track of the new predecessors. - FlexibleRowType newCurrentStatePredecessors; - - std::vector newBackwardProbabilities(currentStateSuccessors.size()); - for (auto& backwardProbabilities : newBackwardProbabilities) { - backwardProbabilities.reserve(currentStatePredecessors.size()); - } - - // Now go through the predecessors and eliminate the ones (satisfying the constraint if given). - for (auto const& predecessorEntry : currentStatePredecessors) { - uint_fast64_t predecessor = predecessorEntry.getColumn(); - STORM_LOG_TRACE("Found predecessor " << predecessor << "."); - - // Skip the state itself as one of its predecessors. - if (predecessor == state) { - assert(hasSelfLoop); - continue; - } - - // Skip the state if the elimination is constrained, but the predecessor is not in the constraint. - if (predecessorFilterCallback && !predecessorFilterCallback.get()(predecessor)) { - newCurrentStatePredecessors.emplace_back(predecessorEntry); - STORM_LOG_TRACE("Not eliminating predecessor " << predecessor << ", because it does not fit the filter."); - continue; - } - STORM_LOG_TRACE("Eliminating predecessor " << predecessor << "."); - - // 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. - 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."); - ValueType multiplyFactor = multiplyElement->getValue(); - multiplyElement->setValue(storm::utility::zero()); - - // At this point, we need to update the (forward) transitions of the predecessor. - FlexibleRowIterator first1 = predecessorForwardTransitions.begin(); - FlexibleRowIterator last1 = predecessorForwardTransitions.end(); - FlexibleRowIterator first2 = currentStateSuccessors.begin(); - FlexibleRowIterator last2 = currentStateSuccessors.end(); - - FlexibleRowType newSuccessors; - newSuccessors.reserve((last1 - first1) + (last2 - first2)); - 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). - for (; first1 != last1; ++result) { - // Skip the transitions to the state that is currently being eliminated. - if (first1->getColumn() == state || (first2 != last2 && first2->getColumn() == state)) { - if (first1->getColumn() == state) { - ++first1; - } - if (first2 != last2 && first2->getColumn() == state) { - ++first2; - } - continue; - } - - if (first2 == last2) { - 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()) { - auto successorEntry = storm::utility::simplify(std::move(*first2 * multiplyFactor)); - *result = successorEntry; - newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, successorEntry.getValue()); -// std::cout << "(1) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; - ++first2; - ++successorOffsetInNewBackwardTransitions; - } else if (first1->getColumn() < first2->getColumn()) { - *result = *first1; - ++first1; - } else { - auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue())); - *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; - ++first2; - ++successorOffsetInNewBackwardTransitions; - } - } - for (; first2 != last2; ++first2) { - if (first2->getColumn() != state) { - auto stateProbability = storm::utility::simplify(std::move(*first2 * multiplyFactor)); - *result = stateProbability; - newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, stateProbability.getValue()); -// std::cout << "(3) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; - ++successorOffsetInNewBackwardTransitions; - } - } - - // Now move the new transitions in place. - predecessorForwardTransitions = std::move(newSuccessors); - STORM_LOG_TRACE("Fixed new next-state probabilities of predecessor state " << predecessor << "."); - - predecessorCallback(predecessor, multiplyFactor, state); - - if (priorityUpdateCallback) { - STORM_LOG_TRACE("Updating priority of predecessor."); - priorityUpdateCallback.get()(predecessor); - } - } - - // Finally, we need to add the predecessor to the set of predecessors of every successor. - uint_fast64_t successorOffsetInNewBackwardTransitions = 0; - for (auto const& successorEntry : currentStateSuccessors) { - if (successorEntry.getColumn() == state) { - continue; - } - - 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; -// } - - // 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) { - 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); - } - - 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; -// } - - FlexibleRowType newPredecessors; - newPredecessors.reserve((last1 - first1) + (last2 - first2)); - std::insert_iterator result(newPredecessors, newPredecessors.end()); - - for (; first1 != last1; ++result) { - if (first2 == last2) { - std::copy(first1, last1, result); - break; - } - if (first2->getColumn() < first1->getColumn()) { - if (first2->getColumn() != state) { - *result = *first2; - } - ++first2; - } else if (first1->getColumn() == first2->getColumn()) { - if (estimateComplexity(first1->getValue()) > estimateComplexity(first2->getValue())) { - *result = *first1; - } else { - *result = *first2; - } - ++first1; - ++first2; - } else { - *result = *first1; - ++first1; - } - } - if (predecessorFilterCallback) { - 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::index_type, typename storm::storage::FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; }); - } - - // Now move the new predecessors in place. - successorBackwardTransitions = std::move(newPredecessors); -// std::cout << "new backward trans of " << successorEntry.getColumn() << std::endl; -// for (auto const& trans : successorBackwardTransitions) { -// std::cout << trans << std::endl; -// } - ++successorOffsetInNewBackwardTransitions; - } - STORM_LOG_TRACE("Fixed predecessor lists of successor states."); - - if (removeForwardTransitions) { - // Clear the eliminated row to reduce memory consumption. - currentStateSuccessors.clear(); - currentStateSuccessors.shrink_to_fit(); - } - if (predecessorFilterCallback) { - currentStatePredecessors = std::move(newCurrentStatePredecessors); - } else { - currentStatePredecessors.clear(); - currentStatePredecessors.shrink_to_fit(); - } - } - template std::vector SparseDtmcEliminationModelChecker::getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse) { std::vector statePriorities(transitionMatrix.getRowCount()); @@ -1444,13 +1192,13 @@ namespace storm { return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size(); } - template - void SparseDtmcEliminationModelChecker::StatePriorityQueue::update(storm::storage::sparse::state_type, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + template + void StatePriorityQueue::update(storm::storage::sparse::state_type, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { // Intentionally left empty. } template - SparseDtmcEliminationModelChecker::StaticStatePriorityQueue::StaticStatePriorityQueue(std::vector const& sortedStates) : StatePriorityQueue(), sortedStates(sortedStates), currentPosition(0) { + SparseDtmcEliminationModelChecker::StaticStatePriorityQueue::StaticStatePriorityQueue(std::vector const& sortedStates) : StatePriorityQueue(), sortedStates(sortedStates), currentPosition(0) { // Intentionally left empty. } @@ -1471,7 +1219,7 @@ namespace storm { } template - SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::DynamicPenaltyStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, PenaltyFunctionType const& penaltyFunction) : StatePriorityQueue(), priorityQueue(), stateToPriorityMapping(), penaltyFunction(penaltyFunction) { + SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::DynamicPenaltyStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, PenaltyFunctionType const& penaltyFunction) : StatePriorityQueue(), priorityQueue(), stateToPriorityMapping(), penaltyFunction(penaltyFunction) { // Insert all state-penalty pairs into our priority queue. for (auto const& statePenalty : sortedStatePenaltyPairs) { priorityQueue.insert(priorityQueue.end(), statePenalty); @@ -1552,9 +1300,11 @@ namespace storm { return true; } + template class StatePriorityQueue; template class SparseDtmcEliminationModelChecker>; - + #ifdef STORM_HAVE_CARL + template class StatePriorityQueue; template class SparseDtmcEliminationModelChecker>; #endif } // namespace modelchecker diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 30c8e528a..bfcfbcd31 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -10,6 +10,18 @@ namespace storm { namespace modelchecker { + template + uint_fast64_t estimateComplexity(ValueType const& value); + + template + 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, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + virtual std::size_t size() const = 0; + }; + template class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker { public: @@ -34,18 +46,10 @@ namespace storm { virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - + private: - - 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, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); - virtual std::size_t size() const = 0; - }; - class StaticStatePriorityQueue : public StatePriorityQueue { + class StaticStatePriorityQueue : public StatePriorityQueue { public: StaticStatePriorityQueue(std::vector const& sortedStates); @@ -66,7 +70,7 @@ namespace storm { typedef std::function const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities)> PenaltyFunctionType; - class DynamicPenaltyStatePriorityQueue : public StatePriorityQueue { + class DynamicPenaltyStatePriorityQueue : public StatePriorityQueue { public: DynamicPenaltyStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, PenaltyFunctionType const& penaltyFunction); @@ -85,11 +89,11 @@ 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, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::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 std::unique_ptr> createNaivePriorityQueue(storm::storage::BitVector const& states); - 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 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(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); @@ -98,14 +102,7 @@ namespace storm { 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(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); - - 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, 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); diff --git a/src/solver/stateelimination/ConditionalEliminator.cpp b/src/solver/stateelimination/ConditionalEliminator.cpp new file mode 100644 index 000000000..bba964596 --- /dev/null +++ b/src/solver/stateelimination/ConditionalEliminator.cpp @@ -0,0 +1,53 @@ +#include "src/solver/stateelimination/ConditionalEliminator.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + ConditionalEliminator::ConditionalEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector& phiStates, storm::storage::BitVector& psiStates) : StateEliminator(transitionMatrix, backwardTransitions), oneStepProbabilities(oneStepProbabilities), phiStates(phiStates), psiStates(psiStates), specificState(NONE) { + } + + template + void ConditionalEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { + oneStepProbabilities[state] = storm::utility::simplify(loopProbability * oneStepProbabilities[state]); + } + + template + void ConditionalEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { + oneStepProbabilities[predecessor] = storm::utility::simplify(oneStepProbabilities[predecessor] * storm::utility::simplify(probability * oneStepProbabilities[state])); + } + + template + void ConditionalEliminator::updatePriority(storm::storage::sparse::state_type const& state) { + // Do nothing + } + + template + bool ConditionalEliminator::filterPredecessor(storm::storage::sparse::state_type const& state) { + // TODO find better solution than flag + switch (specificState) { + case PHI: + return phiStates.get(state); + case PSI: + return psiStates.get(state); + case NONE: + assert(false); + } + } + + template + bool ConditionalEliminator::isFilterPredecessor() const { + return true; + } + + + template class ConditionalEliminator>; + +#ifdef STORM_HAVE_CARL + template class ConditionalEliminator>; +#endif + + } // namespace stateelimination + } // namespace storage +} // namespace storm diff --git a/src/solver/stateelimination/ConditionalEliminator.h b/src/solver/stateelimination/ConditionalEliminator.h new file mode 100644 index 000000000..b98066d3f --- /dev/null +++ b/src/solver/stateelimination/ConditionalEliminator.h @@ -0,0 +1,53 @@ +#ifndef STORM_SOLVER_STATEELIMINATION_CONDITIONALELIMINATOR_H_ +#define STORM_SOLVER_STATEELIMINATION_CONDITIONALELIMINATOR_H_ + +#include "src/solver/stateelimination/StateEliminator.h" + +#include "src/storage/BitVector.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + class ConditionalEliminator : public StateEliminator { + + typedef typename SparseModelType::ValueType ValueType; + + enum SpecificState { NONE, PHI, PSI}; + + public: + ConditionalEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector& phiStates, storm::storage::BitVector& psiStates); + + // Instantiaton of Virtual methods + void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override; + void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override; + void updatePriority(storm::storage::sparse::state_type const& state) override; + bool filterPredecessor(storm::storage::sparse::state_type const& state) override; + bool isFilterPredecessor() const override; + + void setStatePsi() { + specificState = PSI; + } + + void setStatePhi() { + specificState = PHI; + } + + void clearState() { + specificState = NONE; + } + + private: + std::vector& oneStepProbabilities; + storm::storage::BitVector& phiStates; + storm::storage::BitVector& psiStates; + SpecificState specificState; + + }; + + } // namespace stateelimination + } // namespace storage +} // namespace storm + +#endif // STORM_SOLVER_STATEELIMINATION_CONDITIONALELIMINATOR_H_ diff --git a/src/solver/stateelimination/LongRunAverageEliminator.cpp b/src/solver/stateelimination/LongRunAverageEliminator.cpp new file mode 100644 index 000000000..250030c54 --- /dev/null +++ b/src/solver/stateelimination/LongRunAverageEliminator.cpp @@ -0,0 +1,47 @@ +#include "src/solver/stateelimination/LongRunAverageEliminator.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + LongRunAverageEliminator::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::modelchecker::StatePriorityQueue& priorityQueue, std::vector& stateValues, std::vector& averageTimeInStates) : StateEliminator(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues), averageTimeInStates(averageTimeInStates) { + } + + template + void LongRunAverageEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { + stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]); + averageTimeInStates[state] = storm::utility::simplify(loopProbability * averageTimeInStates[state]); + } + + template + void LongRunAverageEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { + stateValues[predecessor] = storm::utility::simplify(stateValues[predecessor] + storm::utility::simplify(probability * stateValues[state])); + averageTimeInStates[predecessor] = storm::utility::simplify(averageTimeInStates[predecessor] + storm::utility::simplify(probability * averageTimeInStates[state])); + } + + template + void LongRunAverageEliminator::updatePriority(storm::storage::sparse::state_type const& state) { + priorityQueue.update(state, StateEliminator::transitionMatrix, StateEliminator::backwardTransitions, stateValues); + } + + template + bool LongRunAverageEliminator::filterPredecessor(storm::storage::sparse::state_type const& state) { + assert(false); + } + + template + bool LongRunAverageEliminator::isFilterPredecessor() const { + return false; + } + + + template class LongRunAverageEliminator>; + +#ifdef STORM_HAVE_CARL + template class LongRunAverageEliminator>; +#endif + + } // namespace stateelimination + } // namespace storage +} // namespace storm diff --git a/src/solver/stateelimination/LongRunAverageEliminator.h b/src/solver/stateelimination/LongRunAverageEliminator.h new file mode 100644 index 000000000..0e5522fef --- /dev/null +++ b/src/solver/stateelimination/LongRunAverageEliminator.h @@ -0,0 +1,36 @@ +#ifndef STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_ +#define STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_ + +#include "src/solver/stateelimination/StateEliminator.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + class LongRunAverageEliminator : public StateEliminator { + + typedef typename SparseModelType::ValueType ValueType; + + public: + LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::modelchecker::StatePriorityQueue& priorityQueue, std::vector& stateValues, std::vector& averageTimeInStates); + + // Instantiaton of Virtual methods + void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override; + void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override; + void updatePriority(storm::storage::sparse::state_type const& state) override; + bool filterPredecessor(storm::storage::sparse::state_type const& state) override; + bool isFilterPredecessor() const override; + + private: + + storm::modelchecker::StatePriorityQueue& priorityQueue; + std::vector& stateValues; + std::vector& averageTimeInStates; + }; + + } // namespace stateelimination + } // namespace storage +} // namespace storm + +#endif // STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_ diff --git a/src/solver/stateelimination/PrioritizedEliminator.cpp b/src/solver/stateelimination/PrioritizedEliminator.cpp new file mode 100644 index 000000000..de760e66b --- /dev/null +++ b/src/solver/stateelimination/PrioritizedEliminator.cpp @@ -0,0 +1,45 @@ +#include "src/solver/stateelimination/PrioritizedEliminator.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + PrioritizedEliminator::PrioritizedEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::modelchecker::StatePriorityQueue priorityQueue, std::vector& stateValues) : StateEliminator(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) { + } + + template + void PrioritizedEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { + stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]); + } + + template + void PrioritizedEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { + stateValues[predecessor] = storm::utility::simplify(stateValues[predecessor] + storm::utility::simplify(probability * stateValues[state])); + } + + template + void PrioritizedEliminator::updatePriority(storm::storage::sparse::state_type const& state) { + priorityQueue.update(state, StateEliminator::transitionMatrix, StateEliminator::backwardTransitions, stateValues); + } + + template + bool PrioritizedEliminator::filterPredecessor(storm::storage::sparse::state_type const& state) { + assert(false); + } + + template + bool PrioritizedEliminator::isFilterPredecessor() const { + return false; + } + + + template class PrioritizedEliminator>; + +#ifdef STORM_HAVE_CARL + template class PrioritizedEliminator>; +#endif + + } // namespace stateelimination + } // namespace storage +} // namespace storm diff --git a/src/solver/stateelimination/PrioritizedEliminator.h b/src/solver/stateelimination/PrioritizedEliminator.h new file mode 100644 index 000000000..7a242ebdf --- /dev/null +++ b/src/solver/stateelimination/PrioritizedEliminator.h @@ -0,0 +1,34 @@ +#ifndef STORM_SOLVER_STATEELIMINATION_PRIORITIZEDELIMINATOR_H_ +#define STORM_SOLVER_STATEELIMINATION_PRIORITIZEDELIMINATOR_H_ + +#include "src/solver/stateelimination/StateEliminator.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + class PrioritizedEliminator : public StateEliminator { + + typedef typename SparseModelType::ValueType ValueType; + + public: + PrioritizedEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::modelchecker::StatePriorityQueue priorityQueue, std::vector& stateValues); + + // Instantiaton of Virtual methods + void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override; + void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override; + void updatePriority(storm::storage::sparse::state_type const& state) override; + bool filterPredecessor(storm::storage::sparse::state_type const& state) override; + bool isFilterPredecessor() const override; + + private: + storm::modelchecker::StatePriorityQueue& priorityQueue; + std::vector& stateValues; + }; + + } // namespace stateelimination + } // namespace storage +} // namespace storm + +#endif // STORM_SOLVER_STATEELIMINATION_PRIORITIZEDELIMINATOR_H_ diff --git a/src/solver/stateelimination/StateEliminator.cpp b/src/solver/stateelimination/StateEliminator.cpp new file mode 100644 index 000000000..3e3d8c53a --- /dev/null +++ b/src/solver/stateelimination/StateEliminator.cpp @@ -0,0 +1,259 @@ +#include "src/solver/stateelimination/StateEliminator.h" + +#include "src/storage/BitVector.h" +#include "src/adapters/CarlAdapter.h" +#include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidStateException.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + StateEliminator::StateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions) : transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions) { + } + + template + void StateEliminator::eliminateState(storm::storage::sparse::state_type state, bool removeForwardTransitions, storm::storage::BitVector predecessorConstraint) { + + STORM_LOG_TRACE("Eliminating state " << state << "."); + + // Start by finding loop probability. + bool hasSelfLoop = false; + ValueType loopProbability = storm::utility::zero(); + FlexibleRowType& currentStateSuccessors = transitionMatrix.getRow(state); + for (auto entryIt = currentStateSuccessors.begin(), entryIte = currentStateSuccessors.end(); entryIt != entryIte; ++entryIt) { + if (entryIt->getColumn() >= state) { + if (entryIt->getColumn() == state) { + loopProbability = entryIt->getValue(); + hasSelfLoop = true; + + // If we do not clear the forward transitions completely, we need to remove the self-loop, + // because we scale all the other outgoing transitions with it anyway. + if (!removeForwardTransitions) { + currentStateSuccessors.erase(entryIt); + } + } + break; + } + } + + // Scale all entries in this row with (1 / (1 - loopProbability)) only in case there was a self-loop. + STORM_LOG_TRACE((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop.")); + if (hasSelfLoop) { + STORM_LOG_ASSERT(loopProbability != storm::utility::one(), "Must not eliminate state with probability 1 self-loop."); + loopProbability = storm::utility::simplify(storm::utility::one() / (storm::utility::one() - loopProbability)); + for (auto& entry : transitionMatrix.getRow(state)) { + // Only scale the non-diagonal entries. + if (entry.getColumn() != state) { + entry.setValue(storm::utility::simplify(entry.getValue() * loopProbability)); + } + } + updateValue(state, loopProbability); + } + + // Now connect the predecessors of the state being eliminated with its successors. + FlexibleRowType& currentStatePredecessors = backwardTransitions.getRow(state); + + // In case we have a constrained elimination, we need to keep track of the new predecessors. + FlexibleRowType newCurrentStatePredecessors; + + std::vector newBackwardProbabilities(currentStateSuccessors.size()); + for (auto& backwardProbabilities : newBackwardProbabilities) { + backwardProbabilities.reserve(currentStatePredecessors.size()); + } + + // Now go through the predecessors and eliminate the ones (satisfying the constraint if given). + for (auto const& predecessorEntry : currentStatePredecessors) { + uint_fast64_t predecessor = predecessorEntry.getColumn(); + STORM_LOG_TRACE("Found predecessor " << predecessor << "."); + + // Skip the state itself as one of its predecessors. + if (predecessor == state) { + assert(hasSelfLoop); + continue; + } + + // Skip the state if the elimination is constrained, but the predecessor is not in the constraint. + if (isFilterPredecessor() && !filterPredecessor(predecessor)) { + newCurrentStatePredecessors.emplace_back(predecessorEntry); + STORM_LOG_TRACE("Not eliminating predecessor " << predecessor << ", because it does not fit the filter."); + continue; + } + STORM_LOG_TRACE("Eliminating predecessor " << predecessor << "."); + + // 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. + FlexibleRowType& predecessorForwardTransitions = transitionMatrix.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."); + ValueType multiplyFactor = multiplyElement->getValue(); + multiplyElement->setValue(storm::utility::zero()); + + // At this point, we need to update the (forward) transitions of the predecessor. + FlexibleRowIterator first1 = predecessorForwardTransitions.begin(); + FlexibleRowIterator last1 = predecessorForwardTransitions.end(); + FlexibleRowIterator first2 = currentStateSuccessors.begin(); + FlexibleRowIterator last2 = currentStateSuccessors.end(); + + FlexibleRowType newSuccessors; + newSuccessors.reserve((last1 - first1) + (last2 - first2)); + 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). + for (; first1 != last1; ++result) { + // Skip the transitions to the state that is currently being eliminated. + if (first1->getColumn() == state || (first2 != last2 && first2->getColumn() == state)) { + if (first1->getColumn() == state) { + ++first1; + } + if (first2 != last2 && first2->getColumn() == state) { + ++first2; + } + continue; + } + + if (first2 == last2) { + 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()) { + auto successorEntry = storm::utility::simplify(std::move(*first2 * multiplyFactor)); + *result = successorEntry; + newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, successorEntry.getValue()); + // std::cout << "(1) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; + ++first2; + ++successorOffsetInNewBackwardTransitions; + } else if (first1->getColumn() < first2->getColumn()) { + *result = *first1; + ++first1; + } else { + auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue())); + *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; + ++first2; + ++successorOffsetInNewBackwardTransitions; + } + } + for (; first2 != last2; ++first2) { + if (first2->getColumn() != state) { + auto stateProbability = storm::utility::simplify(std::move(*first2 * multiplyFactor)); + *result = stateProbability; + newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, stateProbability.getValue()); + // std::cout << "(3) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; + ++successorOffsetInNewBackwardTransitions; + } + } + + // Now move the new transitions in place. + predecessorForwardTransitions = std::move(newSuccessors); + STORM_LOG_TRACE("Fixed new next-state probabilities of predecessor state " << predecessor << "."); + + updatePredecessor(predecessor, multiplyFactor, state); + + STORM_LOG_TRACE("Updating priority of predecessor."); + updatePriority(predecessor); + } + + // Finally, we need to add the predecessor to the set of predecessors of every successor. + uint_fast64_t successorOffsetInNewBackwardTransitions = 0; + for (auto const& successorEntry : currentStateSuccessors) { + if (successorEntry.getColumn() == state) { + continue; + } + + 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; + // } + + // 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) { + 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); + } + + 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; + // } + + FlexibleRowType newPredecessors; + newPredecessors.reserve((last1 - first1) + (last2 - first2)); + std::insert_iterator result(newPredecessors, newPredecessors.end()); + + for (; first1 != last1; ++result) { + if (first2 == last2) { + std::copy(first1, last1, result); + break; + } + if (first2->getColumn() < first1->getColumn()) { + if (first2->getColumn() != state) { + *result = *first2; + } + ++first2; + } else if (first1->getColumn() == first2->getColumn()) { + if (storm::modelchecker::estimateComplexity(first1->getValue()) > storm::modelchecker::estimateComplexity(first2->getValue())) { + *result = *first1; + } else { + *result = *first2; + } + ++first1; + ++first2; + } else { + *result = *first1; + ++first1; + } + } + if (isFilterPredecessor()) { + std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry::index_type, typename storm::storage::FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state && filterPredecessor(a.getColumn()); }); + } else { + 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. + successorBackwardTransitions = std::move(newPredecessors); + // std::cout << "new backward trans of " << successorEntry.getColumn() << std::endl; + // for (auto const& trans : successorBackwardTransitions) { + // std::cout << trans << std::endl; + // } + ++successorOffsetInNewBackwardTransitions; + } + STORM_LOG_TRACE("Fixed predecessor lists of successor states."); + + if (removeForwardTransitions) { + // Clear the eliminated row to reduce memory consumption. + currentStateSuccessors.clear(); + currentStateSuccessors.shrink_to_fit(); + } + if (isFilterPredecessor()) { + currentStatePredecessors = std::move(newCurrentStatePredecessors); + } else { + currentStatePredecessors.clear(); + currentStatePredecessors.shrink_to_fit(); + } + + } + + template class StateEliminator>; + +#ifdef STORM_HAVE_CARL + template class StateEliminator>; +#endif + + } // namespace stateelimination + } // namespace storage +} // namespace storm \ No newline at end of file diff --git a/src/solver/stateelimination/StateEliminator.h b/src/solver/stateelimination/StateEliminator.h new file mode 100644 index 000000000..2a58912e8 --- /dev/null +++ b/src/solver/stateelimination/StateEliminator.h @@ -0,0 +1,42 @@ +#ifndef STORM_SOLVER_STATEELIMINATION_STATEELIMINATOR_H_ +#define STORM_SOLVER_STATEELIMINATION_STATEELIMINATOR_H_ + +#include "src/storage/FlexibleSparseMatrix.h" +#include "src/storage/SparseMatrix.h" +#include "src/storage/sparse/StateType.h" +#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + class StateEliminator { + typedef typename SparseModelType::ValueType ValueType; + typedef typename storm::storage::FlexibleSparseMatrix::row_type FlexibleRowType; + typedef typename FlexibleRowType::iterator FlexibleRowIterator; + + public: + StateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions); + + void eliminateState(storm::storage::sparse::state_type state, bool removeForwardTransitions, storm::storage::BitVector predecessorConstraint = storm::storage::BitVector()); + + // Virtual methods for base classes to distinguish between different state elimination approaches + virtual void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) = 0; + virtual void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) = 0; + virtual void updatePriority(storm::storage::sparse::state_type const& state) = 0; + virtual bool filterPredecessor(storm::storage::sparse::state_type const& state) = 0; + virtual bool isFilterPredecessor() const = 0; + + + protected: + storm::storage::FlexibleSparseMatrix& transitionMatrix; + storm::storage::FlexibleSparseMatrix& backwardTransitions; + + }; + + } // namespace stateelimination + } // namespace storage +} // namespace storm + +#endif // STORM_SOLVER_STATEELIMINATION_STATEELIMINATOR_H_ \ No newline at end of file