MemoryStructure.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <vector>
 
#include "storm/logic/Formula.h"
#include "storm/models/sparse/Model.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/StateLabeling.h"
 
namespace storm {
namespace storage {
 
template<typename ValueType, typename RewardModelType>
class SparseModelMemoryProduct;

class MemoryStructure {
   public:
    typedef std::vector<std::vector<boost::optional<storm::storage::BitVector>>> TransitionMatrix;

    MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling,
                    std::vector<uint_fast64_t> const& initialMemoryStates, bool onlyInitialStatesRelevant = true);
    MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling,
                    std::vector<uint_fast64_t>&& initialMemoryStates, bool onlyInitialStatesRelevant = true);
 
    bool isOnlyInitialStatesRelevantSet() const;
    TransitionMatrix const& getTransitionMatrix() const;
    storm::models::sparse::StateLabeling const& getStateLabeling() const;
    std::vector<uint_fast64_t> const& getInitialMemoryStates() const;
    uint_fast64_t getNumberOfStates() const;
 
    uint_fast64_t getSuccessorMemoryState(uint_fast64_t const& currentMemoryState, uint_fast64_t const& modelTransitionIndex) const;

    MemoryStructure product(MemoryStructure const& rhs) const;

    template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
    SparseModelMemoryProduct<ValueType, RewardModelType> product(storm::models::sparse::Model<ValueType, RewardModelType> const& sparseModel) const;
 
    std::string toString() const;
 
   private:
    TransitionMatrix transitions;
    storm::models::sparse::StateLabeling stateLabeling;
    std::vector<uint_fast64_t> initialMemoryStates;
    bool onlyInitialStatesRelevant;  // Whether initial memory states are only defined for initial model states or for all model states
};
 
}  // namespace storage
}  // namespace storm