diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h index 845b93c4a..e5cee0782 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..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" @@ -49,19 +49,25 @@ 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(); // 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; + 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; @@ -78,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; @@ -215,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/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_ */ diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index 32b2580e6..bee88ba3f 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -81,7 +81,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 { 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") ; }