MemoryIncorporation.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
 
#include "storm/logic/Formula.h"
#include "storm/logic/MultiObjectiveFormula.h"
#include "storm/storage/memorystructure/MemoryStructure.h"
#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h"
 
namespace storm {
namespace transformer {
 
template<class SparseModelType>
class MemoryIncorporation {
    typedef typename SparseModelType::ValueType ValueType;
    typedef typename SparseModelType::RewardModelType RewardModelType;
 
   public:
    static std::shared_ptr<SparseModelType> incorporateGoalMemory(SparseModelType const& model,
                                                                  std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
 
    static std::pair<std::shared_ptr<SparseModelType>, storm::storage::SparseModelMemoryProductReverseData> incorporateGoalMemoryWithReverseData(
        SparseModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
 
    static std::shared_ptr<SparseModelType> incorporateFullMemory(SparseModelType const& model, uint64_t memoryStates);
 
    static std::shared_ptr<SparseModelType> incorporateCountingMemory(SparseModelType const& model, uint64_t memoryStates);
};
}  // namespace transformer
}  // namespace storm