From 718608622fa456e83fa451aa03dc3a39b2f8e4eb Mon Sep 17 00:00:00 2001 From: gereon Date: Wed, 6 Feb 2013 22:12:29 +0100 Subject: [PATCH] added Ctmdp model, changed MdpParser to NonDetModelParser --- src/models/Ctmdp.h | 251 ++++++++++++++++++ src/parser/AutoParser.cpp | 9 +- src/parser/MdpParser.h | 40 --- ...er.cpp => NonDeterministicModelParser.cpp} | 20 +- src/parser/NonDeterministicModelParser.h | 62 +++++ test/parser/ParseMdpTest.cpp | 6 +- 6 files changed, 333 insertions(+), 55 deletions(-) create mode 100644 src/models/Ctmdp.h delete mode 100644 src/parser/MdpParser.h rename src/parser/{MdpParser.cpp => NonDeterministicModelParser.cpp} (73%) create mode 100644 src/parser/NonDeterministicModelParser.h diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h new file mode 100644 index 000000000..137095e9f --- /dev/null +++ b/src/models/Ctmdp.h @@ -0,0 +1,251 @@ +/* + * Ctmdp.h + * + * Created on: 14.01.2013 + * Author: Philipp Berger + */ + +#ifndef STORM_MODELS_CTMDP_H_ +#define STORM_MODELS_CTMDP_H_ + +#include +#include +#include +#include + +#include "AtomicPropositionsLabeling.h" +#include "GraphTransitions.h" +#include "src/storage/SparseMatrix.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/utility/CommandLine.h" +#include "src/utility/Settings.h" +#include "src/models/AbstractModel.h" +#include "src/parser/NonDeterministicSparseTransitionParser.h" + +namespace storm { + +namespace models { + +/*! + * This class represents a Markov Decision Process (CTMDP) whose states are + * labeled with atomic propositions. + */ +template +class Ctmdp : public storm::models::AbstractModel { + +public: + //! Constructor + /*! + * Constructs a CTMDP object from the given transition probability matrix and + * the given labeling of the states. + * @param probabilityMatrix The transition probability relation of the + * CTMDP given by a matrix. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + */ + Ctmdp(std::shared_ptr> probabilityMatrix, + std::shared_ptr stateLabeling, + std::shared_ptr> rowMapping, + std::shared_ptr> stateRewards = nullptr, + std::shared_ptr> transitionRewardMatrix = nullptr) + : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping), + stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), + backwardTransitions(nullptr) { + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + } + + //! Copy Constructor + /*! + * Copy Constructor. Performs a deep copy of the given CTMDP. + * @param ctmdp A reference to the CTMDP that is to be copied. + */ + Ctmdp(const Ctmdp &ctmdp) : probabilityMatrix(ctmdp.probabilityMatrix), + stateLabeling(ctmdp.stateLabeling), rowMapping(ctmdp.rowMapping), stateRewards(ctmdp.stateRewards), + transitionRewardMatrix(ctmdp.transitionRewardMatrix) { + if (ctmdp.backwardTransitions != nullptr) { + this->backwardTransitions = new storm::models::GraphTransitions(*ctmdp.backwardTransitions); + } + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + } + + //! Destructor + /*! + * Destructor. Frees the matrix and labeling associated with this CTMDP. + */ + ~Ctmdp() { + if (this->backwardTransitions != nullptr) { + delete this->backwardTransitions; + } + } + + /*! + * Returns the state space size of the CTMDP. + * @return The size of the state space of the CTMDP. + */ + uint_fast64_t getNumberOfStates() const { + return this->probabilityMatrix->getColumnCount(); + } + + /*! + * Returns the number of (non-zero) transitions of the CTMDP. + * @return The number of (non-zero) transitions of the CTMDP. + */ + uint_fast64_t getNumberOfTransitions() const { + return this->probabilityMatrix->getNonZeroEntryCount(); + } + + /*! + * Returns a bit vector in which exactly those bits are set to true that + * correspond to a state labeled with the given atomic proposition. + * @param ap The atomic proposition for which to get the bit vector. + * @return A bit vector in which exactly those bits are set to true that + * correspond to a state labeled with the given atomic proposition. + */ + storm::storage::BitVector* getLabeledStates(std::string ap) const { + return this->stateLabeling->getAtomicProposition(ap); + } + + /*! + * Returns a pointer to the matrix representing the transition probability + * function. + * @return A pointer to the matrix representing the transition probability + * function. + */ + std::shared_ptr> getTransitionProbabilityMatrix() const { + 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; + } + + /*! + * + */ + std::set const getPropositionsForState(uint_fast64_t const &state) const { + return stateLabeling->getPropositionsForState(state); + } + + /*! + * Retrieves a reference to the backwards transition relation. + * @return A reference to the backwards transition relation. + */ + storm::models::GraphTransitions& getBackwardTransitions() { + if (this->backwardTransitions == nullptr) { + this->backwardTransitions = new storm::models::GraphTransitions(this->probabilityMatrix, false); + } + return *this->backwardTransitions; + } + + /*! + * Retrieves whether this CTMDP has a state reward model. + * @return True if this CTMDP has a state reward model. + */ + bool hasStateRewards() { + return this->stateRewards != nullptr; + } + + /*! + * Retrieves whether this CTMDP has a transition reward model. + * @return True if this CTMDP has a transition reward model. + */ + bool hasTransitionRewards() { + return this->transitionRewardMatrix != nullptr; + } + + /*! + * Retrieves whether the given atomic proposition is a valid atomic proposition in this model. + * @param atomicProposition The atomic proposition to be checked for validity. + * @return True if the given atomic proposition is valid in this model. + */ + bool hasAtomicProposition(std::string const& atomicProposition) { + return this->stateLabeling->containsAtomicProposition(atomicProposition); + } + + /*! + * Prints information about the model to the specified stream. + * @param out The stream the information is to be printed to. + */ + void printModelInformationToStream(std::ostream& out) const { + storm::utility::printSeparationLine(out); + out << std::endl; + out << "Model type: \t\tCTMDP" << std::endl; + out << "States: \t\t" << this->getNumberOfStates() << std::endl; + out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; + this->stateLabeling->printAtomicPropositionsInformationToStream(out); + out << "Size in memory: \t" + << (this->probabilityMatrix->getSizeInMemory() + + this->stateLabeling->getSizeInMemory() + + sizeof(*this))/1024 << " kbytes" << std::endl; + out << std::endl; + storm::utility::printSeparationLine(out); + } + + storm::models::ModelType getType() { + return CTMDP; + } + +private: + + /*! + * @brief Perform some sanity checks. + * + * Checks probability matrix if all rows sum up to one. + */ + bool checkValidityOfProbabilityMatrix() { + // Get the settings object to customize linear solving. + storm::settings::Settings* s = storm::settings::instance(); + double precision = s->get("precision"); + for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) { + T sum = this->probabilityMatrix->getRowSum(row); + if (sum == 0) continue; + if (std::abs(sum - 1) > precision) return false; + } + return true; + } + + /*! A matrix representing the transition probability function of the CTMDP. */ + std::shared_ptr> probabilityMatrix; + + /*! The labeling of the states of the CTMDP. */ + std::shared_ptr stateLabeling; + + /*! The mapping from states to rows. */ + std::shared_ptr> rowMapping; + + /*! The state-based rewards of the CTMDP. */ + std::shared_ptr> stateRewards; + + /*! The transition-based rewards of the CTMDP. */ + std::shared_ptr> transitionRewardMatrix; + + /*! + * A data structure that stores the predecessors for all states. This is + * needed for backwards directed searches. + */ + storm::models::GraphTransitions* backwardTransitions; +}; + +} // namespace models + +} // namespace storm + +#endif /* STORM_MODELS_CTMDP_H_ */ diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 110831ff6..6c0d5cc40 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -6,7 +6,7 @@ #include "src/exceptions/WrongFileFormatException.h" #include "src/models/AbstractModel.h" #include "src/parser/DeterministicModelParser.h" -#include "src/parser/MdpParser.h" +#include "src/parser/NonDeterministicModelParser.h" namespace storm { namespace parser { @@ -37,12 +37,15 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con break; } case storm::models::MDP: { - MdpParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); this->model = parser.getMdp(); break; } - case storm::models::CTMDP: + case storm::models::CTMDP: { + NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser.getCtmdp(); break; + } default: ; // Unknown } diff --git a/src/parser/MdpParser.h b/src/parser/MdpParser.h deleted file mode 100644 index e64356dc9..000000000 --- a/src/parser/MdpParser.h +++ /dev/null @@ -1,40 +0,0 @@ -/* - * MdpParser.h - * - * Created on: 14.01.2013 - * Author: thomas - */ - -#ifndef STORM_PARSER_MDPPARSER_H_ -#define STORM_PARSER_MDPPARSER_H_ - -#include "src/parser/Parser.h" -#include "src/models/Mdp.h" - -namespace storm { -namespace parser { - -/*! - * @brief Load label and transition file and return initialized mdp object - * - * @Note This class creates a new Mdp object that can - * be accessed via getMdp(). However, it will not delete this object! - * - * @Note The labeling representation in the file may use at most as much nodes as are specified in the mdp. - */ -class MdpParser: public storm::parser::Parser { -public: - MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); - - std::shared_ptr> getMdp() { - return this->mdp; - } - -private: - std::shared_ptr> mdp; -}; - -} /* namespace parser */ -} /* namespace storm */ -#endif /* STORM_PARSER_MDPPARSER_H_ */ diff --git a/src/parser/MdpParser.cpp b/src/parser/NonDeterministicModelParser.cpp similarity index 73% rename from src/parser/MdpParser.cpp rename to src/parser/NonDeterministicModelParser.cpp index ac73b4e40..017d3b31e 100644 --- a/src/parser/MdpParser.cpp +++ b/src/parser/NonDeterministicModelParser.cpp @@ -1,11 +1,11 @@ /* - * MdpParser.cpp + * NonDeterministicModelParser.cpp * * Created on: 14.01.2013 * Author: Philipp Berger */ -#include "src/parser/MdpParser.h" +#include "src/parser/NonDeterministicModelParser.h" #include #include @@ -27,25 +27,27 @@ namespace parser { * @param stateRewardFile String containing the location of the state reward file (...srew) * @param transitionRewardFile String containing the location of the transition reward file (...trew) */ -MdpParser::MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile, +NonDeterministicModelParser::NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { storm::parser::NonDeterministicSparseTransitionParser tp(transitionSystemFile); uint_fast64_t stateCount = tp.getMatrix()->getRowCount(); - std::shared_ptr> stateRewards = nullptr; - std::shared_ptr> transitionRewards = nullptr; - storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); if (stateRewardFile != "") { storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); - stateRewards = srp.getStateRewards(); + this->stateRewards = srp.getStateRewards(); } if (transitionRewardFile != "") { storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile); - transitionRewards = trp.getMatrix(); + this->transitionRewardMatrix = trp.getMatrix(); } - mdp = std::shared_ptr>(new storm::models::Mdp(tp.getMatrix(), lp.getLabeling(), tp.getRowMapping(), stateRewards, transitionRewards)); + this->probabilityMatrix = tp.getMatrix(); + this->stateLabeling = lp.getLabeling(); + this->rowMapping = tp.getRowMapping(); + + this->mdp = nullptr; + this->ctmdp = nullptr; } } /* namespace parser */ diff --git a/src/parser/NonDeterministicModelParser.h b/src/parser/NonDeterministicModelParser.h new file mode 100644 index 000000000..b203154a7 --- /dev/null +++ b/src/parser/NonDeterministicModelParser.h @@ -0,0 +1,62 @@ +/* + * NonDeterministicModelParser.h + * + * Created on: 14.01.2013 + * Author: thomas + */ + +#ifndef STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ +#define STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ + +#include "src/parser/Parser.h" +#include "src/models/Mdp.h" +#include "src/models/Ctmdp.h" + +namespace storm { +namespace parser { + +/*! + * @brief Load label and transition file and return initialized mdp object + * + * @Note This class creates a new Mdp object that can + * be accessed via getMdp(). However, it will not delete this object! + * + * @Note The labeling representation in the file may use at most as much nodes as are specified in the mdp. + */ +class NonDeterministicModelParser: public storm::parser::Parser { +public: + NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + + std::shared_ptr> getMdp() { + if (this->mdp == nullptr) { + this->mdp = std::shared_ptr>(new storm::models::Mdp( + this->probabilityMatrix, this->stateLabeling, this->rowMapping, this->stateRewards, this->transitionRewardMatrix + )); + } + return this->mdp; + } + + std::shared_ptr> getCtmdp() { + if (this->ctmdp == nullptr) { + this->ctmdp = std::shared_ptr>(new storm::models::Ctmdp( + this->probabilityMatrix, this->stateLabeling, this->rowMapping, this->stateRewards, this->transitionRewardMatrix + )); + } + return this->ctmdp; + } + +private: + std::shared_ptr> probabilityMatrix; + std::shared_ptr stateLabeling; + std::shared_ptr> rowMapping; + std::shared_ptr> stateRewards; + std::shared_ptr> transitionRewardMatrix; + + std::shared_ptr> mdp; + std::shared_ptr> ctmdp; +}; + +} /* namespace parser */ +} /* namespace storm */ +#endif /* STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ */ diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp index 53100426b..353b470c2 100644 --- a/test/parser/ParseMdpTest.cpp +++ b/test/parser/ParseMdpTest.cpp @@ -8,12 +8,12 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/parser/MdpParser.h" +#include "src/parser/NonDeterministicModelParser.h" #include "src/utility/IoUtility.h" TEST(ParseMdpTest, parseAndOutput) { - storm::parser::MdpParser* mdpParser = nullptr; - ASSERT_NO_THROW(mdpParser = new storm::parser::MdpParser( + storm::parser::NonDeterministicModelParser* mdpParser = nullptr; + ASSERT_NO_THROW(mdpParser = new storm::parser::NonDeterministicModelParser( STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));