ExplicitModelBuilder.h

Go to the documentation of this file.

#pragma once
 
#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/logic/Formulas.h"
#include "storm/models/sparse/ChoiceLabeling.h"
#include "storm/models/sparse/Model.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/storage/BitVectorHashMap.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/prism/Program.h"
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/storage/sparse/StateStorage.h"
 
#include "storm/builder/ExplorationOrder.h"
 
#include "storm/generator/CompressedState.h"
#include "storm/generator/NextStateGenerator.h"
#include "storm/generator/VariableInformation.h"
 
namespace storm {
 
namespace builder {
 
using namespace storm::generator;
 
// Forward-declare classes.
template<typename ValueType>
class RewardModelBuilder;
class StateAndChoiceInformationBuilder;
 
template<typename StateType>
class ExplicitStateLookup {
   public:
    ExplicitStateLookup(VariableInformation const& varInfo, storm::storage::BitVectorHashMap<StateType> const& stateToId)
        : varInfo(varInfo), stateToId(stateToId) {
        // intentionally left empty.
    }

    StateType lookup(std::map<storm::expressions::Variable, storm::expressions::Expression> const& stateDescription) const;
    uint64_t size() const;
 
   private:
    VariableInformation varInfo;
    storm::storage::BitVectorHashMap<StateType> stateToId;
};
 
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
class ExplicitModelBuilder {
   public:
    struct Options {
        Options();
 
        // The order in which to explore the model.
        ExplorationOrder explorationOrder;
 
        // If set, deadlocks states will be fixed by adding a self-loop with probability 1.
        bool fixDeadlocks;
 
        // If set, no further states will be explored once the given number is exceeded.
        std::optional<StateType> explorationStateLimit;
    };

    ExplicitModelBuilder(std::shared_ptr<storm::generator::NextStateGenerator<ValueType, StateType>> const& generator, Options const& options = Options());

    ExplicitModelBuilder(storm::prism::Program const& program,
                         storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(),
                         Options const& builderOptions = Options());

    ExplicitModelBuilder(storm::jani::Model const& model,
                         storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(),
                         Options const& builderOptions = Options())
        requires(!storm::IsIntervalType<ValueType>);

    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;
};
 
}  // namespace builder
}  // namespace storm