Model.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <optional>
#include <unordered_map>
#include <vector>
 
#include "storm/adapters/IntervalForward.h"
#include "storm/adapters/RationalFunctionForward.h"
#include "storm/adapters/RationalNumberForward.h"
#include "storm/models/Model.h"
#include "storm/models/ModelRepresentation.h"
#include "storm/models/sparse/ChoiceLabeling.h"
#include "storm/models/sparse/ModelForward.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/valuations/Valuations.h"
 
namespace storm {
namespace storage {
class BitVector;
}
 
namespace models {
namespace sparse {

template<class CValueType, class CRewardModelType>
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);
    Model& operator=(Model<ValueType, RewardModelType> const& other);

    Model(ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components);
    Model(ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components);
 
    virtual ~Model() = default;

    ValueType const& getStochasticTolerance() const;

    void setStochasticTolerance(ValueType const& tolerance);

    storm::storage::SparseMatrix<ValueType> getBackwardTransitions() 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::Valuations const& getStateValuations() const;

    std::optional<storm::storage::sparse::Valuations> const& getOptionalStateValuations() const;

    std::optional<storm::storage::sparse::Valuations>& 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 override;

    virtual bool hasUncertainty() const;
 
    virtual std::size_t hash() const;
 
   protected:
    RewardModelType& rewardModel(std::string const& rewardModelName);

    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::Valuations> 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;
 
    // The tolerance up to which the model components are considered valid. Stored as a heap-allocated value to avoid
    // requiring the value type to be complete at the point of instantiation of the class template.
    std::unique_ptr<ValueType> stochasticTolerance;
};

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);
 
// Must precede the extern template below, which would otherwise be the point of instantiation.
template<>
void Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>::writeJsonToStream(std::ostream& outStream) const;
 
// Instantiated in Model.cpp; prevents hidden consumers from duplicating the vtable/RTTI.
extern template class Model<double>;
extern template class Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
extern template class Model<storm::RationalNumber>;
extern template class Model<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalInterval>>;
extern template class Model<storm::Interval>;
extern template class Model<storm::RationalInterval>;
extern template class Model<storm::RationalFunction>;
 
}  // namespace sparse
}  // namespace models
}  // namespace storm