From 64b883f695292cc6d3fcda9cb5a04928d1010e83 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 30 May 2013 11:28:26 +0200 Subject: [PATCH] Some cleanup in storm.cpp. Refactored and commented the utility module for vector operations. --- src/modelchecker/GmmxxDtmcPrctlModelChecker.h | 4 +- src/modelchecker/GmmxxMdpPrctlModelChecker.h | 21 +- .../SparseDtmcPrctlModelChecker.h | 26 +- src/modelchecker/SparseMdpPrctlModelChecker.h | 43 ++- src/storm.cpp | 160 ++++------ src/utility/Vector.h | 212 ------------- src/utility/graph.h | 2 +- src/utility/vector.h | 281 ++++++++++++++++++ 8 files changed, 399 insertions(+), 350 deletions(-) delete mode 100644 src/utility/Vector.h create mode 100644 src/utility/vector.h diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index e7b24188e..1c2725fb3 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -34,7 +34,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. } @@ -277,7 +277,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/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h index d742d55ed..90526a24c 100644 --- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h @@ -52,6 +52,17 @@ public: private: + /*! + * 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 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. @@ -74,9 +85,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); } } @@ -124,13 +135,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/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h index c19cc471a..d22831618 100644 --- a/src/modelchecker/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/SparseDtmcPrctlModelChecker.h @@ -96,7 +96,7 @@ public: // Create the vector with which to multiply. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(*result, *rightStates, storm::utility::constGetOne()); // Perform the matrix vector multiplication as often as required by the formula bound. this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound()); @@ -124,7 +124,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; @@ -187,7 +187,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; } @@ -248,16 +248,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; } @@ -384,7 +384,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 @@ -392,7 +392,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 { @@ -400,19 +400,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/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h index 8849cd222..6c1694276 100644 --- a/src/modelchecker/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/SparseMdpPrctlModelChecker.h @@ -102,7 +102,7 @@ public: // Create the vector with which to multiply. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(*result, *rightStates, storm::utility::constGetOne()); this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound()); @@ -129,7 +129,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 sub-result. delete nextStates; @@ -191,7 +191,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; } @@ -255,12 +255,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; } @@ -396,36 +396,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; @@ -466,15 +465,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); } } } @@ -510,18 +509,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/storm.cpp b/src/storm.cpp index 76d0f38ca..237006a35 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -123,6 +123,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) { @@ -132,14 +133,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. @@ -180,111 +175,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::AbstractModelChecker* createPrctlModelChecker(storm::models::Dtmc& dtmc) { +storm::modelchecker::AbstractModelChecker* createPrctlModelChecker(storm::models::Dtmc const& dtmc) { + // Create the appropriate model checker. storm::settings::Settings* s = storm::settings::instance(); if (s->getString("matrixlib") == "gmm++") { return new storm::modelchecker::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::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp& mdp) { +storm::modelchecker::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp const& mdp) { + // Create the appropriate model checker. storm::settings::Settings* s = storm::settings::instance(); if (s->getString("matrixlib") == "gmm++") { return new storm::modelchecker::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::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 - */ -void checkPrctlFormulasAgainstModel(std::list*>& formulaList, - storm::modelchecker::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); - 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::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 + * @param modelchecker The model checker that is to be invoked on all given formulae. */ -void checkDtmc(std::shared_ptr> dtmc) { - dtmc->printModelInformationToStream(std::cout); +void checkPrctlFormulae(storm::modelchecker::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::AbstractModelChecker* mc = createPrctlModelChecker(*dtmc); - - checkPrctlFormulasAgainstModel(formulaList, *mc); - - delete mc; - } - - if(s->isSet("csl")) { - LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on DTMCs."); + + for (auto formula : formulaList) { + modelchecker.check(*formula); + delete formula; + } } } @@ -292,56 +253,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::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)); @@ -349,13 +320,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/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..dc8980b80 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 diff --git a/src/utility/vector.h b/src/utility/vector.h new file mode 100644 index 000000000..314084ef7 --- /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, [] (T const& val1, T const& val2) -> bool { return val1 < val2; }); +} + +/*! + * 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, [] (T const& val1, T const& val2) -> bool { return val1 > val2; }); +} + +/*! + * 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_ */