diff --git a/src/modelchecker/csl/AbstractModelChecker.h b/src/modelchecker/csl/AbstractModelChecker.h index eed4aea0b..e25cd52f5 100644 --- a/src/modelchecker/csl/AbstractModelChecker.h +++ b/src/modelchecker/csl/AbstractModelChecker.h @@ -147,8 +147,7 @@ public: delete result; } } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); + std::cout << std::endl << "-------------------------------------------" << std::endl; } /*! @@ -177,8 +176,7 @@ public: delete result; } } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); + std::cout << std::endl << "-------------------------------------------" << std::endl; } /*! diff --git a/src/modelchecker/ltl/AbstractModelChecker.h b/src/modelchecker/ltl/AbstractModelChecker.h index 14f42553a..6ed75ceb0 100644 --- a/src/modelchecker/ltl/AbstractModelChecker.h +++ b/src/modelchecker/ltl/AbstractModelChecker.h @@ -131,8 +131,7 @@ public: delete result; } } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); + std::cout << std::endl << "-------------------------------------------" << std::endl; } /*! diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index 080d6198b..2ac3fd241 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -5,8 +5,17 @@ * Author: Thomas Heinemann */ -#ifndef STORM_MODELCHECKER_PRCTL_ABSTRACTMODELCHECKER_H_ -#define STORM_MODELCHECKER_PRCTL_ABSTRACTMODELCHECKER_H_ +#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ +#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ + +// Forward declaration of abstract model checker class needed by the formula classes. +namespace storm { +namespace modelchecker { +namespace prctl { + template class AbstractModelChecker; +} +} +} #include "src/exceptions/InvalidPropertyException.h" #include "src/formula/Prctl.h" @@ -151,8 +160,7 @@ public: delete result; } } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); + std::cout << std::endl << "-------------------------------------------" << std::endl; } /*! @@ -181,8 +189,7 @@ public: delete result; } } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); + std::cout << std::endl << "-------------------------------------------" << std::endl; } /*! diff --git a/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h b/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h index ad02fa8a6..6a1f82096 100644 --- a/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h @@ -8,7 +8,7 @@ #ifndef STORM_MODELCHECKER_PRCTL_EIGENDTMCPRCTLMODELCHECKER_H_ #define STORM_MODELCHECKER_PRCTL_EIGENDTMCPRCTLMODELCHECKER_H_ -#include "src/utility/Vector.h" +#include "src/utility/vector.h" #include "src/models/Dtmc.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" diff --git a/src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h index 4b4c31c82..60c473b49 100644 --- a/src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h @@ -35,7 +35,7 @@ public: * * @param model The DTMC to be checked. */ - explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : SparseDtmcPrctlModelChecker(dtmc) { + explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc const& dtmc) : SparseDtmcPrctlModelChecker(dtmc) { // Intentionally left empty. } @@ -278,7 +278,7 @@ private: xCurrent = swap; // Now check if the process already converged within our precision. - converged = storm::utility::equalModuloPrecision(*xCurrent, *xNext, precision, relative); + converged = storm::utility::vector::equalModuloPrecision(*xCurrent, *xNext, precision, relative); // Increase iteration count so we can abort if convergence is too slow. ++iterationCount; diff --git a/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h index bc846f15e..f5fb601f1 100644 --- a/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h @@ -53,12 +53,19 @@ public: private: - virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1) const { - // Get the starting row indices for the non-deterministic choices to reduce the resulting - // vector properly. - std::vector const& nondeterministicChoiceIndices = *this->getModel().getNondeterministicChoiceIndices(); - - + /*! + * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes x[i+1] = A*x[i] + b + * until x[n], where x[0] = x. + * + * @param A The matrix that is to be multiplied against the vector. + * @param x The initial vector that is to be multiplied against the matrix. This is also the output parameter, + * i.e. after the method returns, this vector will contain the computed values. + * @param nondeterministicChoiceIndices The assignment of states to their rows in the matrix. + * @param b If not null, this vector is being added to the result after each matrix-vector multiplication. + * @param n Specifies the number of iterations the matrix-vector multiplication is performed. + * @returns The result of the repeated matrix-vector multiplication as the content of the parameter vector. + */ + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& nondeterministicChoiceIndices, std::vector* b = nullptr, uint_fast64_t n = 1) const { // Transform the transition probability matrix to the gmm++ format to use its arithmetic. gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A); @@ -75,9 +82,9 @@ private: } if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(multiplyResult, &x, nondeterministicChoiceIndices); + storm::utility::vector::reduceVectorMin(multiplyResult, x, nondeterministicChoiceIndices); } else { - storm::utility::reduceVectorMax(multiplyResult, &x, nondeterministicChoiceIndices); + storm::utility::vector::reduceVectorMax(multiplyResult, x, nondeterministicChoiceIndices); } } @@ -125,13 +132,13 @@ private: // Reduce the vector x' by applying min/max for all non-deterministic choices. if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(multiplyResult, newX, nondeterministicChoiceIndices); + storm::utility::vector::reduceVectorMin(multiplyResult, *newX, nondeterministicChoiceIndices); } else { - storm::utility::reduceVectorMax(multiplyResult, newX, nondeterministicChoiceIndices); + storm::utility::vector::reduceVectorMax(multiplyResult, *newX, nondeterministicChoiceIndices); } // Determine whether the method converged. - converged = storm::utility::equalModuloPrecision(*currentX, *newX, precision, relative); + converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative); // Update environment variables. swap = currentX; diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 2f7b8048d..36f2ff9ee 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -10,7 +10,7 @@ #include "src/modelchecker/prctl/AbstractModelChecker.h" #include "src/models/Dtmc.h" -#include "src/utility/Vector.h" +#include "src/utility/vector.h" #include "src/utility/graph.h" #include @@ -89,19 +89,31 @@ public: storm::storage::BitVector* leftStates = formula.getLeft().check(*this); storm::storage::BitVector* rightStates = formula.getRight().check(*this); - // Copy the matrix before we make any changes. - storm::storage::SparseMatrix tmpMatrix(*this->getModel().getTransitionMatrix()); - - // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. - tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); + // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the + // further analysis. + storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(this->getModel(), *leftStates, *rightStates, true, formula.getBound()); + + // Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0. + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); + + // Compute the new set of target states in the reduced system. + storm::storage::BitVector rightStatesInReducedSystem = maybeStates % *rightStates; + + // Make all rows absorbing that satisfy the second sub-formula. + submatrix.makeRowsAbsorbing(rightStatesInReducedSystem); // Create the vector with which to multiply. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); + std::vector subresult(maybeStates.getNumberOfSetBits()); + storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne()); // Perform the matrix vector multiplication as often as required by the formula bound. - this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound()); + this->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound()); + // Create result vector and set its values accordingly. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + storm::utility::vector::setVectorValues(*result, maybeStates, subresult); + storm::utility::vector::setVectorValues(*result, ~maybeStates, storm::utility::constGetZero()); + // Delete obsolete intermediates and return result. delete leftStates; delete rightStates; @@ -125,7 +137,7 @@ public: // Create the vector with which to multiply and initialize it correctly. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(*result, *nextStates, storm::utility::constGetOne()); // Delete obsolete intermediate. delete nextStates; @@ -188,7 +200,7 @@ public: std::vector* result = this->checkEventually(temporaryEventuallyFormula, qualitative); // Now subtract the resulting vector from the constant one vector to obtain final result. - storm::utility::subtractFromConstantOneVector(result); + storm::utility::vector::subtractFromConstantOneVector(*result); return result; } @@ -249,16 +261,16 @@ public: this->solveEquationSystem(submatrix, x, b); // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, x); + storm::utility::vector::setVectorValues(*result, maybeStates, x); } else if (qualitative) { // If we only need a qualitative result, we can safely assume that the results will only be compared to // bounds which are either 0 or 1. Setting the value to 0.5 is thus safe. - storm::utility::setVectorValues(result, maybeStates, Type(0.5)); + storm::utility::vector::setVectorValues(*result, maybeStates, Type(0.5)); } // Set values of resulting vector that are known exactly. - storm::utility::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(*result, statesWithProbability0, storm::utility::constGetZero()); + storm::utility::vector::setVectorValues(*result, statesWithProbability1, storm::utility::constGetOne()); return result; } @@ -385,7 +397,7 @@ public: // side to the vector resulting from summing the rows of the pointwise product // of the transition probability matrix and the transition reward matrix. std::vector pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); - storm::utility::selectVectorValues(&b, maybeStates, pointwiseProductRowSumVector); + storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector); if (this->getModel().hasStateRewards()) { // If a state-based reward model is also available, we need to add this vector @@ -393,7 +405,7 @@ public: // that we still consider (i.e. maybeStates), we need to extract these values // first. std::vector subStateRewards(maybeStatesSetBitCount); - storm::utility::selectVectorValues(&subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); + storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); gmm::add(subStateRewards, b); } } else { @@ -401,19 +413,19 @@ public: // right-hand side. As the state reward vector contains entries not just for the // states that we still consider (i.e. maybeStates), we need to extract these values // first. - storm::utility::selectVectorValues(&b, maybeStates, *this->getModel().getStateRewardVector()); + storm::utility::vector::selectVectorValues(b, maybeStates, *this->getModel().getStateRewardVector()); } // Now solve the resulting equation system. this->solveEquationSystem(submatrix, x, b); // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, x); + storm::utility::vector::setVectorValues(*result, maybeStates, x); } // Set values of resulting vector that are known exactly. - storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); + storm::utility::vector::setVectorValues(*result, *targetStates, storm::utility::constGetZero()); + storm::utility::vector::setVectorValues(*result, infinityStates, storm::utility::constGetInfinity()); // Delete temporary storages and return result. delete targetStates; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index f0a359a11..81c9b45e1 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -10,7 +10,7 @@ #include "src/modelchecker/prctl/AbstractModelChecker.h" #include "src/models/Mdp.h" -#include "src/utility/Vector.h" +#include "src/utility/vector.h" #include "src/utility/graph.h" #include @@ -94,18 +94,37 @@ public: // First, we need to compute the states that satisfy the sub-formulas of the until-formula. storm::storage::BitVector* leftStates = formula.getLeft().check(*this); storm::storage::BitVector* rightStates = formula.getRight().check(*this); + + // Determine the states that have 0 probability of reaching the target states. + storm::storage::BitVector maybeStates; + if (this->minimumOperatorStack.top()) { + maybeStates = storm::utility::graph::performProbGreater0A(this->getModel(), this->getModel().getBackwardTransitions(), *leftStates, *rightStates, true, formula.getBound()); + } else { + maybeStates = storm::utility::graph::performProbGreater0E(this->getModel(), this->getModel().getBackwardTransitions(), *leftStates, *rightStates, true, formula.getBound()); + } + + // Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0. + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); - // Copy the matrix before we make any changes. - storm::storage::SparseMatrix tmpMatrix(*this->getModel().getTransitionMatrix()); + // Get the "new" nondeterministic choice indices for the submatrix. + std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); - // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. - tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates, *this->getModel().getNondeterministicChoiceIndices()); - - // Create the vector with which to multiply. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); + // Compute the new set of target states in the reduced system. + storm::storage::BitVector rightStatesInReducedSystem = maybeStates % *rightStates; - this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound()); + // Make all rows absorbing that satisfy the second sub-formula. + submatrix.makeRowsAbsorbing(rightStatesInReducedSystem, subNondeterministicChoiceIndices); + + // Create the vector with which to multiply. + std::vector subresult(maybeStates.getNumberOfSetBits()); + storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne()); + + this->performMatrixVectorMultiplication(submatrix, subresult, subNondeterministicChoiceIndices, nullptr, formula.getBound()); + + // Create the resulting vector. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + storm::utility::vector::setVectorValues(*result, maybeStates, subresult); + storm::utility::vector::setVectorValues(*result, ~maybeStates, storm::utility::constGetZero()); // Delete intermediate results and return result. delete leftStates; @@ -130,12 +149,12 @@ public: // Create the vector with which to multiply and initialize it correctly. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(*result, *nextStates, storm::utility::constGetOne()); // Delete obsolete sub-result. delete nextStates; - this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result); + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, *this->getModel().getNondeterministicChoiceIndices()); // Return result. return result; @@ -155,7 +174,7 @@ public: virtual std::vector* checkBoundedEventually(const storm::property::prctl::BoundedEventually& formula, bool qualitative) const { // Create equivalent temporary bounded until formula and check it. storm::property::prctl::BoundedUntil temporaryBoundedUntilFormula(new storm::property::prctl::Ap("true"), formula.getChild().clone(), formula.getBound()); - return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative); + return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative); } /*! @@ -192,7 +211,7 @@ public: std::vector* result = this->checkEventually(temporaryEventuallyFormula, qualitative); // Now subtract the resulting vector from the constant one vector to obtain final result. - storm::utility::subtractFromConstantOneVector(result); + storm::utility::vector::subtractFromConstantOneVector(*result); return result; } @@ -256,12 +275,12 @@ public: this->solveEquationSystem(submatrix, x, b, subNondeterministicChoiceIndices); // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, x); + storm::utility::vector::setVectorValues(*result, maybeStates, x); } // Set values of resulting vector that are known exactly. - storm::utility::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(*result, statesWithProbability0, storm::utility::constGetZero()); + storm::utility::vector::setVectorValues(*result, statesWithProbability1, storm::utility::constGetOne()); return result; } @@ -287,7 +306,7 @@ public: // Initialize result to state rewards of the model. std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); - this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound()); + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, *this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound()); // Return result. return result; @@ -330,7 +349,7 @@ public: result = new std::vector(this->getModel().getNumberOfStates()); } - this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, &totalRewardVector, formula.getBound()); + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, *this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound()); // Delete temporary variables and return result. return result; @@ -397,36 +416,35 @@ public: // side to the vector resulting from summing the rows of the pointwise product // of the transition probability matrix and the transition reward matrix. std::vector pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); - storm::utility::selectVectorValues(&b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), pointwiseProductRowSumVector); + storm::utility::vector::selectVectorValues(b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), pointwiseProductRowSumVector); if (this->getModel().hasStateRewards()) { // If a state-based reward model is also available, we need to add this vector // as well. As the state reward vector contains entries not just for the states // that we still consider (i.e. maybeStates), we need to extract these values // first. - std::vector* subStateRewards = new std::vector(b.size()); - storm::utility::selectVectorValuesRepeatedly(subStateRewards, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector()); - gmm::add(*subStateRewards, b); - delete subStateRewards; + std::vector subStateRewards(b.size()); + storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector()); + gmm::add(subStateRewards, b); } } else { // If only a state-based reward model is available, we take this vector as the // right-hand side. As the state reward vector contains entries not just for the // states that we still consider (i.e. maybeStates), we need to extract these values // first. - storm::utility::selectVectorValuesRepeatedly(&b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector()); + storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector()); } // Solve the corresponding system of equations. this->solveEquationSystem(submatrix, x, b, subNondeterministicChoiceIndices); // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, x); + storm::utility::vector::setVectorValues(*result, maybeStates, x); } // Set values of resulting vector that are known exactly. - storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); + storm::utility::vector::setVectorValues(*result, *targetStates, storm::utility::constGetZero()); + storm::utility::vector::setVectorValues(*result, infinityStates, storm::utility::constGetInfinity()); // Delete temporary storages and return result. delete targetStates; @@ -448,15 +466,12 @@ private: * @param A The matrix that is to be multiplied against the vector. * @param x The initial vector that is to be multiplied against the matrix. This is also the output parameter, * i.e. after the method returns, this vector will contain the computed values. + * @param nondeterministicChoiceIndices The assignment of states to their rows in the matrix. * @param b If not null, this vector is being added to the result after each matrix-vector multiplication. * @param n Specifies the number of iterations the matrix-vector multiplication is performed. * @returns The result of the repeated matrix-vector multiplication as the content of the parameter vector. */ - virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1) const { - // Get the starting row indices for the non-deterministic choices to reduce the resulting - // vector properly. - std::vector const& nondeterministicChoiceIndices = *this->getModel().getNondeterministicChoiceIndices(); - + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& nondeterministicChoiceIndices, std::vector* b = nullptr, uint_fast64_t n = 1) const { // Create vector for result of multiplication, which is reduced to the result vector after // each multiplication. std::vector multiplyResult(A.getRowCount()); @@ -467,15 +482,15 @@ private: // Add b if it is non-null. if (b != nullptr) { - storm::utility::addVectors(multiplyResult, *b); + storm::utility::vector::addVectorsInPlace(multiplyResult, *b); } // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(multiplyResult, &x, nondeterministicChoiceIndices); + storm::utility::vector::reduceVectorMin(multiplyResult, x, nondeterministicChoiceIndices); } else { - storm::utility::reduceVectorMax(multiplyResult, &x, nondeterministicChoiceIndices); + storm::utility::vector::reduceVectorMax(multiplyResult, x, nondeterministicChoiceIndices); } } } @@ -487,6 +502,7 @@ private: * @param x The solution vector x. The initial values of x represent a guess of the real values to the solver, but * may be ignored. * @param b The right-hand side of the equation system. + * @param nondeterministicChoiceIndices The assignment of states to their rows in the matrix. * @returns The solution vector x of the system of linear equations as the content of the parameter x. */ virtual void solveEquationSystem(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const { @@ -511,18 +527,18 @@ private: while (!converged && iterations < maxIterations) { // Compute x' = A*x + b. A.multiplyWithVector(*currentX, multiplyResult); - storm::utility::addVectors(multiplyResult, b); + storm::utility::vector::addVectorsInPlace(multiplyResult, b); // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(multiplyResult, newX, nondeterministicChoiceIndices); + storm::utility::vector::reduceVectorMin(multiplyResult, *newX, nondeterministicChoiceIndices); } else { - storm::utility::reduceVectorMax(multiplyResult, newX, nondeterministicChoiceIndices); + storm::utility::vector::reduceVectorMax(multiplyResult, *newX, nondeterministicChoiceIndices); } // Determine whether the method converged. - converged = storm::utility::equalModuloPrecision(*currentX, *newX, precision, relative); + converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative); // Update environment variables. swap = currentX; diff --git a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h index 7fbbb2351..61f67a623 100644 --- a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h @@ -68,9 +68,9 @@ private: bool relative = s->get("relative"); // Now, we need to determine the SCCs of the MDP and a topological sort. - std::vector> stronglyConnectedComponents = storm::utility::GraphAnalyzer::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + std::vector> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); - std::vector topologicalSort = storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); + std::vector topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); // Set up the environment for the power method. std::vector multiplyResult(matrix.getRowCount()); diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index c4896a6c6..5d99b0f8f 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -4,7 +4,6 @@ #include "src/models/AtomicPropositionsLabeling.h" #include "src/storage/BitVector.h" #include "src/storage/SparseMatrix.h" -#include "src/utility/CommandLine.h" #include #include @@ -86,55 +85,53 @@ class AbstractModel: public std::enable_shared_from_this> { virtual ModelType getType() const = 0; /*! - * Extracts the SCC dependency graph from the model according to the given SCC decomposition. + * Extracts the dependency graph from the model according to the given partition. * - * @param stronglyConnectedComponents A vector containing the SCCs of the system. - * @param stateToSccMap A mapping from state indices to + * @param partition A vector containing the blocks of the partition of the system. + * @return A sparse matrix with bool entries that represents the dependency graph of the blocks of the partition. */ - storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents) const { - uint_fast64_t numberOfStates = stronglyConnectedComponents.size(); + storm::storage::SparseMatrix extractPartitionDependencyGraph(std::vector> const& partition) const { + uint_fast64_t numberOfStates = partition.size(); // First, we need to create a mapping of states to their SCC index, to ease the computation // of dependency transitions later. - std::vector stateToSccMap(this->getNumberOfStates()); + std::vector stateToBlockMap(this->getNumberOfStates()); for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (uint_fast64_t j = 0; j < stronglyConnectedComponents[i].size(); ++j) { - stateToSccMap[stronglyConnectedComponents[i][j]] = i; + for (uint_fast64_t j = 0; j < partition[i].size(); ++j) { + stateToBlockMap[partition[i][j]] = i; } } - // The resulting sparse matrix will have as many rows/columns as there are SCCs. - - storm::storage::SparseMatrix sccDependencyGraph(numberOfStates); - sccDependencyGraph.initialize(); + // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition. + storm::storage::SparseMatrix dependencyGraph(numberOfStates); + dependencyGraph.initialize(); - for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) { - // Get the actual SCC. - std::vector const& scc = stronglyConnectedComponents[currentSccIndex]; + for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < partition.size(); ++currentBlockIndex) { + // Get the next block. + std::vector const& block = partition[currentBlockIndex]; - // Now, we determine the SCCs which are reachable (in one step) from the current SCC. - std::set allTargetSccs; - for (auto state : scc) { + // 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 targetScc = stateToSccMap[*succIt]; + uint_fast64_t targetBlock = stateToBlockMap[*succIt]; // We only need to consider transitions that are actually leaving the SCC. - if (targetScc != currentSccIndex) { - allTargetSccs.insert(targetScc); + if (targetBlock != currentBlockIndex) { + allTargetBlocks.insert(targetBlock); } } } // Now we can just enumerate all the target SCCs and insert the corresponding transitions. - for (auto targetScc : allTargetSccs) { - sccDependencyGraph.insertNextValue(currentSccIndex, targetScc, true); + for (auto targetBlock : allTargetBlocks) { + dependencyGraph.insertNextValue(currentBlockIndex, targetBlock, true); } } - // Finalize the matrix. - sccDependencyGraph.finalize(true); - - return sccDependencyGraph; + // Finalize the matrix and return result. + dependencyGraph.finalize(true); + return dependencyGraph; } /*! @@ -333,7 +330,7 @@ class AbstractModel: public std::enable_shared_from_this> { << std::endl; } - protected: +protected: /*! A matrix representing the likelihoods of moving between states. */ std::shared_ptr> transitionMatrix; diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index fe5cb5a30..d412b2eb7 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -111,8 +111,8 @@ public: BitVector(uint_fast64_t length, bool initTrue = false) : bitCount(length), endIterator(*this, length, length, false), truncateMask((1ll << (bitCount & mod64mask)) - 1ll) { // Check whether the given length is valid. if (length == 0) { - LOG4CPLUS_ERROR(logger, "Trying to create bit vector of size 0."); - throw storm::exceptions::InvalidArgumentException("Trying to create a bit vector of size 0."); + LOG4CPLUS_ERROR(logger, "Cannot create bit vector of size 0."); + throw storm::exceptions::InvalidArgumentException() << "Cannot create bit vector of size 0."; } // Compute the correct number of buckets needed to store the given number of bits @@ -272,7 +272,7 @@ public: */ void set(const uint_fast64_t index, const bool value) { uint_fast64_t bucket = index >> 6; - if (bucket >= this->bucketCount) throw storm::exceptions::OutOfRangeException(); + if (bucket >= this->bucketCount) throw storm::exceptions::OutOfRangeException() << "Written index " << index << " out of bounds."; uint_fast64_t mask = static_cast(1) << (index & mod64mask); if (value) { this->bucketArray[bucket] |= mask; @@ -290,7 +290,7 @@ public: */ bool get(const uint_fast64_t index) const { uint_fast64_t bucket = index >> 6; - if (bucket >= this->bucketCount) throw storm::exceptions::OutOfRangeException(); + if (bucket >= this->bucketCount) throw storm::exceptions::OutOfRangeException() << "Read index " << index << " out of bounds."; uint_fast64_t mask = static_cast(1) << (index & mod64mask); return ((this->bucketArray[bucket] & mask) == mask); } @@ -469,6 +469,41 @@ public: } return true; } + + /*! + * Computes a bit vector such that bit i is set iff the i-th set bit of the current bit vector is also contained + * in the given bit vector. + * + * @param bv A reference the bit vector to be used. + * @return A bit vector whose i-th bit is set iff the i-th set bit of the current bit vector is also contained + * in the given bit vector. + */ + BitVector operator%(BitVector const& bv) const { + // Create resulting bit vector. + BitVector result(this->getNumberOfSetBits()); + + // If the current bit vector has not too many elements compared to the given bit vector we prefer iterating + // over its elements. + if (this->getNumberOfSetBits() / 10 < bv.getNumberOfSetBits()) { + uint_fast64_t position = 0; + for (auto bit : *this) { + if (bv.get(bit)) { + result.set(position, true); + } + ++position; + } + } else { + // If the given bit vector had much less elements, we iterate over its elements and accept calling the more + // costly operation getNumberOfSetBitsBeforeIndex on the current bit vector. + for (auto bit : bv) { + if (this->get(bit)) { + result.set(this->getNumberOfSetBitsBeforeIndex(bit), true); + } + } + } + + return result; + } /*! * Adds all indices of bits set to one to the provided list. @@ -565,7 +600,7 @@ public: */ std::string toString() const { std::stringstream result; - result << "bit vector(" << this->getNumberOfSetBits() << ") ["; + result << "bit vector(" << this->getNumberOfSetBits() << "/" << bitCount << ") ["; for (auto index : *this) { result << index << " "; } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 566629f3c..4ee005881 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -592,7 +592,7 @@ public: // Check whether the accessed state exists. if (row > rowCount) { LOG4CPLUS_ERROR(logger, "Trying to make an illegal row " << row << " absorbing."); - throw storm::exceptions::OutOfRangeException("Trying to make an illegal row absorbing."); + throw storm::exceptions::OutOfRangeException() << "Trying to make an illegal row " << row << " absorbing."; return false; } @@ -713,14 +713,18 @@ public: SparseMatrix result(constraint.getNumberOfSetBits()); result.initialize(subNonZeroEntries); - // Create a temporary array that stores for each index whose bit is set - // to true the number of bits that were set before that particular index. - uint_fast64_t* bitsSetBeforeIndex = new uint_fast64_t[colCount]; + // Create a temporary vecotr that stores for each index whose bit is set + // to true the number of bits that were set before that particular index. + std::vector bitsSetBeforeIndex; + bitsSetBeforeIndex.reserve(colCount); + + // Compute the information to fill this vector. uint_fast64_t lastIndex = 0; uint_fast64_t currentNumberOfSetBits = 0; for (auto index : constraint) { while (lastIndex <= index) { - bitsSetBeforeIndex[lastIndex++] = currentNumberOfSetBits; + bitsSetBeforeIndex.push_back(currentNumberOfSetBits); + ++lastIndex; } ++currentNumberOfSetBits; } @@ -737,9 +741,6 @@ public: ++rowCount; } - // Dispose of the temporary array. - delete[] bitsSetBeforeIndex; - // Finalize sub-matrix and return result. result.finalize(); LOG4CPLUS_DEBUG(logger, "Done creating sub-matrix."); @@ -758,8 +759,7 @@ public: SparseMatrix getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, std::vector const& rowGroupIndices) const { LOG4CPLUS_DEBUG(logger, "Creating a sub-matrix (of unknown size)."); - // First, we need to determine the number of non-zero entries and the number of rows of the - // sub-matrix. + // First, we need to determine the number of non-zero entries and the number of rows of the sub-matrix. uint_fast64_t subNonZeroEntries = 0; uint_fast64_t subRowCount = 0; for (auto index : rowGroupConstraint) { @@ -779,14 +779,18 @@ public: SparseMatrix result(subRowCount, rowGroupConstraint.getNumberOfSetBits()); result.initialize(subNonZeroEntries); - // Create a temporary array that stores for each index whose bit is set + // Create a temporary vector that stores for each index whose bit is set // to true the number of bits that were set before that particular index. - uint_fast64_t* bitsSetBeforeIndex = new uint_fast64_t[colCount]; + std::vector bitsSetBeforeIndex; + bitsSetBeforeIndex.reserve(colCount); + + // Compute the information to fill this vector. uint_fast64_t lastIndex = 0; uint_fast64_t currentNumberOfSetBits = 0; for (auto index : rowGroupConstraint) { while (lastIndex <= index) { - bitsSetBeforeIndex[lastIndex++] = currentNumberOfSetBits; + bitsSetBeforeIndex.push_back(currentNumberOfSetBits); + ++lastIndex; } ++currentNumberOfSetBits; } @@ -804,9 +808,6 @@ public: } } - // Dispose of the temporary array. - delete[] bitsSetBeforeIndex; - // Finalize sub-matrix and return result. result.finalize(); LOG4CPLUS_DEBUG(logger, "Done creating sub-matrix."); diff --git a/src/storm.cpp b/src/storm.cpp index 0ddc1c970..1fcd0c1ec 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -124,6 +124,7 @@ void printHeader(const int argc, const char* argv[]) { std::cout << "-----" << std::endl << std::endl; std::cout << "Version: 1.0 Alpha" << std::endl; + // "Compute" the command line argument string with which STORM was invoked. std::stringstream commandStream; for (int i = 0; i < argc; ++i) { @@ -133,14 +134,8 @@ void printHeader(const int argc, const char* argv[]) { } /*! - * Prints the footer. - */ -void printFooter() { - std::cout << "Nothing more to do, exiting." << std::endl; -} - -/*! - * Function that parses the command line options. + * Parses the given command line arguments. + * * @param argc The argc argument of main(). * @param argv The argv argument of main(). * @return True iff the program should continue to run after parsing the options. @@ -181,126 +176,77 @@ bool parseOptions(const int argc, const char* argv[]) { return true; } +/*! + * Performs some necessary initializations. + */ void setUp() { + // Increase the precision of output. std::cout.precision(10); } /*! - * Function to perform some cleanup. + * Performs some necessary clean-up. */ void cleanUp() { delete storm::utility::cuddUtilityInstance(); } /*! - * Factory style creation of new DTMC model checker - * @param dtmc The Dtmc that the model checker will check - * @return + * Creates a model checker for the given DTMC that complies with the given options. + * + * @param dtmc A reference to the DTMC for which the model checker is to be created. + * @return A pointer to the resulting model checker. */ storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Dtmc& dtmc) { + // Create the appropriate model checker. storm::settings::Settings* s = storm::settings::instance(); if (s->getString("matrixlib") == "gmm++") { return new storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker(dtmc); } - // The control flow should never reach this point, as there is a default setting for matrixlib (gmm++) - std::string message = "No matrix library suitable for DTMC model checking has been set"; + + // The control flow should never reach this point, as there is a default setting for matrixlib. + std::string message = "No matrix library suitable for DTMC model checking has been set."; throw storm::exceptions::InvalidSettingsException() << message; return nullptr; } /*! - * Factory style creation of new MDP model checker + * Creates a model checker for the given MDP that complies with the given options. + * * @param mdp The Dtmc that the model checker will check * @return */ storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp& mdp) { + // Create the appropriate model checker. storm::settings::Settings* s = storm::settings::instance(); if (s->getString("matrixlib") == "gmm++") { return new storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker(mdp); - } - // The control flow should never reach this point, as there is a default setting for matrixlib (gmm++) - std::string message = "No matrix library suitable for MDP model checking has been set"; + } else if (s->getString("matrixlib") == "native") { + return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp); + } + + // The control flow should never reach this point, as there is a default setting for matrixlib. + std::string message = "No matrix library suitable for MDP model checking has been set."; throw storm::exceptions::InvalidSettingsException() << message; return nullptr; } /*! - * Calls the check method of a model checker for all PRCTL formulas in a given list. + * Checks the PRCTL formulae provided on the command line on the given model checker. * - * @param formulaList The list of PRCTL formulas - * @param mc the model checker + * @param modelchecker The model checker that is to be invoked on all given formulae. */ -void checkPrctlFormulasAgainstModel(std::list*>& formulaList, - storm::modelchecker::prctl::AbstractModelChecker const& mc) { - for ( auto formula : formulaList ) { - mc.check(*formula); - - //TODO: Should that be done here or in a second iteration through the list? - delete formula; - } - formulaList.clear(); -} - -/*! - * Check method for DTMCs - * @param dtmc Reference to the DTMC to check - */ -void checkMdp(std::shared_ptr> mdp) { - mdp->printModelInformationToStream(std::cout); +void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker const& modelchecker) { storm::settings::Settings* s = storm::settings::instance(); if (s->isSet("prctl")) { - LOG4CPLUS_INFO(logger, "Parsing prctl file"+ s->getString("prctl")); + LOG4CPLUS_INFO(logger, "Parsing prctl file: " << s->getString("prctl") << "."); storm::parser::PrctlFileParser fileParser; std::list*> formulaList = fileParser.parseFormulas(s->getString("prctl")); - - storm::modelchecker::prctl::AbstractModelChecker* mc = createPrctlModelChecker(*mdp); - - checkPrctlFormulasAgainstModel(formulaList, *mc); - - delete mc; - } - - if(s->isSet("csl")) { - LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on MDPs."); - } -} - -/*! - * Check method for DTMCs - * @param dtmc Reference to the DTMC to check - */ -void checkDtmc(std::shared_ptr> dtmc) { - dtmc->printModelInformationToStream(std::cout); - storm::settings::Settings* s = storm::settings::instance(); - if (s->isSet("prctl")) { - LOG4CPLUS_INFO(logger, "Parsing prctl file"+ s->getString("prctl")); - storm::parser::PrctlFileParser fileParser; - std::list*> formulaList = fileParser.parseFormulas(s->getString("prctl")); - - storm::modelchecker::prctl::AbstractModelChecker* mc = createPrctlModelChecker(*dtmc); - - checkPrctlFormulasAgainstModel(formulaList, *mc); - - delete mc; - } - - if (s->isSet("ltl")) { - LOG4CPLUS_INFO(logger, "Parsing ltl file"+ s->getString("ltl")); - storm::parser::LtlFileParser fileParser; - std::list*> formulaList = fileParser.parseFormulas(s->getString("ltl")); - - LOG4CPLUS_ERROR(logger, "LTL model checking is not implemented yet."); - - //Debug output while LTL formulas cannot be checked - for (auto formula : formulaList) { - LOG4CPLUS_DEBUG(logger, formula->toString()); - } - - - } - - if(s->isSet("csl")) { - LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on DTMCs."); + + for (auto formula : formulaList) { + modelchecker.check(*formula); + delete formula; + } } } @@ -308,56 +254,66 @@ void checkDtmc(std::shared_ptr> dtmc) { * Main entry point. */ int main(const int argc, const char* argv[]) { - // Catch segfaults and display a backtrace. + // Register a signal handler to catch segfaults and display a backtrace. installSignalHandler(); + // Print an information header. printHeader(argc, argv); + // Initialize the logging engine and perform other initalizations. initializeLogger(); - setUp(); try { LOG4CPLUS_INFO(logger, "StoRM was invoked."); - // Parse options + // Parse options. if (!parseOptions(argc, argv)) { - // If false is returned, the program execution is stopped here - // E.g. if the user asked to see the help text + // If parsing failed or the option to see the usage was set, program execution stops here. return 0; } - // Now, the settings are receivd and the model is parsed. + // Now, the settings are received and the specified model is parsed. The actual actions taken depend on whether + // the model was provided in explicit or symbolic format. storm::settings::Settings* s = storm::settings::instance(); if (s->isSet("explicit")) { std::vector args = s->get>("explicit"); storm::parser::AutoParser parser(args[0], args[1], s->getString("staterew"), s->getString("transrew")); + // Determine which engine is to be used to choose the right model checker. LOG4CPLUS_DEBUG(logger, s->getString("matrixlib")); - - // Depending on the model type, the respective model checking procedure is chosen. + // Depending on the model type, the appropriate model checking procedure is chosen. + storm::modelchecker::prctl::AbstractModelChecker* modelchecker = nullptr; switch (parser.getType()) { case storm::models::DTMC: - LOG4CPLUS_INFO(logger, "Model was detected as DTMC"); - checkDtmc(parser.getModel>()); + LOG4CPLUS_INFO(logger, "Model is a DTMC."); + modelchecker = createPrctlModelChecker(*parser.getModel>()); + checkPrctlFormulae(*modelchecker); break; case storm::models::MDP: - LOG4CPLUS_INFO(logger, "Model was detected as MDP"); - checkMdp(parser.getModel>()); + LOG4CPLUS_INFO(logger, "Model is an MDP."); + modelchecker = createPrctlModelChecker(*parser.getModel>()); + checkPrctlFormulae(*modelchecker); break; case storm::models::CTMC: + LOG4CPLUS_INFO(logger, "Model is a CTMC."); + LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); + break; case storm::models::CTMDP: - // Continuous time model checking is not implemented yet - LOG4CPLUS_ERROR(logger, "The model type you selected is not supported in this version of storm."); + LOG4CPLUS_INFO(logger, "Model is a CTMC."); + LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); break; case storm::models::Unknown: default: LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); break; } - } - if (s->isSet("symbolic")) { + + if (modelchecker != nullptr) { + delete modelchecker; + } + } else if (s->isSet("symbolic")) { std::string arg = s->getString("symbolic"); storm::parser::PrismParser parser; storm::adapters::ExplicitModelAdapter adapter(parser.parseFile(arg)); @@ -365,13 +321,12 @@ int main(const int argc, const char* argv[]) { model->printModelInformationToStream(std::cout); } + // Perform clean-up and terminate. cleanUp(); - - LOG4CPLUS_INFO(logger, "StoRM quit."); - + LOG4CPLUS_INFO(logger, "StoRM terminating."); return 0; } catch (std::exception& e) { - LOG4CPLUS_FATAL(logger, "An exception was thrown but not catched. All we can do now is show it to you and die in peace..."); + LOG4CPLUS_FATAL(logger, "An exception was thrown. Terminating."); LOG4CPLUS_FATAL(logger, "\t" << e.what()); } return 1; diff --git a/src/utility/CommandLine.cpp b/src/utility/CommandLine.cpp deleted file mode 100644 index f8f8321b4..000000000 --- a/src/utility/CommandLine.cpp +++ /dev/null @@ -1,18 +0,0 @@ -/* - * CommandLine.cpp - * - * Created on: 26.12.2012 - * Author: Christian Dehnert - */ - -#include - -namespace storm { -namespace utility { - -void printSeparationLine(std::ostream& out) { - out << "------------------------------------------------------" << std::endl; -} - -} // namespace utility -} // namespace storm diff --git a/src/utility/CommandLine.h b/src/utility/CommandLine.h deleted file mode 100644 index 134706ec2..000000000 --- a/src/utility/CommandLine.h +++ /dev/null @@ -1,24 +0,0 @@ -/* - * CommandLine.h - * - * Created on: 26.12.2012 - * Author: Christian Dehnert - */ - -#ifndef STORM_UTILITY_COMMANDLINE_H_ -#define STORM_UTILITY_COMMANDLINE_H_ - -namespace storm { - -namespace utility { - -/*! - * Prints a separating line to the standard output. - */ -void printSeparationLine(std::ostream& out); - -} //namespace utility - -} //namespace storm - -#endif /* STORM_UTILITY_COMMANDLINE_H_ */ diff --git a/src/utility/Vector.h b/src/utility/Vector.h deleted file mode 100644 index b3748d9ea..000000000 --- a/src/utility/Vector.h +++ /dev/null @@ -1,212 +0,0 @@ -/* - * Vector.h - * - * Created on: 06.12.2012 - * Author: Christian Dehnert - */ - -#ifndef STORM_UTILITY_VECTOR_H_ -#define STORM_UTILITY_VECTOR_H_ - -#include "Eigen/Core" -#include "ConstTemplates.h" -#include - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -extern log4cplus::Logger logger; - -namespace storm { - -namespace utility { - -template -void setVectorValues(std::vector* vector, const storm::storage::BitVector& positions, std::vector const& values) { - uint_fast64_t oldPosition = 0; - for (auto position : positions) { - (*vector)[position] = values[oldPosition++]; - } -} - -template -void setVectorValues(std::vector* vector, const storm::storage::BitVector& positions, T value) { - for (auto position : positions) { - (*vector)[position] = value; - } -} - -template -void setVectorValues(Eigen::Matrix* eigenVector, const storm::storage::BitVector& positions, T value) { - for (auto position : positions) { - (*eigenVector)(position, 0) = value; - } -} - -template -void selectVectorValues(std::vector* vector, const storm::storage::BitVector& positions, std::vector const& values) { - uint_fast64_t oldPosition = 0; - for (auto position : positions) { - (*vector)[oldPosition++] = values[position]; - } -} - -template -void selectVectorValues(std::vector* vector, const storm::storage::BitVector& positions, const std::vector& rowMapping, std::vector const& values) { - uint_fast64_t oldPosition = 0; - for (auto position : positions) { - for (uint_fast64_t i = rowMapping[position]; i < rowMapping[position + 1]; ++i) { - (*vector)[oldPosition++] = values[i]; - } - } -} - -template -void selectVectorValuesRepeatedly(std::vector* vector, const storm::storage::BitVector& positions, const std::vector& rowMapping, std::vector const& values) { - uint_fast64_t oldPosition = 0; - for (auto position : positions) { - for (uint_fast64_t i = rowMapping[position]; i < rowMapping[position + 1]; ++i) { - (*vector)[oldPosition++] = values[position]; - } - } -} - -template -void subtractFromConstantOneVector(std::vector* vector) { - for (auto it = vector->begin(); it != vector->end(); ++it) { - *it = storm::utility::constGetOne() - *it; - } -} - -template -void addVectors(std::vector& target, std::vector const& summand) { - if (target.size() != target.size()) { - LOG4CPLUS_ERROR(logger, "Lengths of vectors does not match and makes operation impossible."); - throw storm::exceptions::InvalidArgumentException() << "Length of vectors does not match and makes operation impossible."; - } - - for (uint_fast64_t i = 0; i < target.size(); ++i) { - target[i] += summand[i]; - } -} - -template -void addVectors(std::vector const& states, std::vector const& nondeterministicChoiceIndices, std::vector& original, std::vector const& summand) { - for (auto stateIt = states.cbegin(), stateIte = states.cend(); stateIt != stateIte; ++stateIt) { - for (auto rowIt = nondeterministicChoiceIndices[*stateIt], rowIte = nondeterministicChoiceIndices[*stateIt + 1]; rowIt != rowIte; ++rowIt) { - original[rowIt] += summand[rowIt]; - } - } -} - -template -void reduceVectorMin(std::vector const& source, std::vector* target, std::vector const& filter) { - uint_fast64_t currentSourceRow = 0; - uint_fast64_t currentTargetRow = -1; - for (auto it = source.cbegin(); it != source.cend(); ++it, ++currentSourceRow) { - // Check whether we have considered all source rows for the current target row. - if (filter[currentTargetRow + 1] <= currentSourceRow || currentSourceRow == 0) { - ++currentTargetRow; - (*target)[currentTargetRow] = source[currentSourceRow]; - continue; - } - - // We have to minimize the value, so only overwrite the current value if the - // value is actually lower. - if (*it < (*target)[currentTargetRow]) { - (*target)[currentTargetRow] = *it; - } - } -} - -template -void reduceVectorMin(std::vector const& source, std::vector* target, std::vector const& scc, std::vector const& filter) { - for (auto stateIt = scc.cbegin(); stateIt != scc.cend(); ++stateIt) { - (*target)[*stateIt] = source[filter[*stateIt]]; - - for (auto row = filter[*stateIt] + 1; row < filter[*stateIt + 1]; ++row) { - // We have to minimize the value, so only overwrite the current value if the - // value is actually lower. - if (source[row] < (*target)[*stateIt]) { - (*target)[*stateIt] = source[row]; - } - } - } -} - -template -void reduceVectorMax(std::vector const& source, std::vector* target, std::vector const& filter) { - uint_fast64_t currentSourceRow = 0; - uint_fast64_t currentTargetRow = -1; - for (auto it = source.cbegin(); it != source.cend(); ++it, ++currentSourceRow) { - // Check whether we have considered all source rows for the current target row. - if (filter[currentTargetRow + 1] <= currentSourceRow || currentSourceRow == 0) { - ++currentTargetRow; - (*target)[currentTargetRow] = source[currentSourceRow]; - continue; - } - - // We have to maximize the value, so only overwrite the current value if the - // value is actually greater. - if (*it > (*target)[currentTargetRow]) { - (*target)[currentTargetRow] = *it; - } - } -} - -template -void reduceVectorMax(std::vector const& source, std::vector* target, std::vector const& scc, std::vector const& filter) { - for (auto stateIt = scc.cbegin(); stateIt != scc.cend(); ++stateIt) { - (*target)[*stateIt] = source[filter[*stateIt]]; - - for (auto row = filter[*stateIt] + 1; row < filter[*stateIt + 1]; ++row) { - // We have to maximize the value, so only overwrite the current value if the - // value is actually lower. - if (source[row] > (*target)[*stateIt]) { - (*target)[*stateIt] = source[row]; - } - } - } -} - -template -bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T precision, bool relativeError) { - if (vectorLeft.size() != vectorRight.size()) { - LOG4CPLUS_ERROR(logger, "Lengths of vectors does not match and makes comparison impossible."); - throw storm::exceptions::InvalidArgumentException() << "Length of vectors does not match and makes comparison impossible."; - } - - for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) { - if (relativeError) { - if (std::abs(vectorLeft[i] - vectorRight[i])/vectorRight[i] > precision) return false; - } else { - if (std::abs(vectorLeft[i] - vectorRight[i]) > precision) return false; - } - } - - return true; -} - -template -bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector const& scc, T precision, bool relativeError) { - if (vectorLeft.size() != vectorRight.size()) { - LOG4CPLUS_ERROR(logger, "Lengths of vectors does not match and makes comparison impossible."); - throw storm::exceptions::InvalidArgumentException() << "Length of vectors does not match and makes comparison impossible."; - } - - for (uint_fast64_t state : scc) { - if (relativeError) { - if (std::abs(vectorLeft[state] - vectorRight[state])/vectorRight[state] > precision) return false; - } else { - if (std::abs(vectorLeft[state] - vectorRight[state]) > precision) return false; - } - } - - return true; -} - -} //namespace utility - -} //namespace storm - -#endif /* STORM_UTILITY_VECTOR_H_ */ diff --git a/src/utility/graph.h b/src/utility/graph.h index d3494877d..8d9f0f024 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -1,5 +1,5 @@ /* - * GraphAnalyzer.h + * graph.h * * Created on: 28.11.2012 * Author: Christian Dehnert @@ -31,10 +31,12 @@ namespace graph { * @param model The model whose graph structure to search. * @param phiStates A bit vector of all states satisfying phi. * @param psiStates A bit vector of all states satisfying psi. + * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. + * @param maximalSteps The maximal number of steps to reach the psi states. * @return A bit vector with all indices of states that have a probability greater than 0. */ template - storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { // Prepare the resulting bit vector. storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); @@ -48,16 +50,43 @@ namespace graph { std::vector stack; stack.reserve(model.getNumberOfStates()); psiStates.addSetIndicesToVector(stack); + + // Initialize the stack for the step bound, if the number of steps is bounded. + std::vector stepStack; + std::vector remainingSteps; + if (useStepBound) { + stepStack.reserve(model.getNumberOfStates()); + stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps); + remainingSteps.resize(model.getNumberOfStates()); + for (auto state : psiStates) { + remainingSteps[state] = maximalSteps; + } + } // Perform the actual BFS. - while(!stack.empty()) { - uint_fast64_t currentState = stack.back(); + uint_fast64_t currentState, currentStepBound; + while (!stack.empty()) { + currentState = stack.back(); stack.pop_back(); + + if (useStepBound) { + currentStepBound = stepStack.back(); + stepStack.pop_back(); + } - for(auto it = backwardTransitions.constColumnIteratorBegin(currentState); it != backwardTransitions.constColumnIteratorEnd(currentState); ++it) { - if (phiStates.get(*it) && !statesWithProbabilityGreater0.get(*it)) { - statesWithProbabilityGreater0.set(*it, true); - stack.push_back(*it); + for (auto it = backwardTransitions.constColumnIteratorBegin(currentState); it != backwardTransitions.constColumnIteratorEnd(currentState); ++it) { + if (phiStates.get(*it) && (!statesWithProbabilityGreater0.get(*it) || (useStepBound && remainingSteps[*it] < currentStepBound - 1))) { + // If we don't have a number of maximal steps to take, just add the state to the stack. + if (!useStepBound) { + statesWithProbabilityGreater0.set(*it, true); + stack.push_back(*it); + } else if (currentStepBound > 0) { + // If there is at least one more step to go, we need to push the state and the new number of steps. + remainingSteps[*it] = currentStepBound - 1; + statesWithProbabilityGreater0.set(*it, true); + stack.push_back(*it); + stepStack.push_back(currentStepBound - 1); + } } } } @@ -127,45 +156,97 @@ namespace graph { } /*! - * Computes the sets of states that have probability 0 of satisfying phi until psi under all - * possible resolutions of non-determinism in a non-deterministic model. Stated differently, - * this means that these states have probability 0 of satisfying phi until psi even if the - * scheduler tries to maximize this probability. + * Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least + * one possible resolution of non-determinism in a non-deterministic model. Stated differently, + * this means that these states have a probability greater 0 of satisfying phi until psi if the + * scheduler tries to minimize this probability. * * @param model The model whose graph structure to search. * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. + * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. + * @param maximalSteps The maximal number of steps to reach the psi states. * @return A bit vector that represents all states with probability 0. */ template - storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - // Prepare the resulting bit vector. - storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); - + storm::storage::BitVector performProbGreater0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { + // Prepare resulting bit vector. + storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); + + // Get some temporaries for convenience. + std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); + std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + // Add all psi states as the already satisfy the condition. - statesWithProbability0 |= psiStates; - + statesWithProbabilityGreater0 |= psiStates; + // Initialize the stack used for the BFS with the states std::vector stack; stack.reserve(model.getNumberOfStates()); psiStates.addSetIndicesToVector(stack); - + + // Initialize the stack for the step bound, if the number of steps is bounded. + std::vector stepStack; + std::vector remainingSteps; + if (useStepBound) { + stepStack.reserve(model.getNumberOfStates()); + stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps); + remainingSteps.resize(model.getNumberOfStates()); + for (auto state : psiStates) { + remainingSteps[state] = maximalSteps; + } + } + // Perform the actual BFS. - while(!stack.empty()) { - uint_fast64_t currentState = stack.back(); + uint_fast64_t currentState, currentStepBound; + while (!stack.empty()) { + currentState = stack.back(); stack.pop_back(); - - for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { - if (phiStates.get(*it) && !statesWithProbability0.get(*it)) { - statesWithProbability0.set(*it, true); - stack.push_back(*it); - } + + if (useStepBound) { + currentStepBound = stepStack.back(); + stepStack.pop_back(); + } + + for (auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { + if (phiStates.get(*it) && (!statesWithProbabilityGreater0.get(*it) || (useStepBound && remainingSteps[*it] < currentStepBound - 1))) { + // If we don't have a bound on the number of steps to take, just add the state to the stack. + if (!useStepBound) { + statesWithProbabilityGreater0.set(*it, true); + stack.push_back(*it); + } else if (currentStepBound > 0) { + // If there is at least one more step to go, we need to push the state and the new number of steps. + remainingSteps[*it] = currentStepBound - 1; + statesWithProbabilityGreater0.set(*it, true); + stack.push_back(*it); + stepStack.push_back(currentStepBound - 1); + } + } } } - - // Finally, invert the computed set of states and return result. - statesWithProbability0.complement(); + + return statesWithProbabilityGreater0; + } + + /*! + * Computes the sets of states that have probability 0 of satisfying phi until psi under all + * possible resolutions of non-determinism in a non-deterministic model. Stated differently, + * this means that these states have probability 0 of satisfying phi until psi even if the + * scheduler tries to maximize this probability. + * + * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. + * @param maximalSteps The maximal number of steps to reach the psi states. + * @return A bit vector that represents all states with probability 0. + */ + template + storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector statesWithProbability0 = performProbGreater0E(model, backwardTransitions, phiStates, psiStates); + statesWithProbability0.complement(); return statesWithProbability0; } @@ -194,13 +275,14 @@ namespace graph { // Perform the loop as long as the set of states gets larger. bool done = false; + uint_fast64_t currentState; while (!done) { stack.clear(); storm::storage::BitVector nextStates(psiStates); psiStates.addSetIndicesToVector(stack); while (!stack.empty()) { - uint_fast64_t currentState = stack.back(); + currentState = stack.back(); stack.pop_back(); for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { @@ -263,69 +345,116 @@ namespace graph { } /*! - * Computes the sets of states that have probability 0 of satisfying phi until psi under at least - * one possible resolution of non-determinism in a non-deterministic model. Stated differently, - * this means that these states have probability 0 of satisfying phi until psi if the - * scheduler tries to minimize this probability. + * Computes the sets of states that have probability greater 0 of satisfying phi until psi under any + * possible resolution of non-determinism in a non-deterministic model. Stated differently, + * this means that these states have a probability greater 0 of satisfying phi until psi if the + * scheduler tries to maximize this probability. * * @param model The model whose graph structure to search. * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. + * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. + * @param maximalSteps The maximal number of steps to reach the psi states. * @return A bit vector that represents all states with probability 0. */ template - storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProbGreater0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { // Prepare resulting bit vector. - storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); + storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - + // Add all psi states as the already satisfy the condition. - statesWithProbability0 |= psiStates; - - // Initialize the stack used for the DFS with the states + statesWithProbabilityGreater0 |= psiStates; + + // Initialize the stack used for the BFS with the states std::vector stack; stack.reserve(model.getNumberOfStates()); psiStates.addSetIndicesToVector(stack); - - // Perform the actual DFS. + + // Initialize the stack for the step bound, if the number of steps is bounded. + std::vector stepStack; + std::vector remainingSteps; + if (useStepBound) { + stepStack.reserve(model.getNumberOfStates()); + stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps); + remainingSteps.resize(model.getNumberOfStates()); + for (auto state : psiStates) { + remainingSteps[state] = maximalSteps; + } + } + + // Perform the actual BFS. + uint_fast64_t currentState, currentStepBound; while(!stack.empty()) { - uint_fast64_t currentState = stack.back(); + currentState = stack.back(); stack.pop_back(); - + + if (useStepBound) { + currentStepBound = stepStack.back(); + stepStack.pop_back(); + } + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { - if (phiStates.get(*it) && !statesWithProbability0.get(*it)) { - // Check whether the predecessor has at least one successor in the current state - // set for every nondeterministic choice. - bool addToStatesWithProbability0 = true; - for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) { - bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; - for (auto colIt = transitionMatrix->constColumnIteratorBegin(*rowIt); colIt != transitionMatrix->constColumnIteratorEnd(*rowIt); ++colIt) { - if (statesWithProbability0.get(*colIt)) { - hasAtLeastOneSuccessorWithProbabilityGreater0 = true; - break; - } - } - if (!hasAtLeastOneSuccessorWithProbabilityGreater0) { - addToStatesWithProbability0 = false; - break; - } - } - - // If we need to add the state, then actually add it and perform further search - // from the state. - if (addToStatesWithProbability0) { - statesWithProbability0.set(*it, true); - stack.push_back(*it); - } - } + if (phiStates.get(*it) && (!statesWithProbabilityGreater0.get(*it) || (useStepBound && remainingSteps[*it] < currentStepBound - 1))) { + // Check whether the predecessor has at least one successor in the current state set for every + // nondeterministic choice. + bool addToStatesWithProbabilityGreater0 = true; + for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) { + bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; + for (auto colIt = transitionMatrix->constColumnIteratorBegin(*rowIt); colIt != transitionMatrix->constColumnIteratorEnd(*rowIt); ++colIt) { + if (statesWithProbabilityGreater0.get(*colIt)) { + hasAtLeastOneSuccessorWithProbabilityGreater0 = true; + break; + } + } + + if (!hasAtLeastOneSuccessorWithProbabilityGreater0) { + addToStatesWithProbabilityGreater0 = false; + break; + } + } + + // If we need to add the state, then actually add it and perform further search from the state. + if (addToStatesWithProbabilityGreater0) { + // If we don't have a bound on the number of steps to take, just add the state to the stack. + if (!useStepBound) { + statesWithProbabilityGreater0.set(*it, true); + stack.push_back(*it); + } else if (currentStepBound > 0) { + // If there is at least one more step to go, we need to push the state and the new number of steps. + remainingSteps[*it] = currentStepBound - 1; + statesWithProbabilityGreater0.set(*it, true); + stack.push_back(*it); + stepStack.push_back(currentStepBound - 1); + } + } + } } } - - statesWithProbability0.complement(); + + return statesWithProbabilityGreater0; + } + + /*! + * Computes the sets of states that have probability 0 of satisfying phi until psi under at least + * one possible resolution of non-determinism in a non-deterministic model. Stated differently, + * this means that these states have probability 0 of satisfying phi until psi if the + * scheduler tries to minimize this probability. + * + * @param model The model whose graph structure to search. + * @param backwardTransitions The reversed transition relation of the model. + * @param phiStates The set of all states satisfying phi. + * @param psiStates The set of all states satisfying psi. + * @return A bit vector that represents all states with probability 0. + */ + template + storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector statesWithProbability0 = performProbGreater0A(model, backwardTransitions, phiStates, psiStates); + statesWithProbability0.complement(); return statesWithProbability0; } @@ -347,20 +476,21 @@ namespace graph { std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + // Initialize the environment for the iterative algorithm. storm::storage::BitVector currentStates(model.getNumberOfStates(), true); - std::vector stack; stack.reserve(model.getNumberOfStates()); // Perform the loop as long as the set of states gets smaller. bool done = false; + uint_fast64_t currentState; while (!done) { stack.clear(); storm::storage::BitVector nextStates(psiStates); psiStates.addSetIndicesToVector(stack); while (!stack.empty()) { - uint_fast64_t currentState = stack.back(); + currentState = stack.back(); stack.pop_back(); for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { diff --git a/src/utility/vector.h b/src/utility/vector.h new file mode 100644 index 000000000..fff25fd52 --- /dev/null +++ b/src/utility/vector.h @@ -0,0 +1,281 @@ +/* + * vector.h + * + * Created on: 06.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_UTILITY_VECTOR_H_ +#define STORM_UTILITY_VECTOR_H_ + +#include "Eigen/Core" +#include "ConstTemplates.h" +#include +#include +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +namespace storm { + +namespace utility { + +namespace vector { + +/*! + * Sets the provided values at the provided positions in the given vector. + * + * @param vector The vector in which the values are to be set. + * @param positions The positions at which the values are to be set. + * @param values The values that are to be set. + */ +template +void setVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + vector[position] = values[oldPosition++]; + } +} + +/*! + * Sets the provided value at the provided positions in the given vector. + * + * @param vector The vector in which the value is to be set. + * @param positions The positions at which the value is to be set. + * @param value The value that is to be set. + */ +template +void setVectorValues(std::vector& vector, storm::storage::BitVector const& positions, T value) { + for (auto position : positions) { + vector[position] = value; + } +} + +/*! + * Sets the provided value at the provided positions in the given vector. + * + * @param vector The vector in which the value is to be set. + * @param positions The positions at which the value is to be set. + * @param value The value that is to be set. + */ +template +void setVectorValues(Eigen::Matrix& eigenVector, storm::storage::BitVector const& positions, T value) { + for (auto position : positions) { + eigenVector(position, 0) = value; + } +} + +/*! + * Selects the elements from a vector at the specified positions and writes them consecutively into another vector. + * @param vector The vector into which the selected elements are to be written. + * @param positions The positions at which to select the elements from the values vector. + * @param values The vector from which to select the elements. + */ +template +void selectVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + vector[oldPosition++] = values[position]; + } +} + +/*! + * Selects groups of elements from a vector at the specified positions and writes them consecutively into another vector. + * + * @param vector The vector into which the selected elements are to be written. + * @param positions The positions of the groups of elements that are to be selected. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. + * @param values The vector from which to select groups of elements. + */ +template +void selectVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& rowGrouping, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) { + vector[oldPosition++] = values[i]; + } + } +} + +/*! + * Selects values from a vector at the specified positions and writes them into another vector as often as given by + * the size of the corresponding group of elements. + * + * @param vector The vector into which the selected elements are written. + * @param positions The positions at which to select the values. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. This + * implicitly defines the number of times any element is written to the output vector. + */ +template +void selectVectorValuesRepeatedly(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& rowGrouping, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) { + vector[oldPosition++] = values[position]; + } + } +} + +/*! + * Subtracts the given vector from the constant one-vector and writes the result to the input vector. + * + * @param vector The vector that is to be subtracted from the constant one-vector. + */ +template +void subtractFromConstantOneVector(std::vector& vector) { + for (auto element : vector) { + element = storm::utility::constGetOne() - element; + } +} + +/*! + * Adds the two given vectors and writes the result into the first operand. + * + * @param target The first summand and target vector. + * @param summand The second summand. + */ +template +void addVectorsInPlace(std::vector& target, std::vector const& summand) { + if (target.size() != summand.size()) { + LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes operation impossible."); + throw storm::exceptions::InvalidArgumentException() << "Length of vectors do not match, which makes operation impossible."; + } + + std::transform(target.begin(), target.end(), summand.begin(), target.begin(), std::plus()); +} + +/*! + * Reduces the given source vector by selecting an element according to the given filter out of each row group. + * + * @param source The source vector which is to be reduced. + * @param target The target vector into which a single element from each row group is written. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. + * @param filter A function that compares two elements v1 and v2 according to some filter criterion. This function must + * return true iff v1 is supposed to be taken instead of v2. + */ +template +void reduceVector(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::function filter) { + uint_fast64_t currentSourceRow = 0; + uint_fast64_t currentTargetRow = -1; + for (auto it = source.cbegin(), ite = source.cend(); it != ite; ++it, ++currentSourceRow) { + // Check whether we have considered all source rows for the current target row. + if (rowGrouping[currentTargetRow + 1] <= currentSourceRow || currentSourceRow == 0) { + ++currentTargetRow; + target[currentTargetRow] = source[currentSourceRow]; + continue; + } + + // We have to minimize the value, so only overwrite the current value if the + // value is actually lower. + if (filter(*it, target[currentTargetRow])) { + target[currentTargetRow] = *it; + } + } +} + +/*! + * Reduces the given source vector by selecting the smallest element out of each row group. + * + * @param source The source vector which is to be reduced. + * @param target The target vector into which a single element from each row group is written. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. + */ +template +void reduceVectorMin(std::vector const& source, std::vector& target, std::vector const& rowGrouping) { + reduceVector(source, target, rowGrouping, std::less()); +} + +/*! + * Reduces the given source vector by selecting the largest element out of each row group. + * + * @param source The source vector which is to be reduced. + * @param target The target vector into which a single element from each row group is written. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. + */ +template +void reduceVectorMax(std::vector const& source, std::vector& target, std::vector const& rowGrouping) { + reduceVector(source, target, rowGrouping, std::greater()); +} + +/*! + * Compares the given elements and determines whether they are equal modulo the given precision. The provided flag + * additionaly specifies whether the error is computed in relative or absolute terms. + * + * @param val1 The first value to compare. + * @param val2 The second value to compare. + * @param precision The precision up to which the elements are compared. + * @param relativeError If set, the error is computed relative to the second value. + * @return True iff the elements are considered equal. + */ +template +bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) { + if (relativeError) { + if (std::abs(val1 - val2)/val2 > precision) return false; + } else { + if (std::abs(val1 - val2) > precision) return false; + } + return true; +} + +/*! + * Compares the two vectors and determines whether they are equal modulo the provided precision. Depending on whether the + * flag is set, the difference between the vectors is computed relative to the value or in absolute terms. + * + * @param vectorLeft The first vector of the comparison. + * @param vectorRight The second vector of the comparison. + * @param precision The precision up to which the vectors are to be checked for equality. + * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. + */ +template +bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T precision, bool relativeError) { + if (vectorLeft.size() != vectorRight.size()) { + LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible."); + throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible."; + } + + for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) { + if (!equalModuloPrecision(vectorLeft[i], vectorRight[i], precision, relativeError)) { + return false; + } + } + + return true; +} + +/*! + * Compares the two vectors at the specified positions and determines whether they are equal modulo the provided + * precision. Depending on whether the flag is set, the difference between the vectors is computed relative to the value + * or in absolute terms. + * + * @param vectorLeft The first vector of the comparison. + * @param vectorRight The second vector of the comparison. + * @param precision The precision up to which the vectors are to be checked for equality. + * @param positions A vector representing a set of positions at which the vectors are compared. + * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. + */ +template +bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector const& positions, T precision, bool relativeError) { + if (vectorLeft.size() != vectorRight.size()) { + LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible."); + throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible."; + } + + for (uint_fast64_t position : positions) { + if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) { + return false; + } + } + + return true; +} + +} // namespace vector + +} // namespace utility + +} // namespace storm + +#endif /* STORM_UTILITY_VECTOR_H_ */ diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index ca13fb561..5944f02e3 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -209,7 +209,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); result = mc.checkNoBoundOperator(*probFormula); @@ -218,11 +218,11 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); delete probFormula; - delete result; + delete result; apFormula = new storm::property::prctl::Ap("elected"); boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); result = mc.checkNoBoundOperator(*probFormula); diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 4696ad8e5..5f56136b3 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -93,7 +93,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { ASSERT_EQ(sccDecomposition.size(), 1290297u); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of crowds/crowds20_5..."); - storm::storage::SparseMatrix sccDependencyGraph = dtmc->extractSccDependencyGraph(sccDecomposition); + storm::storage::SparseMatrix sccDependencyGraph = dtmc->extractPartitionDependencyGraph(sccDecomposition); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1371253u); @@ -110,7 +110,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { ASSERT_EQ(sccDecomposition.size(), 1279673u); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of synchronous_leader/leader6_8..."); - sccDependencyGraph = dtmc2->extractSccDependencyGraph(sccDecomposition); + sccDependencyGraph = dtmc2->extractPartitionDependencyGraph(sccDecomposition); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1535367u); @@ -127,7 +127,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { ASSERT_EQ(sccDecomposition.size(), 214675); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6..."); - sccDependencyGraph = mdp->extractSccDependencyGraph(sccDecomposition); + sccDependencyGraph = mdp->extractPartitionDependencyGraph(sccDecomposition); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 684093u); @@ -144,7 +144,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { ASSERT_EQ(sccDecomposition.size(), 63611u); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6..."); - sccDependencyGraph = mdp2->extractSccDependencyGraph(sccDecomposition); + sccDependencyGraph = mdp2->extractPartitionDependencyGraph(sccDecomposition); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 213400u);