diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 303a77739..c766da8cb 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -18,7 +18,7 @@ #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" namespace storm { @@ -49,8 +49,9 @@ public: : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), backwardTransitions(nullptr) { - if (!this->checkValidityProbabilityMatrix()) { - std::cerr << "Probability matrix is invalid" << std::endl; + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; } } @@ -65,8 +66,9 @@ public: if (dtmc.backwardTransitions != nullptr) { this->backwardTransitions = new storm::models::GraphTransitions(*dtmc.backwardTransitions); } - if (!this->checkValidityProbabilityMatrix()) { - std::cerr << "Probability matrix is invalid" << std::endl; + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; } } @@ -206,11 +208,20 @@ private: * * Checks probability matrix if all rows sum up to one. */ - bool checkValidityProbabilityMatrix() { + bool checkValidityOfProbabilityMatrix() { + // Get the settings object to customize linear solving. + storm::settings::Settings* s = storm::settings::instance(); + double precision = s->get("precision"); + + if (this->probabilityMatrix->getRowCount() != this->probabilityMatrix->getColumnCount()) { + // not square + return false; + } + 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) > 1e-10) return false; + if (sum == 0) return false; + if (std::abs(sum - 1) > precision) return false; } return true; } diff --git a/src/models/Mdp.h b/src/models/Mdp.h new file mode 100644 index 000000000..dc58782a2 --- /dev/null +++ b/src/models/Mdp.h @@ -0,0 +1,246 @@ +/* + * Mdp.h + * + * Created on: 14.01.2013 + * Author: Philipp Berger + */ + +#ifndef STORM_MODELS_MDP_H_ +#define STORM_MODELS_MDP_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" + +namespace storm { + +namespace models { + +/*! + * This class represents a Markov Decision Process (MDP) whose states are + * labeled with atomic propositions. + */ +template +class Mdp : public storm::models::AbstractModel { + +public: + //! Constructor + /*! + * Constructs a MDP object from the given transition probability matrix and + * the given labeling of the states. + * @param probabilityMatrix The transition probability relation of the + * MDP given by a matrix. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + */ + Mdp(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->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 MDP. + * @param mdp A reference to the MDP that is to be copied. + */ + Mdp(const Mdp &mdp) : probabilityMatrix(mdp.probabilityMatrix), + stateLabeling(mdp.stateLabeling), stateRewards(mdp.stateRewards), + transitionRewardMatrix(mdp.transitionRewardMatrix) { + if (mdp.backwardTransitions != nullptr) { + this->backwardTransitions = new storm::models::GraphTransitions(*mdp.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 MDP. + */ + ~Mdp() { + if (this->backwardTransitions != nullptr) { + delete this->backwardTransitions; + } + } + + /*! + * Returns the state space size of the MDP. + * @return The size of the state space of the MDP. + */ + uint_fast64_t getNumberOfStates() const { + return this->probabilityMatrix->getColumnCount(); + } + + /*! + * Returns the number of (non-zero) transitions of the MDP. + * @return The number of (non-zero) transitions of the MDP. + */ + 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 MDP has a state reward model. + * @return True if this MDP has a state reward model. + */ + bool hasStateRewards() { + return this->stateRewards != nullptr; + } + + /*! + * Retrieves whether this MDP has a transition reward model. + * @return True if this MDP 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\tMDP" << 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 MDP; + } + +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 MDP. */ + std::shared_ptr> probabilityMatrix; + + /*! The labeling of the states of the MDP. */ + std::shared_ptr stateLabeling; + + /*! The state-based rewards of the MDP. */ + std::shared_ptr> stateRewards; + + /*! The transition-based rewards of the MDP. */ + 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_MDP_H_ */ diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index f52b2cf8e..f2d161559 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -6,6 +6,7 @@ #include "src/exceptions/WrongFileFormatException.h" #include "src/models/AbstractModel.h" #include "src/parser/DtmcParser.h" +#include "src/parser/MdpParser.h" namespace storm { namespace parser { @@ -26,14 +27,17 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con // Do actual parsing switch (type) { case storm::models::DTMC: { - DtmcParser* parser = new DtmcParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - this->model = parser->getDtmc(); - break; - } + DtmcParser* parser = new DtmcParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser->getDtmc(); + break; + } case storm::models::CTMC: break; - case storm::models::MDP: + case storm::models::MDP: { + MdpParser* parser = new MdpParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser->getMdp(); break; + } case storm::models::CTMDP: break; default: ; // Unknown diff --git a/src/parser/DtmcParser.h b/src/parser/DtmcParser.h index 7cf45a335..b1f746bb5 100644 --- a/src/parser/DtmcParser.h +++ b/src/parser/DtmcParser.h @@ -5,8 +5,8 @@ * Author: thomas */ -#ifndef DTMCPARSER_H_ -#define DTMCPARSER_H_ +#ifndef STORM_PARSER_DTMCPARSER_H_ +#define STORM_PARSER_DTMCPARSER_H_ #include "src/parser/Parser.h" #include "src/models/Dtmc.h" @@ -37,4 +37,4 @@ private: } /* namespace parser */ } /* namespace storm */ -#endif /* DTMCPARSER_H_ */ +#endif /* STORM_PARSER_DTMCPARSER_H_ */ diff --git a/src/parser/MdpParser.cpp b/src/parser/MdpParser.cpp new file mode 100644 index 000000000..f73c0b515 --- /dev/null +++ b/src/parser/MdpParser.cpp @@ -0,0 +1,53 @@ +/* + * MdpParser.cpp + * + * Created on: 14.01.2013 + * Author: Philipp Berger + */ + +#include "src/parser/MdpParser.h" + +#include +#include + +#include "src/parser/NonDeterministicSparseTransitionParser.h" +#include "src/parser/AtomicPropositionLabelingParser.h" +#include "src/parser/SparseStateRewardParser.h" + +namespace storm { +namespace parser { + +/*! + * Parses a transition file and a labeling file and produces a MDP out of them; a pointer to the mdp + * is saved in the field "mdp" + * Note that the labeling file may have at most as many nodes as the transition file! + * + * @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) + */ +MdpParser::MdpParser(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(); + } + if (transitionRewardFile != "") { + storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile); + transitionRewards = trp.getMatrix(); + } + + mdp = std::shared_ptr>(new storm::models::Mdp(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); +} + +} /* namespace parser */ + +} /* namespace storm */ diff --git a/src/parser/MdpParser.h b/src/parser/MdpParser.h new file mode 100644 index 000000000..e64356dc9 --- /dev/null +++ b/src/parser/MdpParser.h @@ -0,0 +1,40 @@ +/* + * 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/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 3a84cf4ad..433501efb 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -795,13 +795,15 @@ public: * value. */ void invertDiagonal() { + if (this->getRowCount() != this->getColumnCount()) { + throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!"; + } T one(1); for (uint_fast64_t row = 0; row < rowCount; ++row) { uint_fast64_t rowStart = rowIndications[row]; uint_fast64_t rowEnd = rowIndications[row + 1]; - uint_fast64_t pseudoDiagonal = row % colCount; while (rowStart < rowEnd) { - if (columnIndications[rowStart] == pseudoDiagonal) { + if (columnIndications[rowStart] == row) { valueStorage[rowStart] = one - valueStorage[rowStart]; break; } @@ -814,12 +816,14 @@ public: * Negates all non-zero elements that are not on the diagonal. */ void negateAllNonDiagonalElements() { + if (this->getRowCount() != this->getColumnCount()) { + throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!"; + } for (uint_fast64_t row = 0; row < rowCount; ++row) { uint_fast64_t rowStart = rowIndications[row]; uint_fast64_t rowEnd = rowIndications[row + 1]; - uint_fast64_t pseudoDiagonal = row % colCount; while (rowStart < rowEnd) { - if (columnIndications[rowStart] != pseudoDiagonal) { + if (columnIndications[rowStart] != row) { valueStorage[rowStart] = - valueStorage[rowStart]; } ++rowStart; diff --git a/src/vector/dense_vector.h b/src/vector/dense_vector.h new file mode 100644 index 000000000..b118d8e5d --- /dev/null +++ b/src/vector/dense_vector.h @@ -0,0 +1,183 @@ +#ifndef MRMC_VECTOR_BITVECTOR_H_ +#define MRMC_VECTOR_BITVECTOR_H_ + +#include +#include +#include +#include "boost/integer/integer_mask.hpp" + +#include +#include + +#include "src/exceptions/invalid_state.h" +#include "src/exceptions/invalid_argument.h" +#include "src/exceptions/out_of_range.h" + +namespace mrmc { + +namespace vector { + +//! A Vector +/*! + A bit vector for boolean fields or quick selection schemas on Matrix entries. + Does NOT perform index bound checks! + */ +template +class DenseVector { + public: + //! Constructor + /*! + \param initial_length The initial size of the boolean Array. Can be changed later on via BitVector::resize() + */ + BitVector(uint_fast64_t initial_length) { + bucket_count = initial_length / 64; + if (initial_length % 64 != 0) { + ++bucket_count; + } + bucket_array = new uint_fast64_t[bucket_count](); + + // init all 0 + for (uint_fast64_t i = 0; i < bucket_count; ++i) { + bucket_array[i] = 0; + } + } + + //! Copy Constructor + /*! + Copy Constructor. Creates an exact copy of the source bit vector bv. Modification of either bit vector does not affect the other. + @param bv A reference to the bit vector that should be copied from + */ + BitVector(const BitVector &bv) : bucket_count(bv.bucket_count) + { + pantheios::log_DEBUG("BitVector::CopyCTor: Using Copy() Ctor."); + bucket_array = new uint_fast64_t[bucket_count](); + memcpy(bucket_array, bv.bucket_array, sizeof(uint_fast64_t) * bucket_count); + } + + ~BitVector() { + if (bucket_array != NULL) { + delete[] bucket_array; + } + } + + void resize(uint_fast64_t new_length) { + uint_fast64_t* tempArray = new uint_fast64_t[new_length](); + + // 64 bit/entries per uint_fast64_t + uint_fast64_t copySize = (new_length <= (bucket_count * 64)) ? (new_length/64) : (bucket_count); + memcpy(tempArray, bucket_array, sizeof(uint_fast64_t) * copySize); + + bucket_count = new_length / 64; + if (new_length % 64 != 0) { + ++bucket_count; + } + + delete[] bucket_array; + bucket_array = tempArray; + } + + void set(const uint_fast64_t index, const bool value) { + uint_fast64_t bucket = index / 64; + // Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one. + // MSVC: C4334, use 1i64 or cast to __int64. + // result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?) + uint_fast64_t mask = 1; + mask = mask << (index % 64); + if (value) { + bucket_array[bucket] |= mask; + } else { + bucket_array[bucket] &= ~mask; + } + } + + bool get(const uint_fast64_t index) { + uint_fast64_t bucket = index / 64; + // Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one. + // MSVC: C4334, use 1i64 or cast to __int64. + // result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?) + uint_fast64_t mask = 1; + mask = mask << (index % 64); + return ((bucket_array[bucket] & mask) == mask); + } + + // Operators + BitVector operator &(BitVector const &bv) { + uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; + BitVector result(minSize * 64); + for (uint_fast64_t i = 0; i < minSize; ++i) { + result.bucket_array[i] = this->bucket_array[i] & bv.bucket_array[i]; + } + + return result; + } + BitVector operator |(BitVector const &bv) { + uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; + BitVector result(minSize * 64); + for (uint_fast64_t i = 0; i < minSize; ++i) { + result.bucket_array[i] = this->bucket_array[i] | bv.bucket_array[i]; + } + + return result; + } + + BitVector operator ^(BitVector const &bv) { + uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; + BitVector result(minSize * 64); + for (uint_fast64_t i = 0; i < minSize; ++i) { + result.bucket_array[i] = this->bucket_array[i] ^ bv.bucket_array[i]; + } + + return result; + } + + BitVector operator ~() { + BitVector result(this->bucket_count * 64); + for (uint_fast64_t i = 0; i < this->bucket_count; ++i) { + result.bucket_array[i] = ~this->bucket_array[i]; + } + + return result; + } + + /*! + * Returns the number of bits that are set (to one) in this bit vector. + * @return The number of bits that are set (to one) in this bit vector. + */ + uint_fast64_t getNumberOfSetBits() { + uint_fast64_t set_bits = 0; + for (uint_fast64_t i = 0; i < bucket_count; i++) { +#ifdef __GNUG__ // check if we are using g++ and use built-in function if available + set_bits += __builtin_popcount (this->bucket_array[i]); +#else + uint_fast32_t cnt; + uint_fast64_t bitset = this->bucket_array[i]; + for (cnt = 0; bitset; cnt++) { + bitset &= bitset - 1; + } + set_bits += cnt; +#endif + } + return set_bits; + } + + /*! + * Returns the size of the bit vector in memory measured in bytes. + * @return The size of the bit vector in memory measured in bytes. + */ + uint_fast64_t getSizeInMemory() { + return sizeof(*this) + sizeof(uint_fast64_t) * bucket_count; + } + + private: + uint_fast64_t bucket_count; + + /*! Array containing the boolean bits for each node, 64bits/64nodes per element */ + uint_fast64_t* bucket_array; + +}; + +} // namespace vector + +} // namespace mrmc + +#endif // MRMC_SPARSE_STATIC_SPARSE_MATRIX_H_ diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp new file mode 100644 index 000000000..4147c0122 --- /dev/null +++ b/test/parser/ParseMdpTest.cpp @@ -0,0 +1,32 @@ +/* + * ParseMdpTest.cpp + * + * Created on: 14.01.2013 + * Author: Thomas Heinemann + */ + + +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/MdpParser.h" +#include "src/utility/IoUtility.h" + +TEST(ParseMdpTest, parseAndOutput) { + storm::parser::MdpParser* mdpParser; + ASSERT_NO_THROW(mdpParser = new storm::parser::MdpParser( + 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")); + + std::shared_ptr> mdp = mdpParser->getMdp(); + std::shared_ptr> matrix = mdp->getTransitionProbabilityMatrix(); + + ASSERT_EQ(mdp->getNumberOfStates(), 3); + ASSERT_EQ(mdp->getNumberOfTransitions(), 11); + ASSERT_EQ(matrix->getRowCount(), 2 * 3); + ASSERT_EQ(matrix->getColumnCount(), 3); + + + delete mdpParser; +} + + diff --git a/test/mrmc-tests.cpp b/test/storm-tests.cpp similarity index 100% rename from test/mrmc-tests.cpp rename to test/storm-tests.cpp