diff --git a/examples/mdp/consensus/coin.pctl b/examples/mdp/consensus/coin.pctl index edd87a453..7eb1c2bc8 100644 --- a/examples/mdp/consensus/coin.pctl +++ b/examples/mdp/consensus/coin.pctl @@ -11,10 +11,10 @@ Pmin=? [ F finished & all_coins_equal_1 ] Pmax=? [ F finished & !agree ] // Min/max probability of finishing within k steps -Pmin=? [ F<=50 finished ] -Pmax=? [ F<=50 finished ] +// Pmin=? [ F<=50 finished ] +// Pmax=? [ F<=50 finished ] // Min/max expected steps to finish -Rmin=? [ F finished ] -Rmax=? [ F finished ] +// Rmin=? [ F finished ] +// Rmax=? [ F finished ] diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 5256fda66..66a0fb794 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -279,10 +279,6 @@ namespace storm { storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); - // Delete sub-results that are obsolete now. - delete leftStates; - delete rightStates; - storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); @@ -317,7 +313,7 @@ namespace storm { std::vector b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount()); // Create vector for results for maybe states. - std::vector x = this->getInitialValueIterationValues(submatrix, subNondeterministicChoiceIndices, b); + std::vector x = this->getInitialValueIterationValues(minimize, submatrix, subNondeterministicChoiceIndices, b, statesWithProbability1, maybeStates); // Solve the corresponding system of equations. if (linearEquationSolver != nullptr) { @@ -339,6 +335,9 @@ namespace storm { this->computeTakenChoices(this->minimumOperatorStack.top(), false, *result, *scheduler, this->getModel().getNondeterministicChoiceIndices()); } + // Delete sub-results that are obsolete now. + delete leftStates; + delete rightStates; return result; } @@ -523,7 +522,7 @@ namespace storm { } // Create vector for results for maybe states. - std::vector x = this->getInitialValueIterationValues(submatrix, subNondeterministicChoiceIndices, b); + std::vector x = this->getInitialValueIterationValues(minimize, submatrix, subNondeterministicChoiceIndices, b, *targetStates, maybeStates); // Solve the corresponding system of equations. if (linearEquationSolver != nullptr) { @@ -645,11 +644,20 @@ namespace storm { * * @param submatrix The matrix that will be used for value iteration later. */ - std::vector getInitialValueIterationValues(storm::storage::SparseMatrix const& submatrix, std::vector const& subNondeterministicChoiceIndices, std::vector const& rightHandSide) const { + std::vector getInitialValueIterationValues(bool minimize, storm::storage::SparseMatrix const& submatrix, + std::vector const& subNondeterministicChoiceIndices, + std::vector const& rightHandSide, + storm::storage::BitVector const& targetStates, + storm::storage::BitVector const& maybeStates) const { storm::settings::Settings* s = storm::settings::instance(); double precision = s->get("precision"); if (s->get("use-heuristic-presolve")) { - std::vector scheduler(submatrix.getColumnCount()); + + std::pair, std::vector> distancesAndPredecessorsPair = storm::utility::graph::performDijkstra(this->getModel(), + this->getModel().template getBackwardTransitions([](Type const& value) -> Type { return value; }), + minimize? ~(maybeStates | targetStates) : targetStates, &maybeStates); + + std::vector scheduler = this->convertShortestPathsToScheduler(maybeStates, distancesAndPredecessorsPair.second); std::vector result(scheduler.size(), Type(0.5)); std::vector b(scheduler.size()); storm::utility::vector::selectVectorValues(b, scheduler, subNondeterministicChoiceIndices, rightHandSide); @@ -672,6 +680,31 @@ namespace storm { } } + std::vector convertShortestPathsToScheduler(storm::storage::BitVector const& maybeStates, std::vector const& shortestPathSuccessors) const { + std::vector scheduler(maybeStates.getNumberOfSetBits()); + + Type maxProbability = 0; + uint_fast64_t currentStateIndex = 0; + for (auto state : maybeStates) { + maxProbability = 0; + + for (uint_fast64_t row = 0, rowEnd = this->getModel().getNondeterministicChoiceIndices()[state + 1] - this->getModel().getNondeterministicChoiceIndices()[state]; row < rowEnd; ++row) { + typename storm::storage::SparseMatrix::Rows currentRow = this->getModel().getTransitionMatrix().getRows(this->getModel().getNondeterministicChoiceIndices()[state] + row, this->getModel().getNondeterministicChoiceIndices()[state] + row); + + for (auto& transition : currentRow) { + if (transition.column() == shortestPathSuccessors[state] && transition.value() > maxProbability) { + maxProbability = transition.value(); + scheduler[currentStateIndex] = row; + } + } + } + + ++currentStateIndex; + } + + return scheduler; + } + // An object that is used for solving linear equations and performing matrix-vector multiplication. std::unique_ptr> linearEquationSolver; diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index c8f6e2c1a..2cc6fe8d4 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -68,24 +68,16 @@ class AbstractDeterministicModel: public AbstractModel { // Intentionally left empty. } - /*! - * Returns an iterator to the successors of the given state. - * - * @param state The state for which to return the iterator. - * @return An iterator to the successors of the given state. - */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { - return this->transitionMatrix.constColumnIteratorBegin(state); + virtual typename storm::storage::SparseMatrix::Rows getRows(uint_fast64_t state) const override { + return this->transitionMatrix.getRows(state, state); } - /*! - * Returns an iterator pointing to the element past the successors of the given state. - * - * @param state The state for which to return the iterator. - * @return An iterator pointing to the element past the successors of the given state. - */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { - return this->transitionMatrix.constColumnIteratorEnd(state); + virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const override { + return this->transitionMatrix.begin(state); + } + + virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const override { + return this->transitionMatrix.end(state); } /*! diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index df57d8d51..83e4bbc4a 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -158,8 +158,9 @@ class AbstractModel: public std::enable_shared_from_this> { // Now, we determine the blocks which are reachable (in one step) from the current block. std::set allTargetBlocks; for (auto state : block) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator succIt = this->constStateSuccessorIteratorBegin(state), succIte = this->constStateSuccessorIteratorEnd(state); succIt != succIte; ++succIt) { - uint_fast64_t targetBlock = stateToBlockMap[*succIt]; + typename storm::storage::SparseMatrix::Rows rows = this->getRows(state); + for (auto& transition : rows) { + uint_fast64_t targetBlock = stateToBlockMap[transition.column()]; // We only need to consider transitions that are actually leaving the SCC. if (targetBlock != currentBlockIndex) { @@ -185,18 +186,32 @@ class AbstractModel: public std::enable_shared_from_this> { * * @return A sparse matrix that represents the backward transitions of this model. */ - virtual storm::storage::SparseMatrix getBackwardTransitions() const { + storm::storage::SparseMatrix getBackwardTransitions() const { + return getBackwardTransitions([](T const& value) -> bool { return value != 0; }); + } + + /*! + * Retrieves the backward transition relation of the model, i.e. a set of transitions + * between states that correspond to the reversed transition relation of this model. + * + * @return A sparse matrix that represents the backward transitions of this model. + */ + template + storm::storage::SparseMatrix getBackwardTransitions(std::function const& selectionFunction) const { uint_fast64_t numberOfStates = this->getNumberOfStates(); uint_fast64_t numberOfTransitions = this->getNumberOfTransitions(); std::vector rowIndications(numberOfStates + 1); std::vector columnIndications(numberOfTransitions); - std::vector values(numberOfTransitions, true); + std::vector values(numberOfTransitions, selectionFunction(0)); // First, we need to count how many backward transitions each state has. for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (auto rowIt = this->constStateSuccessorIteratorBegin(i), rowIte = this->constStateSuccessorIteratorEnd(i); rowIt != rowIte; ++rowIt) { - rowIndications[*rowIt + 1]++; + typename storm::storage::SparseMatrix::Rows rows = this->getRows(i); + for (auto& transition : rows) { + if (transition.value() > 0) { + ++rowIndications[transition.column() + 1]; + } } } @@ -218,27 +233,39 @@ class AbstractModel: public std::enable_shared_from_this> { // Now we are ready to actually fill in the list of predecessors for // every state. Again, we start by considering all but the last row. for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (auto rowIt = this->constStateSuccessorIteratorBegin(i), rowIte = this->constStateSuccessorIteratorEnd(i); rowIt != rowIte; ++rowIt) { - columnIndications[nextIndices[*rowIt]++] = i; + typename storm::storage::SparseMatrix::Rows rows = this->getRows(i); + for (auto& transition : rows) { + if (transition.value() > 0) { + values[nextIndices[transition.column()]] = selectionFunction(transition.value()); + columnIndications[nextIndices[transition.column()]++] = i; + } } } - storm::storage::SparseMatrix backwardTransitionMatrix(numberOfStates, numberOfStates, - numberOfTransitions, - std::move(rowIndications), - std::move(columnIndications), - std::move(values)); + storm::storage::SparseMatrix backwardTransitionMatrix(numberOfStates, numberOfStates, + numberOfTransitions, + std::move(rowIndications), + std::move(columnIndications), + std::move(values)); return backwardTransitionMatrix; } + /*! + * Returns an object representing the matrix rows associated with the given state. + * + * @param state The state for which to retrieve the rows. + * @return An object representing the matrix rows associated with the given state. + */ + virtual typename storm::storage::SparseMatrix::Rows getRows(uint_fast64_t state) const = 0; + /*! * Returns an iterator to the successors of the given state. * * @param state The state for which to return the iterator. * @return An iterator to the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const = 0; + virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const = 0; /*! * Returns an iterator pointing to the element past the successors of the given state. @@ -246,8 +273,8 @@ class AbstractModel: public std::enable_shared_from_this> { * @param state The state for which to return the iterator. * @return An iterator pointing to the element past the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const = 0; - + virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const = 0; + /*! * Returns the state space size of the model. * @return The size of the state space of the model. diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 08cb32487..59f1632fb 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -108,24 +108,16 @@ class AbstractNondeterministicModel: public AbstractModel { return nondeterministicChoiceIndices; } - /*! - * Returns an iterator to the successors of the given state. - * - * @param state The state for which to return the iterator. - * @return An iterator to the successors of the given state. - */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { - return this->transitionMatrix.constColumnIteratorBegin(nondeterministicChoiceIndices[state]); + virtual typename storm::storage::SparseMatrix::Rows getRows(uint_fast64_t state) const override { + return this->transitionMatrix.getRows(nondeterministicChoiceIndices[state], nondeterministicChoiceIndices[state + 1] - 1); } - /*! - * Returns an iterator pointing to the element past the successors of the given state. - * - * @param state The state for which to return the iterator. - * @return An iterator pointing to the element past the successors of the given state. - */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { - return this->transitionMatrix.constColumnIteratorEnd(nondeterministicChoiceIndices[state + 1] - 1); + virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const override { + return this->transitionMatrix.begin(nondeterministicChoiceIndices[state]); + } + + virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const override { + return this->transitionMatrix.end(nondeterministicChoiceIndices[state + 1] - 1); } /*! diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h index 66db7df94..2f601f3ed 100644 --- a/src/solver/GmmxxLinearEquationSolver.h +++ b/src/solver/GmmxxLinearEquationSolver.h @@ -177,7 +177,7 @@ namespace storm { std::vector* xCurrent = &x; // Target vector for precision calculation. - std::vector* residuum = new std::vector(x.size()); + std::vector tmpX(x.size()); // Set up additional environment variables. uint_fast64_t iterationCount = 0; @@ -185,11 +185,11 @@ namespace storm { while (!converged && iterationCount < maxIterations) { // R * x_k (xCurrent is x_k) -> xNext - gmm::mult(*gmmxxLU, *xCurrent, *xNext); + gmm::mult(*gmmxxLU, *xCurrent, tmpX); // b - R * x_k (xNext contains R * x_k) -> xNext - gmm::add(b, gmm::scaled(*xNext, -1.0), *xNext); + gmm::add(b, gmm::scaled(tmpX, -1.0), tmpX); // D^-1 * (b - R * x_k) -> xNext - gmm::mult(*gmmxxDiagonalInverted, *xNext, *xNext); + gmm::mult(*gmmxxDiagonalInverted, tmpX, *xNext); // Swap xNext with xCurrent so that the next iteration can use xCurrent again without having to copy the // vector. @@ -214,7 +214,6 @@ namespace storm { delete xCopy; // Also delete the other dynamically allocated variables. - delete residuum; delete gmmxxDiagonalInverted; delete gmmxxLU; diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 690ee86ff..d57fd2e23 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -96,6 +96,16 @@ public: return *this; } + /*! + * Dereferences the iterator by returning a reference to itself. This is needed for making use of the range-based + * for loop over transitions. + * + * @return A reference to itself. + */ + ConstIterator& operator*() { + return *this; + } + /*! * Compares the two iterators for inequality. * @@ -144,34 +154,34 @@ public: }; /*! - * This class represents a single row of the matrix. + * This class represents a number of consecutive rows of the matrix. */ - class Row { + class Rows { public: /*! * Constructs a row from the given parameters. * - * @param valuePtr A pointer to the value of the first non-zero element of the row. - * @param columnPtr A pointer to the column of the first non-zero element of the row. - * @param entryCount The number of non-zero elements of this row. + * @param valuePtr A pointer to the value of the first non-zero element of the rows. + * @param columnPtr A pointer to the column of the first non-zero element of the rows. + * @param entryCount The number of non-zero elements of the rows. */ - Row(T const* valuePtr, uint_fast64_t const* columnPtr, uint_fast64_t entryCount) : valuePtr(valuePtr), columnPtr(columnPtr), entryCount(entryCount) { + Rows(T const* valuePtr, uint_fast64_t const* columnPtr, uint_fast64_t entryCount) : valuePtr(valuePtr), columnPtr(columnPtr), entryCount(entryCount) { // Intentionally left empty. } /*! - * Retrieves an iterator that points to the beginning of the row. + * Retrieves an iterator that points to the beginning of the rows. * - * @return An iterator that points to the beginning of the row. + * @return An iterator that points to the beginning of the rows. */ ConstIterator begin() const { return ConstIterator(valuePtr, columnPtr); } /*! - * Retrieves an iterator that points past the last element of the row. + * Retrieves an iterator that points past the last element of the rows. * - * @return An iterator that points past the last element of the row. + * @return An iterator that points past the last element of the rows. */ ConstIterator end() const { return ConstIterator(valuePtr + entryCount, columnPtr + entryCount); @@ -184,7 +194,7 @@ public: // The pointer to the column of the first element. uint_fast64_t const* columnPtr; - // The number of non-zero entries in this row. + // The number of non-zero entries in the rows. uint_fast64_t entryCount; }; @@ -214,6 +224,13 @@ public: return *this; } + /*! + * Compares the iterator to the given row iterator. + */ + bool operator!=(ConstRowIterator const& other) const { + return this->rowPtr != other.rowPtr; + } + /*! * Retrieves an iterator that points to the beginning of the current row. * @@ -1124,9 +1141,6 @@ public: #else ConstRowIterator rowIt = this->begin(); - // std::cout << this->toString() << std::endl; - // std::cout << vector << std::endl; - for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++rowIt) { *resultIt = storm::utility::constGetZero(); @@ -1134,7 +1148,6 @@ public: *resultIt += elementIt.value() * vector[elementIt.column()]; } } - // std::cout << result << std::endl; #endif } @@ -1153,19 +1166,26 @@ public: size += sizeof(uint_fast64_t) * rowIndications.capacity(); return size; } - - void moveToRow(ConstIterator& it, uint_fast64_t rowOffset) const { - // std::cout << rowOffset << " / " << this->nonZeroEntryCount << std::endl; - it.moveTo(this->valueStorage.data() + rowOffset, this->columnIndications.data() + rowOffset); + + /*! + * Returns an object representing the consecutive rows given by the parameters. + * + * @param The starting row. + * @param The ending row (which is included in the result). + * @return An object representing the consecutive rows given by the parameters. + */ + Rows getRows(uint_fast64_t startRow, uint_fast64_t endRow) const { + return Rows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); } /*! * Returns a const iterator to the rows of the matrix. * + * @param initialRow The initial row to which this iterator points. * @return A const iterator to the rows of the matrix. */ - ConstRowIterator begin() const { - return ConstRowIterator(this->valueStorage.data(), this->columnIndications.data(), this->rowIndications.data()); + ConstRowIterator begin(uint_fast64_t initialRow = 0) const { + return ConstRowIterator(this->valueStorage.data(), this->columnIndications.data(), this->rowIndications.data() + initialRow); } /*! @@ -1174,9 +1194,19 @@ public: * @return A const iterator that points to past the last row of the matrix */ ConstRowIterator end() const { - return ConstRowIterator(this->valueStorage.data() + nonZeroEntryCount, this->columnIndications.data() + nonZeroEntryCount, this->rowIndications.data() + rowCount); + return ConstRowIterator(this->valueStorage.data(), this->columnIndications.data(), this->rowIndications.data() + rowCount); } + /*! + * Returns a const iterator that points past the given row. + * + * @param row The row past which this iterator points. + * @return A const iterator that points past the given row. + */ + ConstRowIterator end(uint_fast64_t row) const { + return ConstRowIterator(this->valueStorage.data(), this->columnIndications.data(), this->rowIndications.data() + row + 1); + } + /*! * Returns an iterator to the columns of the non-zero entries of the matrix. * diff --git a/src/utility/ConstTemplates.h b/src/utility/ConstTemplates.h index 847c38174..20704e3c1 100644 --- a/src/utility/ConstTemplates.h +++ b/src/utility/ConstTemplates.h @@ -160,7 +160,7 @@ inline int_fast32_t constGetInfinity() { template<> inline uint_fast64_t constGetInfinity() { throw storm::exceptions::InvalidArgumentException() << "Integer has no infinity."; - return std::numeric_limits::max(); + return std::numeric_limits::max(); } /*! diff --git a/src/utility/graph.h b/src/utility/graph.h index 4d67f35ac..9d79f72ed 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -8,8 +8,12 @@ #ifndef STORM_UTILITY_GRAPH_H_ #define STORM_UTILITY_GRAPH_H_ +#include +#include + #include "src/models/AbstractDeterministicModel.h" #include "src/models/AbstractNondeterministicModel.h" +#include "ConstTemplates.h" #include "src/exceptions/InvalidArgumentException.h" #include "log4cplus/logger.h" @@ -757,6 +761,72 @@ namespace graph { return topologicalSort; } + template + struct DistanceCompare { + bool operator()(std::pair const& lhs, std::pair const& rhs) const { + return lhs.first < rhs.first || (lhs.first == rhs.first && lhs.second < rhs.second); + } + }; + + template + std::pair, std::vector> performDijkstra(storm::models::AbstractModel const& model, + storm::storage::SparseMatrix const& transitions, + storm::storage::BitVector const& startingStates, +// FIXME: The case in which there are target states given should be handled properly. +// storm::storage::BitVector* targetStates = nullptr, + storm::storage::BitVector const* filterStates = nullptr) { + + LOG4CPLUS_INFO(logger, "Performing Dijkstra search."); + + const uint_fast64_t noPredecessorValue = std::numeric_limits::max(); + std::vector distances(model.getNumberOfStates(), storm::utility::constGetInfinity()); + std::vector predecessors(model.getNumberOfStates(), noPredecessorValue); + + // Set the distance to 0 for all starting states. + std::set, DistanceCompare> distanceStateSet; + for (auto state : startingStates) { + distanceStateSet.emplace(storm::utility::constGetZero(), state); + distances[state] = 0; + } + + while (!distanceStateSet.empty()) { + // Get the state with the least distance from the set and remove it. + std::pair distanceStatePair = *distanceStateSet.begin(); + distanceStateSet.erase(distanceStateSet.begin()); + + // Now check the new distances for all successors of the current state. + typename storm::storage::SparseMatrix::Rows row = transitions.getRows(distanceStatePair.second, distanceStatePair.second); + for (auto& transition : row) { + // Only follow the transition if it lies within the filtered states. + if (filterStates != nullptr && filterStates->get(transition.column())) { + // Calculate the distance we achieve when we take the path to the successor via the current state. + T newDistance = distanceStatePair.first + std::log(storm::utility::constGetOne() / transition.value()); + + // We found a cheaper way to get to the target state of the transition. + if (newDistance < distances[transition.column()]) { + // Remove the old distance. + if (distances[transition.column()] != noPredecessorValue) { + distanceStateSet.erase(std::make_pair(distances[transition.column()], transition.column())); + } + + // Set and add the new distance. + distances[transition.column()] = newDistance; + predecessors[transition.column()] = distanceStatePair.second; + distanceStateSet.insert(std::make_pair(newDistance, transition.column())); + } + } + } + } + + std::pair, std::vector> result; + result.first = std::move(distances); + result.second = std::move(predecessors); + + LOG4CPLUS_INFO(logger, "Done performing Dijkstra search."); + + return result; + } + } // namespace graph } // namespace utility