NextStateGenerator.h

Go to the documentation of this file.

#ifndef STORM_GENERATOR_NEXTSTATEGENERATOR_H_
#define STORM_GENERATOR_NEXTSTATEGENERATOR_H_
 
#include <cstdint>
#include <vector>
 
#include <boost/variant.hpp>
 
#include "storm/storage/PlayerIndex.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/sparse/ChoiceOrigins.h"
#include "storm/storage/sparse/StateStorage.h"
#include "storm/storage/sparse/StateValuations.h"
 
#include "storm/builder/BuilderOptions.h"
#include "storm/builder/RewardModelInformation.h"
 
#include "storm/generator/CompressedState.h"
#include "storm/generator/StateBehavior.h"
#include "storm/generator/VariableInformation.h"
 
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/utility/ConstantsComparator.h"
 
namespace storm {
namespace expressions {
template<typename V>
class ExpressionEvaluator;
class SimpleValuation;
}  // namespace expressions
namespace generator {
typedef storm::builder::BuilderOptions NextStateGeneratorOptions;
 
enum class ModelType { DTMC, CTMC, MDP, MA, POMDP, SMG };
 
template<typename ValueType, typename StateType = uint32_t>
class NextStateGenerator;
 
template<typename ValueType, typename StateType = uint32_t>
class ActionMask {
   public:
    virtual ~ActionMask() = default;
    virtual bool query(storm::generator::NextStateGenerator<ValueType, StateType> const& generator, uint64_t actionIndex) = 0;
};
 
template<typename ValueType, typename StateType = uint32_t>
class StateValuationFunctionMask : public ActionMask<ValueType, StateType> {
   public:
    StateValuationFunctionMask(std::function<bool(storm::expressions::SimpleValuation const&, uint64_t)> const& f);
    virtual ~StateValuationFunctionMask() = default;
    bool query(storm::generator::NextStateGenerator<ValueType, StateType> const& generator, uint64_t actionIndex) override;
 
   private:
    std::function<bool(storm::expressions::SimpleValuation, uint64_t)> func;
};
 
template<typename ValueType, typename StateType>
class NextStateGenerator {
   public:
    typedef std::function<StateType(CompressedState const&)> StateToIdCallback;
 
    NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation,
                       NextStateGeneratorOptions const& options, std::shared_ptr<ActionMask<ValueType, StateType>> const& = nullptr);
 
    NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options,
                       std::shared_ptr<ActionMask<ValueType, StateType>> const& = nullptr);
 
    virtual ~NextStateGenerator();
 
    uint64_t getStateSize() const;
    virtual ModelType getModelType() const = 0;
    virtual bool isDeterministicModel() const = 0;
    virtual bool isDiscreteTimeModel() const = 0;
    virtual bool isPartiallyObservable() const = 0;
    virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
 
    void initializeSpecialStates();
 
    virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const;
 
    void load(CompressedState const& state);
    virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) = 0;
    bool satisfies(storm::expressions::Expression const& expression) const;
 
    virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex,
                                   storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const;
    virtual storm::storage::sparse::StateValuations makeObservationValuation() const;
 
    virtual std::size_t getNumberOfRewardModels() const = 0;
    virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0;
 
    std::string stateToString(CompressedState const& state) const;
 
    storm::json<ValueType> currentStateToJson(bool onlyObservable = false) const;
    storm::expressions::SimpleValuation currentStateToSimpleValuation() const;
 
    uint32_t observabilityClass(CompressedState const& state) const;
 
    virtual std::map<std::string, storm::storage::PlayerIndex> getPlayerNameToIndexMap() const;
 
    virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage,
                                                       std::vector<StateType> const& initialStateIndices = {},
                                                       std::vector<StateType> const& deadlockStateIndices = {},
                                                       std::vector<StateType> const& unexploredStateIndices = {}) = 0;
 
    NextStateGeneratorOptions const& getOptions() const;
 
    VariableInformation const& getVariableInformation() const;
 
    virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const;
 
    void remapStateIds(std::function<StateType(StateType const&)> const& remapping);
 
   protected:
    using BaseValueType = storm::IntervalBaseType<ValueType>;
 
    bool isSpecialLabel(std::string const& label) const;
 
    storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage,
                                               std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices,
                                               std::vector<StateType> const& unexploredStateIndices,
                                               std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
 
    virtual void unpackTransientVariableValuesIntoEvaluator(CompressedState const& state,
                                                            storm::expressions::ExpressionEvaluator<BaseValueType>& evaluator) const;
 
    virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const = 0;
 
    virtual void extendStateInformation(storm::json<BaseValueType>& stateInfo) const;
 
    virtual storm::storage::sparse::StateValuationsBuilder initializeObservationValuationsBuilder() const;
 
    void postprocess(StateBehavior<ValueType, StateType>& result);
 
    NextStateGeneratorOptions options;
 
    std::shared_ptr<storm::expressions::ExpressionManager const> expressionManager;
 
    std::vector<std::pair<storm::expressions::Expression, bool>> terminalStates;
 
    VariableInformation variableInformation;
 
    std::unique_ptr<storm::expressions::ExpressionEvaluator<BaseValueType>> evaluator;
 
    CompressedState const* state;
 
    storm::utility::ConstantsComparator<ValueType> comparator;
 
    mutable storm::storage::BitVector mask;
 
    // TODO consider using a BitVectorHashMap for this?
    mutable std::unordered_map<storm::storage::BitVector, uint32_t> observabilityMap;
    CompressedState outOfBoundsState;
 
    boost::optional<std::vector<uint64_t>> overlappingGuardStates;
 
    std::shared_ptr<ActionMask<ValueType, StateType>> actionMask;
};
}  // namespace generator
}  // namespace storm
 
#endif /* STORM_GENERATOR_NEXTSTATEGENERATOR_H_ */