ExplicitTruncatedModelBuilder.h

#ifndef STAMINA_BUILDER_EXPLICITTRUNCATEDMODELBUILDER_H
#define STAMINA_BUILDER_EXPLICITTRUNCATEDMODELBUILDER_H
 
#include <boost/container/flat_map.hpp>
#include <boost/functional/hash.hpp>
#include <boost/variant.hpp>
#include <cstdint>
#include <deque>
#include <memory>
#include <utility>
#include <vector>
#include "storm/models/sparse/StandardRewardModel.h"
 
#include "storm/builder/ExplicitModelBuilder.h"
 
#include "storm/logic/Formulas.h"
#include "storm/models/sparse/ChoiceLabeling.h"
#include "storm/models/sparse/Model.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/settings/SettingsManager.h"
#include "storm/storage/BitVectorHashMap.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/expressions/ExpressionEvaluator.h"
#include "storm/storage/prism/Program.h"
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/storage/sparse/StateStorage.h"
 
#include "storm/utility/prism.h"
 
#include "storm/builder/ExplorationOrder.h"
 
#include "storm/generator/CompressedState.h"
#include "storm/generator/NextStateGenerator.h"
#include "storm/generator/VariableInformation.h"
 
namespace stamina {
 
namespace builder {
 
using namespace storm::utility::prism;
using namespace storm::generator;
using namespace storm::builder;
using namespace storm;
 
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
class ExplicitTruncatedModelBuilder {
public:
    struct Options {
        Options();
 
        // The order in which to explore the model.
        ExplorationOrder explorationOrder;
    };
 
    ExplicitTruncatedModelBuilder(std::shared_ptr<storm::generator::NextStateGenerator<ValueType, StateType>> const& generator, Options const& options = Options());
 
    ExplicitTruncatedModelBuilder(storm::prism::Program const& program,
                        storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(),
                        Options const& builderOptions = Options());
 
    ExplicitTruncatedModelBuilder(storm::jani::Model const& model,
                        storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(),
                        Options const& builderOptions = Options());
 
    std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build();
 
    ExplicitStateLookup<StateType> exportExplicitStateLookup() const;
 
private:
    StateType getOrAddStateIndex(CompressedState const& state);
 
    void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder,
                    std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders,
                    StateAndChoiceInformationBuilder& stateAndChoiceInformationBuilder);
 
    storm::storage::sparse::ModelComponents<ValueType, RewardModelType> buildModelComponents();
 
    storm::models::sparse::StateLabeling buildStateLabeling();
 
    std::shared_ptr<storm::generator::NextStateGenerator<ValueType, StateType>> generator;
 
    Options options;
 
    storm::storage::sparse::StateStorage<StateType> stateStorage;
 
    std::deque<std::pair<CompressedState, StateType>> statesToExplore;
 
    boost::optional<std::vector<uint_fast64_t>> stateRemapping;
    uint64_t numberOfExploredStates;
};
 
}
}  // namespace stamina
 
#endif /* STAMINA_BUILDER_EXPLICITTRUNCATEDMODELBUILDER_H */