MemoryStructureBuilder.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <vector>
 
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/storage/memorystructure/MemoryStructure.h"
 
namespace storm {
namespace storage {
 
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
class MemoryStructureBuilder {
   public:
    MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model,
                           bool onlyInitialStatesRelevant = true);
 
    MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model<ValueType, RewardModelType> const& model);
 
    void setInitialMemoryState(uint_fast64_t initialModelState, uint_fast64_t initialMemoryState);
 
    void setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, storm::storage::BitVector const& modelStates,
                       boost::optional<storm::storage::BitVector> const& modelChoices = boost::none);
 
    void setLabel(uint_fast64_t const& state, std::string const& label);
 
    MemoryStructure build();
 
    static MemoryStructure buildTrivialMemoryStructure(storm::models::sparse::Model<ValueType, RewardModelType> const& model);
 
   private:
    storm::models::sparse::Model<ValueType, RewardModelType> const& model;
    MemoryStructure::TransitionMatrix transitions;
    storm::models::sparse::StateLabeling stateLabeling;
    std::vector<uint_fast64_t> initialMemoryStates;
    bool onlyInitialStatesRelevant;
};
 
}  // namespace storage
}  // namespace storm