diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index edb5fd8a8..dd844a6ae 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -166,7 +166,7 @@ public: * @param formula The Or state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or& formula) { + virtual mrmc::storage::BitVector* checkOr(mrmc::formula::Or& formula) { mrmc::storage::BitVector* result = check(formula.getLeft()); mrmc::storage::BitVector* right = check(formula.getRight()); (*result) |= (*right); diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h new file mode 100644 index 000000000..0493cda1a --- /dev/null +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -0,0 +1,162 @@ +/* + * GmmxxDtmcPrctlModelChecker.h + * + * Created on: 06.12.2012 + * Author: Christian Dehnert + */ + +#ifndef GMMXXDTMCPRCTLMODELCHECKER_H_ +#define GMMXXDTMCPRCTLMODELCHECKER_H_ + +#include "src/utility/vector.h" + +#include "src/models/dtmc.h" +#include "src/solver/GraphAnalyzer.h" + +#include "gmm/gmm_matrix.h" +#include "gmm/gmm_iter_solvers.h" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +log4cplus::Logger logger; + +namespace mrmc { + +namespace modelChecker { + +/* + * A model checking engine that makes use of the gmm++ backend. + */ +template +class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker { + +public: + explicit GmmxxDtmcPrctlModelChecker(const mrmc::models::Dtmc* dtmc) : DtmcPrctlModelChecker(dtmc) { } + + virtual ~GmmxxDtmcPrctlModelChecker() { } + + virtual std::vector* checkBoundedUntil(mrmc::formula::BoundedUntil& formula) { + // First, we need to compute the states that satisfy the sub-formulas of the until-formula. + mrmc::storage::BitVector* leftStates = this->check(formula.getLeft()); + mrmc::storage::BitVector* rightStates = this->check(formula.getRight()); + + // Copy the matrix before we make any changes. + mrmc::storage::SquareSparseMatrix* tmpMatrix(dtmc.getTransitionProbabilityMatrix()); + + // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. + tmpMatrix.makeRowsAbsorbing((~leftStates & rightStates) | rightStates); + + // Transform the transition probability matrix to the gmm++ format to use its arithmetic. + gmm::csr_matrix* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix(); + + // Create the vector with which to multiply. + std::vector* result = new st::vector(dtmc.getNumberOfStates()); + mrmc::utility::setVectorValue(result, *rightStates, 1); + + // Now perform matrix-vector multiplication as long as we meet the bound of the formula. + for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { + gmm::mult(*gmmxxMatrix, *result, *result); + } + + // Delete intermediate results. + delete leftStates; + delete rightStates; + + return result; + } + + virtual std::vector* checkNext(const mrmc::formula::Next& formula) { + // First, we need to compute the states that satisfy the sub-formula of the next-formula. + mrmc::storage::BitVector* nextStates = this->check(formula.getChild()); + + // Transform the transition probability matrix to the gmm++ format to use its arithmetic. + gmm::csr_matrix* gmmxxMatrix = dtmc.getTransitionProbabilityMatrix()->toGMMXXSparseMatrix(); + + // Create the vector with which to multiply and initialize it correctly. + std::vector x(dtmc.getNumberOfStates()); + mrmc::utility::setVectorValue(x, nextStates, 1); + + // Delete not needed next states bit vector. + delete nextStates; + + // Create resulting vector. + std::vector* result = new std::vector(dtmc.getNumberOfStates()); + + // Perform the actual computation. + gmm::mult(*gmmxxMatrix, x, *result); + + // Delete temporary matrix and return result. + delete gmmxxMatrix; + return result; + } + + virtual std::vector* checkUntil(const mrmc::formula::Until& formula) { + // First, we need to compute the states that satisfy the sub-formulas of the until-formula. + mrmc::storage::BitVector* leftStates = this->check(formula.getLeft()); + mrmc::storage::BitVector* rightStates = this->check(formula.getRight()); + + // Then, we need to identify the states which have to be taken out of the matrix, i.e. + // all states that have probability 0 and 1 of satisfying the until-formula. + mrmc::storage::BitVector notExistsPhiUntilPsiStates(dtmc.getNumberOfStates()); + mrmc::storage::BitVector alwaysPhiUntilPsiStates(dtmc.getNumberOfStates()); + mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates(dtmc, *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); + notExistsPhiUntilPsiStates->complement(); + + delete leftStates; + delete rightStates; + + LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states."); + LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states."); + mrmc::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates); + LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " maybe states."); + + // Only try to solve system if there are states for which the probability is unknown. + if (maybeStates.getNumberOfSetBits() > 0) { + // Now we can eliminate the rows and columns from the original transition probability matrix. + mrmc::storage::SquareSparseMatrix* submatrix = dtmc.getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); + // Converting the matrix to the form needed for the equation system. That is, we go from + // x = A*x + b to (I-A)x = b. + submatrix->convertToEquationSystem(); + + // Transform the submatrix to the gmm++ format to use its solvers. + gmm::csr_matrix* gmmxxMatrix = submatrix->toGMMXXSparseMatrix(); + + // Initialize the x vector with 0.5 for each element. This is the initial guess for + // the iterative solvers. It should be safe as for all 'maybe' states we know that the + // probability is strictly larger than 0. + std::vector* x = new std::vector(maybeStates.getNumberOfSetBits(), 0.5); + + // Prepare the right-hand side of the equation system. For entry i this corresponds to + // the accumulated probability of going from state i to some 'yes' state. + std::vector b(maybeStates.getNumberOfSetBits()); + dtmc.getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x); + + // Set up the precondition of the iterative solver. + gmm::ilu_precond> P(*gmmxxMatrix); + // Prepare an iteration object that determines the accuracy, maximum number of iterations + // and the like. + gmm::iteration iter(0.000001); + + // Now do the actual solving. + LOG4CPLUS_INFO(logger, "Starting iterations..."); + gmm::bicgstab(*gmmxxMatrix, x, b, P, iter); + LOG4CPLUS_INFO(logger, "Done with iterations."); + + // Create resulting vector and set values accordingly. + std::vector* result = new std::vector(dtmc.getNumberOfStates()); + mrmc::utility::setVectorValues>(result, maybeStates, x); + + // Delete temporary matrix and return result. + delete x; + delete gmmxxMatrix; + } + + mrmc::utility::setVectorValue>(result, notExistsPhiUntilPsiStates, 0); + mrmc::utility::setVectorValue>(result, alwaysPhiUntilPsiStates, 1); + + return result; + } +}; + +#endif /* GMMXXDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 932673be4..baa2f20d5 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -15,6 +15,7 @@ #include #include #include +#include #include "mrmc-config.h" #include "src/models/Dtmc.h" @@ -25,8 +26,6 @@ #include "src/parser/readPrctlFile.h" #include "src/solver/GraphAnalyzer.h" #include "src/utility/settings.h" -#include "Eigen/Sparse" -#include "gmm/gmm_matrix.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -107,9 +106,6 @@ int main(const int argc, const char* argv[]) { delete s; } - delete labparser.getLabeling(); - delete traparser.getMatrix(); - LOG4CPLUS_INFO(logger, "Nothing more to do, exiting."); return 0; diff --git a/src/solver/GraphAnalyzer.h b/src/solver/GraphAnalyzer.h index 6221250d5..34864520e 100644 --- a/src/solver/GraphAnalyzer.h +++ b/src/solver/GraphAnalyzer.h @@ -9,8 +9,12 @@ #define GRAPHANALYZER_H_ #include "src/models/Dtmc.h" +#include "src/exceptions/invalid_argument.h" -#include +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; namespace mrmc { @@ -24,17 +28,24 @@ public: * of the given target states whilst always staying in the set of filter states * before. The resulting states are written to the given bit vector. * @param model The model whose graph structure to search. - * @param targetStates The target states of the search. - * @param filterStates A set of states constraining the search. - * @param existentialReachabilityStates The result of the search. + * @param phiStates A bit vector of all states satisfying phi. + * @param psiStates A bit vector of all states satisfying psi. + * @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess + * a paths satisfying phi until psi. */ template - static void getExistsPhiUntilPsiStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector& existsPhiUntilPsiStates) { + static void getExistsPhiUntilPsiStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector* existsPhiUntilPsiStates) { + // Check for valid parameter. + if (existsPhiUntilPsiStates == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null."); + throw mrmc::exceptions::invalid_argument("Parameter 'existsPhiUntilPhiStates' must not be null."); + } + // Get the backwards transition relation from the model to ease the search. mrmc::models::GraphTransitions& backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. - existsPhiUntilPsiStates |= psiStates; + *existsPhiUntilPsiStates |= psiStates; // Initialize the stack used for the DFS with the states std::vector stack; @@ -47,8 +58,8 @@ public: stack.pop_back(); for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { - if (phiStates.get(*it) && !existsPhiUntilPsiStates.get(*it)) { - existsPhiUntilPsiStates.set(*it, true); + if (phiStates.get(*it) && !existsPhiUntilPsiStates->get(*it)) { + existsPhiUntilPsiStates->set(*it, true); stack.push_back(*it); } } @@ -62,16 +73,23 @@ public: * characterizes the states that possess at least one path to a target state. * The results are written to the given bit vector. * @param model The model whose graph structure to search. - * @param targetStates The target states of the search. - * @param filterStates A set of states constraining the search. - * @param existentialReachabilityStates The set of states that possess at - * least one path to a target state. - * @param universalReachabilityStates The result of the search. + * @param phiStates A bit vector of all states satisfying phi. + * @param psiStates A bit vector of all states satisfying psi. + * @param existsPhiUntilPsiStates A reference to a bit vector of states that possess a path + * satisfying phi until psi. + * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only + * have paths satisfying phi until psi. */ template - static void getAlwaysPhiUntilPsiStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, const mrmc::storage::BitVector& existsPhiUntilPsiStates, mrmc::storage::BitVector& alwaysPhiUntilPsiStates) { + static void getAlwaysPhiUntilPsiStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, const mrmc::storage::BitVector& existsPhiUntilPsiStates, mrmc::storage::BitVector* alwaysPhiUntilPsiStates) { + // Check for valid parameter. + if (alwaysPhiUntilPsiStates == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); + throw mrmc::exceptions::invalid_argument("Parameter 'alwaysPhiUntilPhiStates' must not be null."); + } + GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); - alwaysPhiUntilPsiStates.complement(); + alwaysPhiUntilPsiStates->complement(); } /*! @@ -79,15 +97,28 @@ public: * the given set of target states and only visit states from the filter set * before. * @param model The model whose graph structure to search. - * @param targetStates The target states of the search. - * @param filterStates A set of states constraining the search. - * @param universalReachabilityStates The result of the search. + * @param phiStates A bit vector of all states satisfying phi. + * @param psiStates A bit vector of all states satisfying psi. + * @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess + * a path satisfying phi until psi. + * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only + * have paths satisfying phi until psi. */ template - static void getAlwaysPhiUntilPsiStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector& alwaysPhiUntilPsiStates) { - mrmc::storage::BitVector existsPhiUntilPsiStates(model.getNumberOfStates()); + static void getPhiUntilPsiStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector* existsPhiUntilPsiStates, mrmc::storage::BitVector* alwaysPhiUntilPsiStates) { + // Check for valid parameters. + if (existsPhiUntilPsiStates == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null."); + throw mrmc::exceptions::invalid_argument("Parameter 'existsPhiUntilPhiStates' must not be null."); + } + if (alwaysPhiUntilPsiStates == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); + throw mrmc::exceptions::invalid_argument("Parameter 'alwaysPhiUntilPhiStates' must not be null."); + } + + // Perform search. GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, existsPhiUntilPsiStates); - GraphAnalyzer::getAlwaysPhiUntilPsiStates(model, phiStates, psiStates, existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); + GraphAnalyzer::getAlwaysPhiUntilPsiStates(model, phiStates, psiStates, *existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); } }; diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index 02cdec904..909bfee9f 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -4,6 +4,7 @@ #include #include #include +#include #include "boost/integer/integer_mask.hpp" #include "src/exceptions/invalid_state.h" @@ -113,19 +114,15 @@ public: ~SquareSparseMatrix() { setState(MatrixStatus::UnInitialized); if (valueStorage != nullptr) { - //free(value_storage); delete[] valueStorage; } if (columnIndications != nullptr) { - //free(column_indications); delete[] columnIndications; } if (rowIndications != nullptr) { - //free(row_indications); delete[] rowIndications; } if (diagonalStorage != nullptr) { - //free(diagonal_storage); delete[] diagonalStorage; } } @@ -570,40 +567,66 @@ public: * @return A pointer to a column-major sparse matrix in GMMXX format. */ gmm::csr_matrix* toGMMXXSparseMatrix() { + uint_fast64_t realNonZeros = getNonZeroEntryCount() + getDiagonalNonZeroEntryCount(); + LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); + // Prepare the resulting matrix. gmm::csr_matrix* result = new gmm::csr_matrix(rowCount, rowCount); - LOG4CPLUS_INFO(logger, "Starting copy1."); - // Copy over the row indications as GMMXX uses the very same internal format. + // Reserve enough elements for the row indications. result->jc.reserve(rowCount + 1); - std::copy(rowIndications, rowIndications + (rowCount + 1), result->jc.begin()); - LOG4CPLUS_INFO(logger, "Done copy1."); // For the column indications and the actual values, we have to gather // the values in a temporary array first, as we have to integrate - // the values from the diagonal. - uint_fast64_t realNonZeros = getNonZeroEntryCount() + getDiagonalNonZeroEntryCount(); + // the values from the diagonal. For the row indications, we can just count the number of + // inserted diagonal elements and add it to the previous value. uint_fast64_t* tmpColumnIndicationsArray = new uint_fast64_t[realNonZeros]; - uint_fast64_t* tmpValueArray = new uint_fast64_t[realNonZeros]; + T* tmpValueArray = new T[realNonZeros]; T zero(0); uint_fast64_t currentPosition = 0; + uint_fast64_t insertedDiagonalElements = 0; for (uint_fast64_t i = 0; i < rowCount; ++i) { - bool includedDiagonal = false; - for (uint_fast64_t j = rowIndications[i]; j < rowIndications[i + 1]; ++j) { - if (diagonalStorage[i] != zero && !includedDiagonal && columnIndications[j] > i) { - includedDiagonal = true; + // Compute correct start index of row. + result->jc[i] = rowIndications[i] + insertedDiagonalElements; + + // If the current row has no non-zero which is not on the diagonal, we have to check the + // diagonal element explicitly. + if (rowIndications[i + 1] - rowIndications[i] == 0) { + if (diagonalStorage[i] != zero) { tmpColumnIndicationsArray[currentPosition] = i; tmpValueArray[currentPosition] = diagonalStorage[i]; + ++currentPosition; ++insertedDiagonalElements; + } + } else { + // Otherwise, we can just enumerate the non-zeros which are not on the diagonal + // and fit in the diagonal element where appropriate. + bool includedDiagonal = false; + for (uint_fast64_t j = rowIndications[i]; j < rowIndications[i + 1]; ++j) { + if (diagonalStorage[i] != zero && !includedDiagonal && columnIndications[j] > i) { + includedDiagonal = true; + tmpColumnIndicationsArray[currentPosition] = i; + tmpValueArray[currentPosition] = diagonalStorage[i]; + ++currentPosition; ++insertedDiagonalElements; + } + tmpColumnIndicationsArray[currentPosition] = columnIndications[j]; + tmpValueArray[currentPosition] = valueStorage[j]; ++currentPosition; } - tmpColumnIndicationsArray[currentPosition] = columnIndications[j]; - tmpValueArray[currentPosition] = valueStorage[j]; + + // If the diagonal element is non-zero and was not inserted until now (i.e. all + // off-diagonal elements in the row are before the diagonal element. + if (!includedDiagonal && diagonalStorage[i] != zero) { + tmpColumnIndicationsArray[currentPosition] = i; + tmpValueArray[currentPosition] = diagonalStorage[i]; + ++currentPosition; ++insertedDiagonalElements; + } } } + // Fill in sentinel element at the end. + result->jc[rowCount] = realNonZeros; - LOG4CPLUS_INFO(logger, "Starting copy2."); // Now, we can copy the temporary array to the GMMXX format. - result->ir.reserve(realNonZeros); + result->ir.resize(realNonZeros); std::copy(tmpColumnIndicationsArray, tmpColumnIndicationsArray + realNonZeros, result->ir.begin()); delete[] tmpColumnIndicationsArray; @@ -611,7 +634,8 @@ public: result->pr.resize(realNonZeros); std::copy(tmpValueArray, tmpValueArray + realNonZeros, result->pr.begin()); delete[] tmpValueArray; - LOG4CPLUS_INFO(logger, "Done copy2."); + + LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format."); return result; } @@ -637,6 +661,15 @@ public: return result; } + /*! + * This function makes the rows given by the bit vector absorbing. + */ + bool makeRowsAbsorbing(const mrmc::storage::BitVector rows) { + for (auto row : rows) { + makeRowAbsorbing(row); + } + } + /*! * This function makes the given row absorbing. This means that all * entries in will be set to 0 and the value 1 will be written @@ -688,13 +721,15 @@ public: /*! * Computes a vector in which each element is the sum of those elements in the * corresponding row whose column bits are set to one in the given constraint. - * @param constraint A bit vector that indicates which columns to add. + * @param rowConstraint A bit vector that indicates for which rows to perform summation. + * @param columnConstraint A bit vector that indicates which columns to add. * @param resultVector A pointer to the resulting vector that has at least * as many elements as there are bits set to true in the constraint. */ - void getConstrainedRowCountVector(const mrmc::storage::BitVector& constraint, T* resultVector) { - for (uint_fast64_t row = 0; row < rowCount; ++row) { - resultVector[row] = getConstrainedRowSum(row, constraint); + void getConstrainedRowCountVector(const mrmc::storage::BitVector& rowConstraint, const mrmc::storage::BitVector& columnConstraint, std::vector* resultVector) { + uint_fast64_t currentRowCount = 0; + for (auto row : rowConstraint) { + resultVector[currentRowCount++] = getConstrainedRowSum(row, columnConstraint); } } @@ -724,8 +759,6 @@ public: } } - LOG4CPLUS_DEBUG(logger, "Done counting non-zeros."); - // Create and initialize resulting matrix. SquareSparseMatrix* result = new SquareSparseMatrix(constraint.getNumberOfSetBits()); result->initialize(subNonZeroEntries); @@ -765,6 +798,31 @@ public: return result; } + void convertToEquationSystem() { + invertDiagonal(); + negateAllNonDiagonalElements(); + } + + /*! + * Inverts all elements on the diagonal, i.e. sets the diagonal values to 1 minus their previous + * value. + */ + void invertDiagonal() { + T one(1); + for (uint_fast64_t i = 0; i < rowCount; ++i) { + diagonalStorage[i] = one - diagonalStorage[i]; + } + } + + /*! + * Negates all non-zero elements that are not on the diagonal. + */ + void negateAllNonDiagonalElements() { + for (uint_fast64_t i = 0; i < nonZeroEntryCount; ++i) { + valueStorage[i] = - valueStorage[i]; + } + } + /*! * Returns the size of the matrix in memory measured in bytes. * @return The size of the matrix in memory measured in bytes. @@ -802,6 +860,19 @@ public: return this->columnIndications + this->rowIndications[row + 1]; } + void print() { + std::cout << "diag: --------------------------------" << std::endl; + for (uint_fast64_t i = 0; i < rowCount; ++i) { + std::cout << "(" << i << "," << i << ") = " << diagonalStorage[i] << std::endl; + } + std::cout << "non diag: ----------------------------" << std::endl; + for (uint_fast64_t i = 0; i < rowCount; ++i) { + for (uint_fast64_t j = rowIndications[i]; j < rowIndications[i + 1]; ++j) { + std::cout << "(" << i << "," << columnIndications[j] << ") = " << valueStorage[j] << std::endl; + } + } + } + private: /*! diff --git a/src/utility/vector.h b/src/utility/vector.h new file mode 100644 index 000000000..393151745 --- /dev/null +++ b/src/utility/vector.h @@ -0,0 +1,34 @@ +/* + * vector.h + * + * Created on: 06.12.2012 + * Author: Christian Dehnert + */ + +#ifndef VECTOR_H_ +#define VECTOR_H_ + +namespace mrmc { + +namespace utility { + +template +void setVectorValues(std::vector* vector, const mrmc::storage::BitVector& positions, std::vector* values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + vector[position] = values[oldPosition++]; + } +} + +template +void setVectorValue(std::vector* vector, const mrmc::storage::BitVector& positions, T value) { + for (auto position : positions) { + vector[position] = value; + } +} + +} //namespace utility + +} //namespace mrmc + +#endif /* VECTOR_H_ */