Model.h

Go to the documentation of this file.

#pragma once
 
#include <optional>
#include <unordered_map>
#include <vector>
 
#include "storm/models/Model.h"
#include "storm/models/ModelRepresentation.h"
#include "storm/models/sparse/ChoiceLabeling.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/sparse/ChoiceOrigins.h"
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/sparse/StateValuations.h"
#include "storm/utility/OsDetection.h"
 
namespace storm {
namespace storage {
class BitVector;
}
 
namespace models {
namespace sparse {
 
template<typename ValueType>
class StandardRewardModel;
 
template<class CValueType, class CRewardModelType = StandardRewardModel<CValueType>>
class Model : public storm::models::Model<CValueType> {
   public:
    typedef CValueType ValueType;
    typedef CRewardModelType RewardModelType;
    static const storm::models::ModelRepresentation Representation = ModelRepresentation::Sparse;
 
    Model(Model<ValueType, RewardModelType> const& other) = default;
    Model& operator=(Model<ValueType, RewardModelType> const& other) = default;
 
    Model(ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components);
    Model(ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components);
 
    virtual ~Model() = default;
 
    storm::storage::SparseMatrix<ValueType> getBackwardTransitions() const;
 
    virtual typename storm::storage::SparseMatrix<ValueType>::const_rows getRows(storm::storage::sparse::state_type state) const;
 
    virtual uint_fast64_t getNumberOfStates() const override;
 
    virtual uint_fast64_t getNumberOfTransitions() const override;
 
    virtual uint_fast64_t getNumberOfChoices() const override;
 
    storm::storage::BitVector const& getInitialStates() const;
 
    void setInitialStates(storm::storage::BitVector const& states);
 
    storm::storage::BitVector const& getStates(std::string const& label) const;
 
    bool hasLabel(std::string const& label) const;
 
    storm::storage::SparseMatrix<ValueType> const& getTransitionMatrix() const;
 
    storm::storage::SparseMatrix<ValueType>& getTransitionMatrix();
 
    std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
 
    std::unordered_map<std::string, RewardModelType>& getRewardModels();
 
    virtual bool hasRewardModel(std::string const& rewardModelName) const override;
 
    RewardModelType const& getRewardModel(std::string const& rewardModelName) const;
 
    RewardModelType& getRewardModel(std::string const& rewardModelName);
 
    RewardModelType const& getUniqueRewardModel() const;
 
    RewardModelType& getUniqueRewardModel();
 
    virtual bool hasUniqueRewardModel() const override;
 
    virtual std::string const& getUniqueRewardModelName() const override;
 
    bool hasRewardModel() const;
 
    uint_fast64_t getNumberOfRewardModels() const;
 
    void addRewardModel(std::string const& rewardModelName, RewardModelType const& rewModel);
 
    bool removeRewardModel(std::string const& rewardModelName);
 
    void restrictRewardModels(std::set<std::string> const& keptRewardModels);
 
    storm::models::sparse::StateLabeling const& getStateLabeling() const;
 
    storm::models::sparse::StateLabeling& getStateLabeling();
 
    bool hasChoiceLabeling() const;
 
    storm::models::sparse::ChoiceLabeling const& getChoiceLabeling() const;
 
    std::optional<storm::models::sparse::ChoiceLabeling> const& getOptionalChoiceLabeling() const;
 
    std::optional<storm::models::sparse::ChoiceLabeling>& getOptionalChoiceLabeling();
 
    bool hasStateValuations() const;
 
    storm::storage::sparse::StateValuations const& getStateValuations() const;
 
    std::optional<storm::storage::sparse::StateValuations> const& getOptionalStateValuations() const;
 
    std::optional<storm::storage::sparse::StateValuations>& getOptionalStateValuations();
 
    bool hasChoiceOrigins() const;
 
    std::shared_ptr<storm::storage::sparse::ChoiceOrigins> const& getChoiceOrigins() const;
 
    std::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>> const& getOptionalChoiceOrigins() const;
 
    std::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>>& getOptionalChoiceOrigins();
 
    virtual void printModelInformationToStream(std::ostream& out) const override;
 
    bool isSinkState(uint64_t sink) const;
 
    virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, bool includeLabeling = true,
                                  storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr,
                                  std::vector<ValueType> const* secondValue = nullptr, std::vector<uint64_t> const* stateColoring = nullptr,
                                  std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr,
                                  bool finalizeOutput = true) const;
 
    virtual void writeJsonToStream(std::ostream& outStream) const;
 
    std::set<std::string> getLabelsOfState(storm::storage::sparse::state_type state) const;
 
    virtual bool isSparseModel() const override;
 
    virtual bool supportsParameters() const override;
 
    virtual bool hasParameters() const override;
 
    virtual bool isExact() const override;
 
    virtual bool supportsUncertainty() const;
 
    virtual bool hasUncertainty() const;
 
    virtual std::size_t hash() const;
 
   protected:
    RewardModelType& rewardModel(std::string const& rewardModelName);
    void setTransitionMatrix(storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
 
    void setTransitionMatrix(storm::storage::SparseMatrix<ValueType>&& transitionMatrix);
 
    void printModelInformationHeaderToStream(std::ostream& out) const;
 
    void printModelInformationFooterToStream(std::ostream& out) const;
 
    void printRewardModelsInformationToStream(std::ostream& out) const;
 
    virtual std::string additionalDotStateInfo(uint64_t state) const;
 
   private:
    // Upon construction of a model, this function asserts that the specified components are valid
    void assertValidityOfComponents(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components) const;
 
    //  A matrix representing transition relation.
    storm::storage::SparseMatrix<ValueType> transitionMatrix;
 
    // The labeling of the states.
    storm::models::sparse::StateLabeling stateLabeling;
 
    // The reward models of the model.
    std::unordered_map<std::string, RewardModelType> rewardModels;
 
    // If set, a vector representing the labels of choices.
    std::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
 
    // if set, retrieves for each state the variable valuation that this state represents
    std::optional<storm::storage::sparse::StateValuations> stateValuations;
 
    // if set, gives information about where each choice originates w.r.t. the input model description
    std::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>> choiceOrigins;
};
 
std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
 
std::set<storm::RationalFunctionVariable> getRewardParameters(Model<storm::RationalFunction> const& model);
 
std::set<storm::RationalFunctionVariable> getRateParameters(Model<storm::RationalFunction> const& model);
 
std::set<storm::RationalFunctionVariable> getAllParameters(Model<storm::RationalFunction> const& model);
}  // namespace sparse
}  // namespace models
}  // namespace storm