PrismNextStateGenerator.h

Go to the documentation of this file.

#pragma once
 
#include "storm/generator/NextStateGenerator.h"
 
#include "storm/storage/BoostTypes.h"
#include "storm/storage/prism/Program.h"
 
namespace storm {
namespace generator {
template<typename StateType, typename ValueType>
class Distribution;
 
template<typename ValueType, typename StateType = uint32_t>
class PrismNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
   public:
    typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
    typedef storm::storage::FlatSet<uint_fast64_t> CommandSet;
    enum class CommandFilter { All, Markovian, Probabilistic };
 
    PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options = NextStateGeneratorOptions(),
                            std::shared_ptr<ActionMask<ValueType, StateType>> const& = nullptr);

    static bool canHandle(storm::prism::Program const& program);
 
    virtual ModelType getModelType() const override;
    virtual bool isDeterministicModel() const override;
    virtual bool isDiscreteTimeModel() const override;
    virtual bool isPartiallyObservable() const override;
    virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
 
    virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
    bool evaluateBooleanExpressionInCurrentState(storm::expressions::Expression const&) const;
 
    virtual std::size_t getNumberOfRewardModels() const override;
    virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
    virtual std::map<std::string, storm::storage::PlayerIndex> getPlayerNameToIndexMap() const override;
 
    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 = {}) override;
 
    virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;
 
   private:
    using BaseValueType = typename NextStateGenerator<ValueType, StateType>::BaseValueType;
    void checkValid() const;

    PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options,
                            std::shared_ptr<ActionMask<ValueType, StateType>> const&, bool flag);

    CompressedState applyUpdate(CompressedState const& state, storm::prism::Update const& update);

    boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(
        uint_fast64_t const& actionIndex, CommandFilter const& commandFilter = CommandFilter::All);

    std::vector<Choice<ValueType>> getAsynchronousChoices(CompressedState const& state, StateToIdCallback stateToIdCallback,
                                                          CommandFilter const& commandFilter = CommandFilter::All);

    void addSynchronousChoices(std::vector<Choice<ValueType>>& choices, CompressedState const& state, StateToIdCallback stateToIdCallback,
                               CommandFilter const& commandFilter = CommandFilter::All);

    std::vector<Choice<ValueType>> getSelfLoopsForAllActions(CompressedState const& state, StateToIdCallback stateToIdCallback,
                                                             CommandFilter const& commandFilter = CommandFilter::All);

    virtual void extendStateInformation(storm::json<BaseValueType>& stateInfo) const override;

    storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const override;

    void generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position,
                                          std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator> const& iteratorList,
                                          storm::generator::Distribution<StateType, ValueType>& distribution, StateToIdCallback stateToIdCallback);
 
    bool isCommandPotentiallySynchronizing(prism::Command const& command) const;
 
    // The program used for the generation of next states.
    storm::prism::Program program;
 
    // The reward models that need to be considered.
    std::vector<std::reference_wrapper<storm::prism::RewardModel const>> rewardModels;
 
    // A flag that stores whether at least one of the selected reward models has state-action rewards.
    bool hasStateActionRewards;
 
    // Mappings from module/action indices to the programs players
    std::vector<storm::storage::PlayerIndex> moduleIndexToPlayerIndexMap;
    std::map<uint_fast64_t, storm::storage::PlayerIndex> actionIndexToPlayerIndexMap;
};
 
}  // namespace generator
}  // namespace storm