Browse Source

Added Mdp Class, Parser and support in the AutoParser.

Added Test for MdpParser
tempestpy_adaptions
PBerger 12 years ago
parent
commit
7800132684
  1. 27
      src/models/Dtmc.h
  2. 246
      src/models/Mdp.h
  3. 6
      src/parser/AutoParser.cpp
  4. 6
      src/parser/DtmcParser.h
  5. 53
      src/parser/MdpParser.cpp
  6. 40
      src/parser/MdpParser.h
  7. 12
      src/storage/SparseMatrix.h
  8. 183
      src/vector/dense_vector.h
  9. 32
      test/parser/ParseMdpTest.cpp
  10. 0
      test/storm-tests.cpp

27
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<T>(*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<double>("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;
}

246
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 <ostream>
#include <iostream>
#include <memory>
#include <cstdlib>
#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 T>
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<storm::storage::SparseMatrix<T>> probabilityMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
std::shared_ptr<std::vector<T>> stateRewards = nullptr,
std::shared_ptr<storm::storage::SparseMatrix<T>> 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<T> &mdp) : probabilityMatrix(mdp.probabilityMatrix),
stateLabeling(mdp.stateLabeling), stateRewards(mdp.stateRewards),
transitionRewardMatrix(mdp.transitionRewardMatrix) {
if (mdp.backwardTransitions != nullptr) {
this->backwardTransitions = new storm::models::GraphTransitions<T>(*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<storm::storage::SparseMatrix<T>> 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<storm::storage::SparseMatrix<T>> 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<std::vector<T>> getStateRewards() const {
return this->stateRewards;
}
/*!
*
*/
std::set<std::string> 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<T>& getBackwardTransitions() {
if (this->backwardTransitions == nullptr) {
this->backwardTransitions = new storm::models::GraphTransitions<T>(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<double>("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<storm::storage::SparseMatrix<T>> probabilityMatrix;
/*! The labeling of the states of the MDP. */
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
/*! The state-based rewards of the MDP. */
std::shared_ptr<std::vector<T>> stateRewards;
/*! The transition-based rewards of the MDP. */
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
/*!
* A data structure that stores the predecessors for all states. This is
* needed for backwards directed searches.
*/
storm::models::GraphTransitions<T>* backwardTransitions;
};
} // namespace models
} // namespace storm
#endif /* STORM_MODELS_MDP_H_ */

6
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 {
@ -32,8 +33,11 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con
}
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

6
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_ */

53
src/parser/MdpParser.cpp

@ -0,0 +1,53 @@
/*
* MdpParser.cpp
*
* Created on: 14.01.2013
* Author: Philipp Berger
*/
#include "src/parser/MdpParser.h"
#include <string>
#include <vector>
#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<std::vector<double>> stateRewards = nullptr;
std::shared_ptr<storm::storage::SparseMatrix<double>> 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<storm::models::Mdp<double>>(new storm::models::Mdp<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards));
}
} /* namespace parser */
} /* namespace storm */

40
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<storm::models::Mdp<double>> getMdp() {
return this->mdp;
}
private:
std::shared_ptr<storm::models::Mdp<double>> mdp;
};
} /* namespace parser */
} /* namespace storm */
#endif /* STORM_PARSER_MDPPARSER_H_ */

12
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;

183
src/vector/dense_vector.h

@ -0,0 +1,183 @@
#ifndef MRMC_VECTOR_BITVECTOR_H_
#define MRMC_VECTOR_BITVECTOR_H_
#include <exception>
#include <new>
#include <cmath>
#include "boost/integer/integer_mask.hpp"
#include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp>
#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 T>
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_

32
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<storm::models::Mdp<double>> mdp = mdpParser->getMdp();
std::shared_ptr<storm::storage::SparseMatrix<double>> 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;
}

0
test/mrmc-tests.cpp → test/storm-tests.cpp

Loading…
Cancel
Save