RewardBoundUnfolder.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <memory>
#include <set>
#include <string>
#include <vector>
 
#include "storm/logic/Formula.h"
#include "storm/models/sparse/Pomdp.h"
 
namespace storm::pomdp::transformer {
// TODO this may be moved to storm/transformer
template<typename ValueType>
class RewardBoundUnfolder {
   public:
    struct ReturnType {
        std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
        std::shared_ptr<storm::logic::Formula> formula;
    };
 
    struct UnfoldingOptions {
        std::vector<uint64_t> levelWidths{};

        std::set<std::string> preservedRewardModels{};
    };

    static ReturnType transform(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula,
                                UnfoldingOptions const& options = {});
};
 
}  // namespace storm::pomdp::transformer