diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h index 2ed172cde..4fd2a98a0 100644 --- a/src/adapters/CarlAdapter.h +++ b/src/adapters/CarlAdapter.h @@ -4,6 +4,8 @@ // Include config to know whether CARL is available or not. #include "storm-config.h" +#include + #ifdef STORM_HAVE_CARL #include @@ -42,9 +44,12 @@ namespace carl { } namespace storm { - typedef cln::cl_RA RationalNumber; +// typedef boost::multiprecision::gmp_rational RationalNumber; + typedef boost::multiprecision::number RationalNumber; + + typedef cln::cl_RA CarlRationalNumber; typedef carl::Variable Variable; - typedef carl::MultivariatePolynomial RawPolynomial; + typedef carl::MultivariatePolynomial RawPolynomial; typedef carl::FactorizedPolynomial Polynomial; typedef carl::Relation CompareRelation; diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 2f4212219..8c64b83a7 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 { @@ -260,10 +264,10 @@ namespace storm { std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. - FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix); - flexibleMatrix.filter(maybeStates, maybeStates); - FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions); - flexibleBackwardTransitions.filter(maybeStates, maybeStates); + storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix); + flexibleMatrix.createSubmatrix(maybeStates, maybeStates); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions); + flexibleBackwardTransitions.createSubmatrix(maybeStates, maybeStates); auto conversionEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); @@ -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 @@ -345,11 +332,11 @@ namespace storm { stateValues[*representativeIt] = bsccValue; } - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type& representativeForwardRow = flexibleMatrix.getRow(*representativeIt); + FlexibleRowType& representativeForwardRow = flexibleMatrix.getRow(*representativeIt); representativeForwardRow.clear(); representativeForwardRow.shrink_to_fit(); - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type& representativeBackwardRow = flexibleBackwardTransitions.getRow(*representativeIt); + FlexibleRowType& representativeBackwardRow = flexibleBackwardTransitions.getRow(*representativeIt); auto it = representativeBackwardRow.begin(), ite = representativeBackwardRow.end(); for (; it != ite; ++it) { if (it->getColumn() == *representativeIt) { @@ -752,21 +739,24 @@ namespace storm { eliminationOrderNeedsReversedDistances(order)); } - FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix); - FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrixTransposed, true); + std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); + storm::storage::FlexibleSparseMatrix flexibleMatrix(submatrix); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(submatrixTransposed, true); + std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now(); - std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); + 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(); + uint_fast64_t numberOfStatesToEliminate = statePriorities->size(); + STORM_LOG_INFO("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl); performPrioritizedStateElimination(statePriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, this->getModel().getInitialStates(), true); - // 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 @@ -797,11 +787,13 @@ namespace storm { for (auto const& element : currentRow) { // If any of the successors is a phi state, we eliminate it (wrt. all its phi predecessors). if (!psiStates.get(element.getColumn())) { - typename FlexibleSparseMatrix::row_type const& successorRow = flexibleMatrix.getRow(element.getColumn()); + FlexibleRowType const& successorRow = flexibleMatrix.getRow(element.getColumn()); // Eliminate the successor only if there possibly is a psi state reachable through it. if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) { STORM_LOG_TRACE("Found non-psi successor " << element.getColumn() << " that needs to be eliminated."); - eliminateState(element.getColumn(), flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorUpdateCallback, boost::none, phiFilterCallback, false); + stateEliminator.setStatePhi(); + stateEliminator.eliminateState(element.getColumn(), false); + stateEliminator.clearState(); hasNonPsiSuccessor = true; } } @@ -827,10 +819,12 @@ namespace storm { for (auto const& element : currentRow) { // If any of the successors is a psi state, we eliminate it (wrt. all its psi predecessors). if (!phiStates.get(element.getColumn())) { - typename FlexibleSparseMatrix::row_type const& successorRow = flexibleMatrix.getRow(element.getColumn()); + FlexibleRowType const& successorRow = flexibleMatrix.getRow(element.getColumn()); if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) { STORM_LOG_TRACE("Found non-phi successor " << element.getColumn() << " that needs to be eliminated."); - eliminateState(element.getColumn(), flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorUpdateCallback, boost::none, psiFilterCallback, false); + stateEliminator.setStatePsi(); + stateEliminator.eliminateState(element.getColumn(), false); + stateEliminator.clearState(); hasNonPhiSuccessor = true; } } @@ -877,7 +871,7 @@ namespace storm { } template - std::unique_ptr::StatePriorityQueue> SparseDtmcEliminationModelChecker::createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states) { + std::unique_ptr> 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); @@ -921,23 +915,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, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) { + void SparseDtmcEliminationModelChecker::performPrioritizedStateElimination(std::unique_ptr>& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) { - ValueUpdateCallback valueUpdateCallback = [&values] (storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { values[state] = storm::utility::simplify(loopProbability * values[state]); }; - PredecessorUpdateCallback predecessorCallback = [&values] (storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { values[predecessor] = storm::utility::simplify(values[predecessor] + storm::utility::simplify(probability * values[state])); }; - 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(); } @@ -946,8 +937,8 @@ namespace storm { } template - void SparseDtmcEliminationModelChecker::performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { - std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); + void SparseDtmcEliminationModelChecker::performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { + std::unique_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); std::size_t numberOfStatesToEliminate = statePriorities->size(); STORM_LOG_DEBUG("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl); @@ -956,7 +947,7 @@ namespace storm { } template - uint_fast64_t SparseDtmcEliminationModelChecker::performHybridStateElimination(storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { + uint_fast64_t SparseDtmcEliminationModelChecker::performHybridStateElimination(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { // When using the hybrid technique, we recursively treat the SCCs up to some size. std::vector entryStateQueue; STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); @@ -966,7 +957,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); @@ -976,8 +967,11 @@ namespace storm { template std::vector::ValueType> SparseDtmcEliminationModelChecker::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) { // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. - FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix); - FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions); + storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions); + auto conversionEnd = std::chrono::high_resolution_clock::now(); + + std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder(); boost::optional> distanceBasedPriorities; @@ -1008,7 +1002,7 @@ namespace storm { } template - uint_fast64_t SparseDtmcEliminationModelChecker::treatScc(FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional> const& distanceBasedPriorities) { + uint_fast64_t SparseDtmcEliminationModelChecker::treatScc(storm::storage::FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional> const& distanceBasedPriorities) { uint_fast64_t maximalDepth = level; // If the SCCs are large enough, we try to split them further. @@ -1024,7 +1018,7 @@ namespace storm { storm::storage::BitVector remainingSccs(decomposition.size(), true); // First, get rid of the trivial SCCs. - storm::storage::BitVector statesInTrivialSccs(matrix.getNumberOfRows()); + storm::storage::BitVector statesInTrivialSccs(matrix.getRowCount()); for (uint_fast64_t sccIndex = 0; sccIndex < decomposition.size(); ++sccIndex) { storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex); if (scc.isTrivial()) { @@ -1034,7 +1028,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."); @@ -1064,7 +1058,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."); } @@ -1072,7 +1066,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 { @@ -1085,229 +1079,6 @@ namespace storm { return maximalDepth; } - template - void SparseDtmcEliminationModelChecker::eliminateState(storm::storage::sparse::state_type state, FlexibleSparseMatrix& matrix, FlexibleSparseMatrix& backwardTransitions, - ValueUpdateCallback const& callback, PredecessorUpdateCallback const& predecessorCallback, - boost::optional const& priorityUpdateCallback, - boost::optional const& predecessorFilterCallback, bool removeForwardTransitions) { - - STORM_LOG_TRACE("Eliminating state " << state << "."); - - // Start by finding loop probability. - bool hasSelfLoop = false; - ValueType loopProbability = storm::utility::zero(); - typename FlexibleSparseMatrix::row_type& currentStateSuccessors = matrix.getRow(state); - 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. - typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state); - - // In case we have a constrained elimination, we need to keep track of the new predecessors. - typename FlexibleSparseMatrix::row_type newCurrentStatePredecessors; - - 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. - typename FlexibleSparseMatrix::row_type& predecessorForwardTransitions = matrix.getRow(predecessor); - typename FlexibleSparseMatrix::row_type::iterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry const& a) { return a.getColumn() == state; }); - - // 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. - 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(); - - typename FlexibleSparseMatrix::row_type 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 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()); - ++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(first1->getColumn(), probability); - newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability); - ++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()); - ++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; - } - - typename FlexibleSparseMatrix::row_type& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn()); - - // Delete the current state as a predecessor of the successor state only if we are going to remove the - // current state's forward transitions. - if (removeForwardTransitions) { - typename FlexibleSparseMatrix::row_type::iterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry const& a) { return a.getColumn() == state; }); - STORM_LOG_ASSERT(elimIt != successorBackwardTransitions.end(), "Expected a proper backward transition from " << successorEntry.getColumn() << " to " << state << ", but found none."); - successorBackwardTransitions.erase(elimIt); - } - - typename FlexibleSparseMatrix::row_type::iterator first1 = successorBackwardTransitions.begin(); - typename FlexibleSparseMatrix::row_type::iterator last1 = successorBackwardTransitions.end(); - typename FlexibleSparseMatrix::row_type::iterator first2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].begin(); - typename FlexibleSparseMatrix::row_type::iterator last2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].end(); - - typename FlexibleSparseMatrix::row_type 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 const& a) { return a.getColumn() != state && predecessorFilterCallback.get()(a.getColumn()); }); - } else { - std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry const& a) { return a.getColumn() != state; }); - } - - // Now move the new predecessors in place. - successorBackwardTransitions = std::move(newPredecessors); - ++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()); @@ -1356,111 +1127,7 @@ namespace storm { } template - SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) { - // Intentionally left empty. - } - - template - void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::reserveInRow(index_type row, index_type numberOfElements) { - this->data[row].reserve(numberOfElements); - } - - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type& SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getRow(index_type index) { - return this->data[index]; - } - - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type const& SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getRow(index_type index) const { - return this->data[index]; - } - - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::index_type SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getNumberOfRows() const { - return this->data.size(); - } - - template - bool SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::hasSelfLoop(storm::storage::sparse::state_type state) { - for (auto const& entry : this->getRow(state)) { - if (entry.getColumn() < state) { - continue; - } else if (entry.getColumn() > state) { - return false; - } else if (entry.getColumn() == state) { - return true; - } - } - return false; - } - - template - void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::print() const { - for (uint_fast64_t index = 0; index < this->data.size(); ++index) { - std::cout << index << " - "; - for (auto const& element : this->getRow(index)) { - std::cout << "(" << element.getColumn() << ", " << element.getValue() << ") "; - } - std::cout << std::endl; - } - } - - template - bool SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::empty() const { - for (auto const& row : this->data) { - if (!row.empty()) { - return false; - } - } - return true; - } - - template - void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::filter(storm::storage::BitVector const& rowFilter, storm::storage::BitVector const& columnFilter) { - for (uint_fast64_t rowIndex = 0; rowIndex < this->data.size(); ++rowIndex) { - auto& row = this->data[rowIndex]; - if (!rowFilter.get(rowIndex)) { - row.clear(); - row.shrink_to_fit(); - continue; - } - row_type newRow; - for (auto const& element : row) { - if (columnFilter.get(element.getColumn())) { - newRow.push_back(element); - } - } - row = std::move(newRow); - } - } - - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix SparseDtmcEliminationModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) { - FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); - - for (typename FlexibleSparseMatrix::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) { - typename storm::storage::SparseMatrix::const_rows row = matrix.getRow(rowIndex); - flexibleMatrix.reserveInRow(rowIndex, row.getNumberOfEntries()); - - for (auto const& element : row) { - // If the probability is zero, we skip this entry. - if (storm::utility::isZero(element.getValue())) { - continue; - } - - if (setAllValuesToOne) { - flexibleMatrix.getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::one()); - } else { - flexibleMatrix.getRow(rowIndex).emplace_back(element); - } - } - } - - return flexibleMatrix; - } - - template - uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenalty(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { uint_fast64_t penalty = 0; bool hasParametricSelfLoop = false; @@ -1487,17 +1154,17 @@ namespace storm { } template - uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size(); } - template - void SparseDtmcEliminationModelChecker::StatePriorityQueue::update(storm::storage::sparse::state_type, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + 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. } @@ -1518,7 +1185,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); @@ -1545,7 +1212,7 @@ namespace storm { } template - void SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::update(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + void SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { // First, we need to find the priority until now. auto priorityIt = stateToPriorityMapping.find(state); @@ -1574,8 +1241,8 @@ namespace storm { } template - bool SparseDtmcEliminationModelChecker::checkConsistent(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions) { - for (uint_fast64_t forwardIndex = 0; forwardIndex < transitionMatrix.getNumberOfRows(); ++forwardIndex) { + bool SparseDtmcEliminationModelChecker::checkConsistent(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions) { + for (uint_fast64_t forwardIndex = 0; forwardIndex < transitionMatrix.getRowCount(); ++forwardIndex) { for (auto const& forwardEntry : transitionMatrix.getRow(forwardIndex)) { if (forwardEntry.getColumn() == forwardIndex) { continue; @@ -1596,9 +1263,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 ba7b48121..005b20b35 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -2,6 +2,7 @@ #define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_ #include "src/storage/sparse/StateType.h" +#include "src/storage/FlexibleSparseMatrix.h" #include "src/models/sparse/Dtmc.h" #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/utility/constants.h" @@ -9,12 +10,26 @@ 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: typedef typename SparseDtmcModelType::ValueType ValueType; typedef typename SparseDtmcModelType::RewardModelType RewardModelType; - + typedef typename storm::storage::FlexibleSparseMatrix::row_type FlexibleRowType; + typedef typename FlexibleRowType::iterator FlexibleRowIterator; + /*! * Creates an elimination-based model checker for the given model. * @@ -37,51 +52,8 @@ namespace storm { static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, bool computeForInitialStatesOnly); private: - class FlexibleSparseMatrix { - public: - typedef uint_fast64_t index_type; - typedef ValueType value_type; - typedef std::vector> row_type; - typedef typename row_type::iterator iterator; - typedef typename row_type::const_iterator const_iterator; - - FlexibleSparseMatrix() = default; - FlexibleSparseMatrix(index_type rows); - - void reserveInRow(index_type row, index_type numberOfElements); - - row_type& getRow(index_type); - row_type const& getRow(index_type) const; - - index_type getNumberOfRows() const; - - void print() const; - - bool empty() const; - - void filter(storm::storage::BitVector const& rowFilter, storm::storage::BitVector const& columnFilter); - - /*! - * Checks whether the given state has a self-loop with an arbitrary probability in the probability matrix. - * - * @param state The state for which to check whether it possesses a self-loop. - * @return True iff the given state has a self-loop with an arbitrary probability in the probability matrix. - */ - bool hasSelfLoop(storm::storage::sparse::state_type state); - - private: - std::vector data; - }; - - class StatePriorityQueue { - public: - virtual bool hasNextState() const = 0; - virtual storm::storage::sparse::state_type popNextState() = 0; - virtual void update(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); - virtual std::size_t size() const = 0; - }; - class StaticStatePriorityQueue : public StatePriorityQueue { + class StaticStatePriorityQueue : public StatePriorityQueue { public: StaticStatePriorityQueue(std::vector const& sortedStates); @@ -100,15 +72,15 @@ namespace storm { } }; - typedef std::function const& oneStepProbabilities)> PenaltyFunctionType; + typedef std::function const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities)> PenaltyFunctionType; - class DynamicPenaltyStatePriorityQueue : public StatePriorityQueue { + class DynamicPenaltyStatePriorityQueue : public StatePriorityQueue { public: DynamicPenaltyStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, PenaltyFunctionType const& penaltyFunction); virtual bool hasNextState() const override; virtual storm::storage::sparse::state_type popNextState() override; - virtual void update(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) override; + virtual void update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) override; virtual std::size_t size() const override; private: @@ -121,38 +93,29 @@ namespace storm { static std::vector computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& oneStepProbabilitiesToTarget); - static std::unique_ptr createStatePriorityQueue(boost::optional> const& stateDistances, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); + static std::unique_ptr> createStatePriorityQueue(boost::optional> const& stateDistances, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); - static std::unique_ptr createNaivePriorityQueue(storm::storage::BitVector const& states); + static std::unique_ptr> createNaivePriorityQueue(storm::storage::BitVector const& states); - static void performPrioritizedStateElimination(std::unique_ptr& priorityQueue, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly); + static void performPrioritizedStateElimination(std::unique_ptr>& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly); - static void performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional>& additionalStateValues, boost::optional> const& distanceBasedPriorities); + static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional>& additionalStateValues, boost::optional> const& distanceBasedPriorities); - static void performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); - - static uint_fast64_t performHybridStateElimination(storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); + static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); - static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional> const& distanceBasedPriorities = boost::none); - - static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); - - typedef std::function ValueUpdateCallback; - typedef std::function PredecessorUpdateCallback; - typedef std::function PriorityUpdateCallback; - typedef std::function PredecessorFilterCallback; - - static void eliminateState(storm::storage::sparse::state_type state, FlexibleSparseMatrix& matrix, FlexibleSparseMatrix& backwardTransitions, ValueUpdateCallback const& valueUpdateCallback, PredecessorUpdateCallback const& predecessorCallback, boost::optional const& priorityUpdateCallback = boost::none, boost::optional const& predecessorFilterCallback = boost::none, bool removeForwardTransitions = true); + static 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); + static std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); static std::vector getStateDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward); - static uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + static uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); - static uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + static uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); - static bool checkConsistent(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions); + static bool checkConsistent(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions); }; diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp new file mode 100644 index 000000000..67a281b70 --- /dev/null +++ b/src/solver/EliminationLinearEquationSolver.cpp @@ -0,0 +1,62 @@ +#include "src/solver/EliminationLinearEquationSolver.h" + +#include "src/utility/vector.h" + +namespace storm { + namespace solver { + template + EliminationLinearEquationSolver::EliminationLinearEquationSolver(storm::storage::SparseMatrix const& A) : A(A) { + // Intentionally left empty. + } + + template + void EliminationLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { + // TODO: implement state-elimination here. + } + + template + void EliminationLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n, std::vector* multiplyResult) const { + // Set up some temporary variables so that we can just swap pointers instead of copying the result after + // each iteration. + std::vector* currentX = &x; + + bool multiplyResultProvided = true; + std::vector* nextX = multiplyResult; + if (nextX == nullptr) { + nextX = new std::vector(x.size()); + multiplyResultProvided = false; + } + std::vector const* copyX = nextX; + + // Now perform matrix-vector multiplication as long as we meet the bound. + for (uint_fast64_t i = 0; i < n; ++i) { + A.multiplyWithVector(*currentX, *nextX); + std::swap(nextX, currentX); + + // If requested, add an offset to the current result vector. + if (b != nullptr) { + storm::utility::vector::addVectors(*currentX, *b, *currentX); + } + } + + // If we performed an odd number of repetitions, we need to swap the contents of currentVector and x, + // because the output is supposed to be stored in the input vector x. + if (currentX == copyX) { + std::swap(x, *currentX); + } + + // If the vector for the temporary multiplication result was not provided, we need to delete it. + if (!multiplyResultProvided) { + delete copyX; + } + } + + template class EliminationLinearEquationSolver; + + // TODO: make this work with the proper implementation of solveEquationSystem. + template class EliminationLinearEquationSolver; + template class EliminationLinearEquationSolver; + + } +} + diff --git a/src/solver/EliminationLinearEquationSolver.h b/src/solver/EliminationLinearEquationSolver.h new file mode 100644 index 000000000..25dffa651 --- /dev/null +++ b/src/solver/EliminationLinearEquationSolver.h @@ -0,0 +1,34 @@ +#ifndef STORM_SOLVER_ELIMINATIONLINEAREQUATIONSOLVER_H_ +#define STORM_SOLVER_ELIMINATIONLINEAREQUATIONSOLVER_H_ + +#include "src/solver/LinearEquationSolver.h" + +namespace storm { + namespace solver { + /*! + * A class that uses gaussian elimination to implement the LinearEquationSolver interface. In particular + */ + template + class EliminationLinearEquationSolver : public LinearEquationSolver { + public: + + /*! + * Constructs a linear equation solver. + * + * @param A The matrix defining the coefficients of the linear equation system. + */ + EliminationLinearEquationSolver(storm::storage::SparseMatrix const& A); + + virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; + + virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + + private: + // A reference to the original matrix used for this equation solver. + storm::storage::SparseMatrix const& A; + + }; + } +} + +#endif /* STORM_SOLVER_ELIMINATIONLINEAREQUATIONSOLVER_H_ */ \ No newline at end of file diff --git a/src/solver/NativeLinearEquationSolver.h b/src/solver/NativeLinearEquationSolver.h index 6fa972f05..42dbbd3d9 100644 --- a/src/solver/NativeLinearEquationSolver.h +++ b/src/solver/NativeLinearEquationSolver.h @@ -10,6 +10,7 @@ namespace storm { enum class NativeLinearEquationSolverSolutionMethod { Jacobi, GaussSeidel, SOR }; + /*! * A class that uses StoRM's native matrix operations to implement the LinearEquationSolver interface. */ @@ -17,7 +18,6 @@ namespace storm { class NativeLinearEquationSolver : public LinearEquationSolver { public: - /*! * Constructs a linear equation solver with parameters being set according to the settings object. * 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 diff --git a/src/storage/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp new file mode 100644 index 000000000..81e87ce20 --- /dev/null +++ b/src/storage/FlexibleSparseMatrix.cpp @@ -0,0 +1,161 @@ +#include "src/storage/FlexibleSparseMatrix.h" + +#include "src/storage/SparseMatrix.h" +#include "src/storage/BitVector.h" +#include "src/adapters/CarlAdapter.h" +#include "src/utility/constants.h" + +namespace storm { + namespace storage { + template + FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows), columnCount(0), nonzeroEntryCount(0) { + // Intentionally left empty. + } + + template + FlexibleSparseMatrix::FlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) : data(matrix.getRowCount()), columnCount(matrix.getColumnCount()), nonzeroEntryCount(matrix.getNonzeroEntryCount()), nontrivialRowGrouping(matrix.hasNontrivialRowGrouping()) { + if (nontrivialRowGrouping) { + rowGroupIndices = matrix.getRowGroupIndices(); + rowIndications = matrix.getRowIndications(); + // Not fully implemented yet + assert(false); + } + for (index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) { + typename storm::storage::SparseMatrix::const_rows row = matrix.getRow(rowIndex); + reserveInRow(rowIndex, row.getNumberOfEntries()); + for (auto const& element : row) { + // If the probability is zero, we skip this entry. + if (storm::utility::isZero(element.getValue())) { + continue; + } + if (setAllValuesToOne) { + getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::one()); + } else { + getRow(rowIndex).emplace_back(element); + } + } + } + } + + template + void FlexibleSparseMatrix::reserveInRow(index_type row, index_type numberOfElements) { + this->data[row].reserve(numberOfElements); + } + + template + typename FlexibleSparseMatrix::row_type& FlexibleSparseMatrix::getRow(index_type index) { + return this->data[index]; + } + + template + typename FlexibleSparseMatrix::row_type const& FlexibleSparseMatrix::getRow(index_type index) const { + return this->data[index]; + } + + template + typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getRowCount() const { + return this->data.size(); + } + + template + typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getColumnCount() const { + return columnCount; + } + + template + typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getNonzeroEntryCount() const { + return nonzeroEntryCount; + } + + template + void FlexibleSparseMatrix::updateDimensions() { + this->nonzeroEntryCount = 0; + this->columnCount = 0; + for (auto const& row : this->data) { + for (auto const& element : row) { + assert(!storm::utility::isZero(element.getValue())); + ++this->nonzeroEntryCount; + this->columnCount = std::max(element.getColumn() + 1, this->columnCount); + } + } + } + + template + bool FlexibleSparseMatrix::empty() const { + for (auto const& row : this->data) { + if (!row.empty()) { + return false; + } + } + return true; + } + + template + bool SparseMatrix::hasNontrivialRowGrouping() const { + return nontrivialRowGrouping; + } + + template + void FlexibleSparseMatrix::createSubmatrix(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) { + for (uint_fast64_t rowIndex = 0; rowIndex < this->data.size(); ++rowIndex) { + auto& row = this->data[rowIndex]; + if (!rowConstraint.get(rowIndex)) { + row.clear(); + row.shrink_to_fit(); + continue; + } + row_type newRow; + for (auto const& element : row) { + if (columnConstraint.get(element.getColumn())) { + newRow.push_back(element); + } + } + row = std::move(newRow); + } + } + + template + storm::storage::SparseMatrix FlexibleSparseMatrix::createSparseMatrix() { + storm::storage::SparseMatrixBuilder matrixBuilder(getRowCount(), getColumnCount()); + for (uint_fast64_t rowIndex = 0; rowIndex < getRowCount(); ++rowIndex) { + auto& row = this->data[rowIndex]; + for (auto const& entry : row) { + matrixBuilder.addNextValue(rowIndex, entry.getColumn(), entry.getValue()); + } + } + return matrixBuilder.build(); + } + + template + bool FlexibleSparseMatrix::rowHasDiagonalElement(storm::storage::sparse::state_type state) { + for (auto const& entry : this->getRow(state)) { + if (entry.getColumn() < state) { + continue; + } else if (entry.getColumn() > state) { + return false; + } else if (entry.getColumn() == state) { + return true; + } + } + return false; + } + + template + std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix) { + for (uint_fast64_t index = 0; index < matrix->data.size(); ++index) { + out << index << " - "; + for (auto const& element : matrix->getRow(index)) { + out << "(" << element.getColumn() << ", " << element.getValue() << ") "; + } + return out; + } + } + + // Explicitly instantiate the matrix. + template class FlexibleSparseMatrix; +#ifdef STORM_HAVE_CARL + template class FlexibleSparseMatrix; +#endif + + } // namespace storage +} // namespace storm \ No newline at end of file diff --git a/src/storage/FlexibleSparseMatrix.h b/src/storage/FlexibleSparseMatrix.h new file mode 100644 index 000000000..295b0337b --- /dev/null +++ b/src/storage/FlexibleSparseMatrix.h @@ -0,0 +1,163 @@ +#ifndef STORM_STORAGE_FLEXIBLESPARSEMATRIX_H_ +#define STORM_STORAGE_FLEXIBLESPARSEMATRIX_H_ + +#include +#include + +#include "src/storage/sparse/StateType.h" +#include "src/storage/SparseMatrix.h" + +namespace storm { + namespace storage { + template + class MatrixEntry; + + class BitVector; + + /*! + * The flexible sparse matrix is used during state elimination. + */ + template + class FlexibleSparseMatrix { + public: + // TODO: make this class a bit more consistent with the big sparse matrix and improve it: + // * add output iterator and improve the way the matrix is printed + // * add stuff like clearRow, multiplyRowWithScalar + // * implement row grouping + + typedef uint_fast64_t index_type; + typedef ValueType value_type; + typedef std::vector> row_type; + typedef typename row_type::iterator iterator; + typedef typename row_type::const_iterator const_iterator; + + /*! + * Constructs an empty flexible sparse matrix. + */ + FlexibleSparseMatrix() = default; + + /*! + * Constructs a flexible sparse matrix with rows many rows. + * @param rows number of rows. + */ + FlexibleSparseMatrix(index_type rows); + + /*! + * Constructs a flexible sparse matrix from a sparse matrix. + * @param matrix Sparse matrix to construct from. + * @param setAllValuesToOne If true, all set entries are set to one. Default is false. + */ + FlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); + + /*! + * Reserves space for elements in row. + * @param row Row to reserve in. + * @param numberOfElements Number of elements to reserve space for. + */ + void reserveInRow(index_type row, index_type numberOfElements); + + /*! + * Returns an object representing the given row. + * + * @param row The row to get. + * @return An object representing the given row. + */ + row_type& getRow(index_type); + + /*! + * Returns an object representing the given row. + * + * @param row The row to get. + * @return An object representing the given row. + */ + row_type const& getRow(index_type) const; + + /*! + * 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; + + /*! + * Retrieves whether the matrix has a (possibly) non-trivial row grouping. + * + * @return True iff the matrix has a (possibly) non-trivial row grouping. + */ + bool hasNontrivialRowGrouping() const; + + /*! + * Creates a submatrix of the current matrix in place by dropping all rows and columns whose bits are not + * set to one in the given bit vector. + * + * @param rowConstraint A bit vector indicating which rows to keep. + * @param columnConstraint A bit vector indicating which columns to keep. + */ + void createSubmatrix(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint); + + /*! + * Creates a sparse matrix from the flexible sparse matrix. + * @return The sparse matrix. + */ + storm::storage::SparseMatrix createSparseMatrix(); + + /*! + * Checks whether the given state has a self-loop with an arbitrary probability in the probability matrix. + * + * @param state The state for which to check whether it possesses a self-loop. + * @return True iff the given state has a self-loop with an arbitrary probability in the probability matrix. + */ + bool rowHasDiagonalElement(storm::storage::sparse::state_type state); + + template + friend std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix); + + private: + std::vector data; + + // The number of columns of the matrix. + index_type columnCount; + + // The number of entries in the matrix. + index_type nonzeroEntryCount; + + // A vector containing the indices at which each given row begins. The values of the entries in row i are + // data[rowIndications[i]] to data[rowIndications[i + 1]] where the last entry is not included anymore. + std::vector rowIndications; + + // A flag that indicates whether the matrix has a non-trivial row-grouping, i.e. (possibly) more than one + // row per row group. + bool nontrivialRowGrouping; + + // A vector indicating the row groups of the matrix. + std::vector rowGroupIndices; + }; + } +} + +#endif /* STORM_STORAGE_FLEXIBLESPARSEMATRIX_H_ */ \ No newline at end of file diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 253609210..04e941561 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -451,6 +451,11 @@ namespace storm { std::vector::index_type> const& SparseMatrix::getRowGroupIndices() const { return rowGroupIndices; } + + template + std::vector::index_type> const& SparseMatrix::getRowIndications() const { + return rowIndications; + } template void SparseMatrix::makeRowsAbsorbing(storm::storage::BitVector const& rows) { diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index f9d9916c4..94defdfa5 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -549,6 +549,13 @@ namespace storm { */ std::vector const& getRowGroupIndices() const; + /*! + * Returns the indices where new row groups start. + * + * @return The indices where new row groups start. + */ + std::vector const& getRowIndications() const; + /*! * This function makes the given rows absorbing. * diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp index 97501aa1b..5e0ebcd64 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp @@ -88,12 +88,12 @@ namespace storm { template boost::any ToRationalFunctionVisitor::visit(IntegerLiteralExpression const& expression) { - return RationalFunctionType(carl::rationalize(static_cast(expression.getValue()))); + return RationalFunctionType(carl::rationalize(static_cast(expression.getValue()))); } template boost::any ToRationalFunctionVisitor::visit(DoubleLiteralExpression const& expression) { - return RationalFunctionType(carl::rationalize(expression.getValue())); + return RationalFunctionType(carl::rationalize(expression.getValue())); } template class ToRationalFunctionVisitor; diff --git a/src/utility/vector.h b/src/utility/vector.h index 6b09f0467..3d86cdc13 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -271,7 +271,7 @@ namespace storm { * @param target The target vector. */ template - void applyPointwise(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target, std::function function) { + void applyPointwise(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target, std::function const& function) { #ifdef STORM_HAVE_INTELTBB tbb::parallel_for(tbb::blocked_range(0, target.size()), [&](tbb::blocked_range const& range) {