gereon
12 years ago
9 changed files with 593 additions and 20 deletions
-
27src/models/Dtmc.h
-
246src/models/Mdp.h
-
14src/parser/AutoParser.cpp
-
6src/parser/DtmcParser.h
-
53src/parser/MdpParser.cpp
-
40src/parser/MdpParser.h
-
12src/storage/SparseMatrix.h
-
183src/vector/dense_vector.h
-
32test/parser/ParseMdpTest.cpp
@ -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_ */ |
|||
@ -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 */ |
|||
@ -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_ */ |
|||
@ -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_ |
|||
@ -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; |
|||
} |
|||
|
|||
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue