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") ; }