From a04bdd9b970e51bd28e1b31330199a77dfdddd8a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 22 Dec 2012 19:41:01 +0100 Subject: [PATCH 1/3] Fixed a few bugs. --- src/modelChecker/EigenDtmcPrctlModelChecker.h | 2 +- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 10 ++++++++-- src/storage/SquareSparseMatrix.h | 2 +- 3 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h index 9a1760292..f17f87def 100644 --- a/src/modelChecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h @@ -51,7 +51,7 @@ public: mrmc::storage::SquareSparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. - tmpMatrix.makeRowsAbsorbing((~*leftStates & *rightStates) | *rightStates); + tmpMatrix.makeRowsAbsorbing((~*leftStates | *rightStates) | *rightStates); // Transform the transition probability matrix to the eigen format to use its arithmetic. Eigen::SparseMatrix* eigenMatrix = tmpMatrix.toEigenSparseMatrix(); diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index cd693da78..83036e3bf 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -49,7 +49,7 @@ public: mrmc::storage::SquareSparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. - tmpMatrix.makeRowsAbsorbing(~(*leftStates & *rightStates) | *rightStates); + tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. gmm::csr_matrix* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix(); @@ -59,9 +59,15 @@ public: mrmc::utility::setVectorValues(result, *rightStates, static_cast(1.0)); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. + std::vector* swap = nullptr; + std::vector* tmpResult = new std::vector(this->getModel().getNumberOfStates()); for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { - gmm::mult(*gmmxxMatrix, *result, *result); + gmm::mult(*gmmxxMatrix, *result, *tmpResult); + swap = tmpResult; + tmpResult = result; + result = swap; } + delete tmpResult; // Delete intermediate results and return result. delete leftStates; diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index cbb56f196..b14e31dd2 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -76,7 +76,7 @@ public: internalStatus(ssm.internalStatus), currentSize(ssm.currentSize), lastRow(ssm.lastRow) { LOG4CPLUS_WARN(logger, "Invoking copy constructor."); // Check whether copying the matrix is safe. - if (!ssm.hasError()) { + if (ssm.hasError()) { LOG4CPLUS_ERROR(logger, "Trying to copy sparse matrix in error state."); throw mrmc::exceptions::InvalidArgumentException("Trying to copy sparse matrix in error state."); } else { From b26a73138384618ed6d38dbd7cf9c43e06ef8d15 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 23 Dec 2012 14:45:01 +0100 Subject: [PATCH 2/3] Added reward parsing: * Transition-based rewards are parsed using the existing (Deterministic)SparseTransitionsParser. * State-based rewards are parsed using a new SparseStateRewardParser that parses lines consisting of a state and an associated reward. * The Dtmc class now stores the two reward models. * The DtmcParser class now parses up to one transition-based and one state-based reward file. They may, however, be omitted in which case the respective reward model is set to null. --- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 10 ++--- src/models/Dtmc.h | 38 ++++++++++++++++--- src/parser/DtmcParser.cpp | 24 ++++++++++-- src/parser/DtmcParser.h | 3 +- src/utility/Settings.cpp | 2 + 5 files changed, 62 insertions(+), 15 deletions(-) diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 83036e3bf..454af57f2 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -14,7 +14,7 @@ #include "src/modelChecker/DtmcPrctlModelChecker.h" #include "src/solver/GraphAnalyzer.h" #include "src/utility/Vector.h" - +#include "src/utility/ConstTemplates.h" #include "src/utility/Settings.h" #include "gmm/gmm_matrix.h" @@ -56,7 +56,7 @@ public: // Create the vector with which to multiply. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - mrmc::utility::setVectorValues(result, *rightStates, static_cast(1.0)); + mrmc::utility::setVectorValues(result, *rightStates, mrmc::utility::constGetOne()); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. std::vector* swap = nullptr; @@ -84,7 +84,7 @@ public: // Create the vector with which to multiply and initialize it correctly. std::vector x(this->getModel().getNumberOfStates()); - mrmc::utility::setVectorValues(&x, *nextStates, static_cast(1.0)); + mrmc::utility::setVectorValues(&x, *nextStates, mrmc::utility::constGetOne()); // Delete obsolete sub-result. delete nextStates; @@ -221,8 +221,8 @@ public: } // Set values of resulting vector that are known exactly. - mrmc::utility::setVectorValues(result, notExistsPhiUntilPsiStates, static_cast(0)); - mrmc::utility::setVectorValues(result, alwaysPhiUntilPsiStates, static_cast(1.0)); + mrmc::utility::setVectorValues(result, notExistsPhiUntilPsiStates, mrmc::utility::constGetZero()); + mrmc::utility::setVectorValues(result, alwaysPhiUntilPsiStates, mrmc::utility::constGetOne()); return result; } diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index c024779ba..35b129991 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -39,9 +39,14 @@ public: * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Dtmc(std::shared_ptr> probabilityMatrix, std::shared_ptr stateLabeling) - : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), backwardTransitions(nullptr) { - if (! this->checkValidityProbabilityMatrix()) { + Dtmc(std::shared_ptr> probabilityMatrix, + std::shared_ptr stateLabeling, + std::shared_ptr> stateRewards = nullptr, + std::shared_ptr> transitionRewardMatrix = nullptr) + : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), + stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), + backwardTransitions(nullptr) { + if (!this->checkValidityProbabilityMatrix()) { std::cerr << "Probability matrix is invalid" << std::endl; } } @@ -52,11 +57,12 @@ public: * @param dtmc A reference to the DTMC that is to be copied. */ Dtmc(const Dtmc &dtmc) : probabilityMatrix(dtmc.probabilityMatrix), - stateLabeling(dtmc.stateLabeling) { + stateLabeling(dtmc.stateLabeling), stateRewards(dtmc.stateRewards), + transitionRewardMatrix(dtmc.transitionRewardMatrix) { if (dtmc.backardTransitions != nullptr) { this->backwardTransitions = new mrmc::models::GraphTransitions(*dtmc.backwardTransitions); } - if (! this->checkValidityProbabilityMatrix()) { + if (!this->checkValidityProbabilityMatrix()) { std::cerr << "Probability matrix is invalid" << std::endl; } } @@ -108,6 +114,22 @@ public: return this->probabilityMatrix; } + /*! + * Returns a pointer to the matrix representing the transition rewards. + * @return A pointer to the matrix representing the transition rewards. + */ + std::shared_ptr> getTransitionRewardMatrix() const { + return this->transitionRewardMatrix; + } + + /*! + * Returns a pointer to the vector representing the state rewards. + * @return A pointer to the vector representing the state rewards. + */ + std::shared_ptr> getStateRewards() const { + return this->stateRewards; + } + /*! * */ @@ -170,6 +192,12 @@ private: /*! The labeling of the states of the DTMC. */ std::shared_ptr stateLabeling; + /*! The state-based rewards of the DTMC. */ + std::shared_ptr> stateRewards; + + /*! The transition-based rewards of the DTMC. */ + std::shared_ptr> transitionRewardMatrix; + /*! * A data structure that stores the predecessors for all states. This is * needed for backwards directed searches. diff --git a/src/parser/DtmcParser.cpp b/src/parser/DtmcParser.cpp index 67dc0ac76..edeab198d 100644 --- a/src/parser/DtmcParser.cpp +++ b/src/parser/DtmcParser.cpp @@ -8,6 +8,7 @@ #include "DtmcParser.h" #include "DeterministicSparseTransitionParser.h" #include "AtomicPropositionLabelingParser.h" +#include "SparseStateRewardParser.h" namespace mrmc { namespace parser { @@ -19,15 +20,30 @@ namespace parser { * * @param transitionSystemFile String containing the location of the transition file (....tra) * @param labelingFile String containing the location of the labeling file (....lab) + * @param stateRewardFile String containing the location of the state reward file (...srew) + * @param transitionRewardFile String containing the location of the transition reward file (...trew) */ -DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile) { +DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile, std::string const & transitionRewardFile) { mrmc::parser::DeterministicSparseTransitionParser tp(transitionSystemFile); - uint_fast64_t nodeCount = tp.getMatrix()->getRowCount(); + uint_fast64_t stateCount = tp.getMatrix()->getRowCount(); - mrmc::parser::AtomicPropositionLabelingParser lp(nodeCount, labelingFile); + std::shared_ptr> stateRewards = nullptr; + std::shared_ptr> transitionRewards = nullptr; - dtmc = std::shared_ptr >(new mrmc::models::Dtmc(tp.getMatrix(), lp.getLabeling())); + mrmc::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); + if (stateRewardFile != "") { + mrmc::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); + stateRewards = srp.getStateRewards(); + } + if (transitionRewardFile != "") { + mrmc::parser::DeterministicSparseTransitionParser trp(transitionRewardFile); + transitionRewards = trp.getMatrix(); + } + + dtmc = std::shared_ptr>(new mrmc::models::Dtmc(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); } } /* namespace parser */ + } /* namespace mrmc */ diff --git a/src/parser/DtmcParser.h b/src/parser/DtmcParser.h index 7db859098..844617e91 100644 --- a/src/parser/DtmcParser.h +++ b/src/parser/DtmcParser.h @@ -24,7 +24,8 @@ namespace parser { */ class DtmcParser: public mrmc::parser::Parser { public: - DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile); + DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); std::shared_ptr> getDtmc() { return this->dtmc; diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 063fc0e33..0e2978a28 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -130,6 +130,8 @@ void Settings::initDescriptions() { ("test-prctl", bpo::value(), "name of prctl file") ("trafile", bpo::value()->required(), "name of the .tra file") ("labfile", bpo::value()->required(), "name of the .lab file") + ("transrew", bpo::value()->default_value(""), "name of transition reward file") + ("staterew", bpo::value()->default_value(""), "name of state reward file") ; } From 504bcb97a6135263615af6ce25cbaa7cfa8cc7ce Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 23 Dec 2012 14:53:12 +0100 Subject: [PATCH 3/3] Added die example from PRISM. Added SparseStateRewardParser. Small fix to main. --- src/mrmc.cpp | 2 +- src/parser/SparseStateRewardParser.cpp | 74 ++++++++++++++++++++++++++ src/parser/SparseStateRewardParser.h | 32 +++++++++++ 3 files changed, 107 insertions(+), 1 deletion(-) create mode 100644 src/parser/SparseStateRewardParser.cpp create mode 100644 src/parser/SparseStateRewardParser.h diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 4a30f12c3..16f4cf9f4 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -100,7 +100,7 @@ bool parseOptions(const int argc, const char* argv[]) { std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; std::cout << std::endl << mrmc::settings::help; delete s; - return 1; + return false; } if (s->isSet("help")) { diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp new file mode 100644 index 000000000..4caee50e1 --- /dev/null +++ b/src/parser/SparseStateRewardParser.cpp @@ -0,0 +1,74 @@ +/*! + * SparseStateRewardParser.cpp + * + * Created on: 23.12.2012 + * Author: Christian Dehnert + */ + +#include "src/parser/SparseStateRewardParser.h" +#include "src/exceptions/WrongFileFormatException.h" +#include "src/exceptions/FileIoException.h" + +#include "src/utility/OsDetection.h" +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + +namespace mrmc { +namespace parser { + + +/*! + * Reads a state reward file and puts the result in a state reward vector. + * + * @param stateCount The number of states. + * @param filename The filename of the state reward file. + * @return A pointer to the created state reward vector. + */ +SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std::string const & filename) + : stateRewards(nullptr) { + // Open file. + MappedFile file(filename.c_str()); + char* buf = file.data; + + char separator[] = " \r\n\t"; + + // Create state reward vector with given state count. + this->stateRewards = std::shared_ptr>(new std::vector(stateCount)); + + { + // Now parse state reward assignments. + uint_fast64_t state; + double reward; + + // Iterate over states. + while (buf[0] != '\0') { + // Parse state number and reward value. + state = checked_strtol(buf, &buf); + reward = strtod(buf, &buf); + if (reward < 0.0) { + LOG4CPLUS_ERROR(logger, "Expected positive probability but got \"" << std::string(buf, 0, 16) << "\"."); + throw mrmc::exceptions::WrongFileFormatException() << "State reward file specifies illegal reward value."; + } + + (*this->stateRewards)[state] = reward; + + buf = trimWhitespaces(buf); + } + } +} + +} //namespace parser + +} //namespace mrmc diff --git a/src/parser/SparseStateRewardParser.h b/src/parser/SparseStateRewardParser.h new file mode 100644 index 000000000..604070759 --- /dev/null +++ b/src/parser/SparseStateRewardParser.h @@ -0,0 +1,32 @@ +#ifndef MRMC_PARSER_SPARSESTATEREWARDPARSER_H_ +#define MRMC_PARSER_SPARSESTATEREWARDPARSER_H_ + +#include "boost/integer/integer_mask.hpp" +#include "src/parser/Parser.h" +#include +#include + +namespace mrmc { + +namespace parser { + +/*! + * @brief Load state reward file and return vector of state rewards. + */ +class SparseStateRewardParser : Parser { + public: + SparseStateRewardParser(uint_fast64_t stateCount, std::string const &filename); + + std::shared_ptr> getStateRewards() { + return this->stateRewards; + } + + private: + std::shared_ptr> stateRewards; +}; + +} // namespace parser + +} // namespace mrmc + +#endif /* MRMC_PARSER_SPARSESTATEREWARDPARSER_H_ */