JaniNextStateGenerator.h

Go to the documentation of this file.

#pragma once
 
#include "storm/generator/NextStateGenerator.h"
#include "storm/generator/TransientVariableInformation.h"
 
#include "storm/storage/BoostTypes.h"
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/OrderedAssignments.h"
#include "storm/storage/jani/eliminator/ArrayEliminator.h"
 
namespace storm {
namespace jani {
class Edge;
class EdgeDestination;
}  // namespace jani
 
namespace generator {
template<typename StateType, typename ValueType>
class Distribution;
 
template<typename ValueType, typename StateType = uint32_t>
class JaniNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
   public:
    static_assert(!storm::IsIntervalType<ValueType>, "JaniNextStateGenerator does not support interval types.");
    typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
    typedef storm::storage::FlatSet<uint_fast64_t> EdgeIndexSet;
    enum class EdgeFilter { All, WithRate, WithoutRate };
 
    JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions());

    static storm::jani::ModelFeatures getSupportedJaniFeatures();

    static bool canHandle(storm::jani::Model const& model);
 
    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 storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const override;
 
    virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;

    virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex,
                                   storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const override;
 
    virtual std::size_t getNumberOfRewardModels() const override;
    virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) 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;

    virtual void unpackTransientVariableValuesIntoEvaluator(CompressedState const& state,
                                                            storm::expressions::ExpressionEvaluator<ValueType>& evaluator) const override;
 
   private:
    uint64_t getLocation(CompressedState const& state, LocationVariableInformation const& locationVariable) const;

    void setLocation(CompressedState& state, LocationVariableInformation const& locationVariable, uint64_t locationIndex) const;

    std::vector<uint64_t> getLocations(CompressedState const& state) const;

    JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag);

    void applyUpdate(CompressedState& state, storm::jani::EdgeDestination const& destination,
                     storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentlevel,
                     storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator);

    void applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments,
                              storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) const;

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

    TransientVariableValuation<ValueType> getTransientVariableValuationAtLocations(std::vector<uint64_t> const& locations,
                                                                                   storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) const;

    std::vector<Choice<ValueType>> getActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback,
                                                    EdgeFilter const& edgeFilter = EdgeFilter::All);

    Choice<ValueType> expandNonSynchronizingEdge(storm::jani::Edge const& edge, uint64_t outputActionIndex, uint64_t automatonIndex,
                                                 CompressedState const& state, StateToIdCallback stateToIdCallback);
 
    typedef std::vector<std::pair<uint64_t, storm::jani::Edge const*>> EdgeSetWithIndices;
    typedef std::unordered_map<uint64_t, EdgeSetWithIndices> LocationsAndEdges;
    typedef std::vector<std::pair<uint64_t, LocationsAndEdges>> AutomataAndEdges;
    typedef std::pair<boost::optional<uint64_t>, AutomataAndEdges> OutputAndEdges;
 
    typedef std::pair<uint64_t, EdgeSetWithIndices> AutomatonAndEdgeSet;
    typedef std::vector<AutomatonAndEdgeSet> AutomataEdgeSets;
 
    void expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state,
                                            StateToIdCallback stateToIdCallback, std::vector<Choice<ValueType>>& newChoices);
    void generateSynchronizedDistribution(storm::storage::BitVector const& state, AutomataEdgeSets const& edgeCombination,
                                          std::vector<EdgeSetWithIndices::const_iterator> const& iteratorList,
                                          storm::generator::Distribution<StateType, ValueType>& distribution, std::vector<ValueType>& stateActionRewards,
                                          EdgeIndexSet& edgeIndices, StateToIdCallback stateToIdCallback);

    void checkGlobalVariableWritesValid(AutomataEdgeSets const& enabledEdges) const;

    std::vector<ValueType> evaluateRewardExpressions() const;

    void addEvaluatedRewardExpressions(std::vector<ValueType>& rewards, ValueType const& factor) const;

    void buildRewardModelInformation();

    void createSynchronizationInformation();

    void checkValid() const;

    storm::jani::Model model;

    std::vector<std::reference_wrapper<storm::jani::Automaton const>> parallelAutomata;

    std::vector<OutputAndEdges> edges;

    std::vector<std::pair<std::string, storm::expressions::Expression>> rewardExpressions;

    std::vector<storm::builder::RewardModelInformation> rewardModelInformation;

    bool hasStateActionRewards;

    bool evaluateRewardExpressionsAtEdges;

    bool evaluateRewardExpressionsAtDestinations;

    storm::jani::ArrayEliminatorData arrayEliminatorData;

    TransientVariableInformation<ValueType> transientVariableInformation;
};
 
}  // namespace generator
}  // namespace storm