Model.h

Go to the documentation of this file.

#ifndef STORM_MODELS_SYMBOLIC_MODEL_H_
#define STORM_MODELS_SYMBOLIC_MODEL_H_
 
#include <memory>
#include <set>
#include <unordered_map>
 
#include "storm/models/Model.h"
#include "storm/models/ModelRepresentation.h"
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/utility/OsDetection.h"
 
#include "storm-config.h"
#include "storm/adapters/RationalFunctionForward.h"
 
namespace storm {
namespace dd {
 
template<storm::dd::DdType Type>
class Dd;
 
template<storm::dd::DdType Type>
class DdManager;
 
}  // namespace dd
 
namespace adapters {
template<storm::dd::DdType Type, typename ValueType>
class AddExpressionAdapter;
}
 
namespace models {
namespace symbolic {
 
template<storm::dd::DdType Type, typename ValueType>
class StandardRewardModel;
 
template<storm::dd::DdType Type, typename CValueType = double>
class Model : public storm::models::Model<CValueType> {
   public:
    typedef CValueType ValueType;
 
    static const storm::dd::DdType DdType = Type;
    typedef StandardRewardModel<Type, ValueType> RewardModelType;
 
    static const storm::models::ModelRepresentation Representation = GetModelRepresentation<DdType>::representation;
 
    Model(Model<Type, ValueType> const& other) = default;
    Model& operator=(Model<Type, ValueType> const& other) = default;
 
#ifndef WINDOWS
    Model(Model<Type, ValueType>&& other) = default;
    Model& operator=(Model<Type, ValueType>&& other) = default;
#endif
 
    Model(storm::models::ModelType const& modelType, std::shared_ptr<storm::dd::DdManager<Type>> manager, storm::dd::Bdd<Type> reachableStates,
          storm::dd::Bdd<Type> initialStates, storm::dd::Bdd<Type> deadlockStates, storm::dd::Add<Type, ValueType> transitionMatrix,
          std::set<storm::expressions::Variable> const& rowVariables,
          std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
          std::set<storm::expressions::Variable> const& columnVariables,
          std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
          std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
          std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
 
    Model(storm::models::ModelType const& modelType, std::shared_ptr<storm::dd::DdManager<Type>> manager, storm::dd::Bdd<Type> reachableStates,
          storm::dd::Bdd<Type> initialStates, storm::dd::Bdd<Type> deadlockStates, storm::dd::Add<Type, ValueType> transitionMatrix,
          std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables,
          std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
          std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
          std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
 
    virtual uint_fast64_t getNumberOfStates() const override;
 
    virtual uint_fast64_t getNumberOfTransitions() const override;
 
    virtual uint_fast64_t getNumberOfChoices() const override;
 
    storm::dd::DdManager<Type>& getManager() const;
 
    std::shared_ptr<storm::dd::DdManager<Type>> const& getManagerAsSharedPointer() const;
 
    storm::dd::Bdd<Type> const& getReachableStates() const;
 
    storm::dd::Bdd<Type> const& getInitialStates() const;
 
    /*
     * Retrieves the deadlock states of the model.
     */
    storm::dd::Bdd<Type> const& getDeadlockStates() const;
 
    virtual storm::dd::Bdd<Type> getStates(std::string const& label) const;
 
    virtual storm::expressions::Expression getExpression(std::string const& label) const;
 
    virtual storm::dd::Bdd<Type> getStates(storm::expressions::Expression const& expression) const;
 
    virtual bool hasLabel(std::string const& label) const;
 
    storm::dd::Add<Type, ValueType> const& getTransitionMatrix() const;
 
    storm::dd::Add<Type, ValueType>& getTransitionMatrix();
 
    virtual storm::dd::Bdd<Type> getQualitativeTransitionMatrix(bool keepNondeterminism = true) const;
 
    std::set<storm::expressions::Variable> const& getRowVariables() const;
 
    std::set<storm::expressions::Variable> const& getColumnVariables() const;
 
    std::set<storm::expressions::Variable> getRowAndNondeterminismVariables() const;
 
    std::set<storm::expressions::Variable> getColumnAndNondeterminismVariables() const;
 
    virtual std::set<storm::expressions::Variable> const& getNondeterminismVariables() const;
 
    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& getRowColumnMetaVariablePairs() const;
 
    storm::dd::Add<Type, ValueType> getRowColumnIdentity() const;
 
    virtual bool hasRewardModel(std::string const& rewardModelName) const override;
 
    RewardModelType const& getRewardModel(std::string const& rewardModelName) const;
 
    RewardModelType const& getUniqueRewardModel() const;
 
    virtual std::string const& getUniqueRewardModelName() const override;
 
    RewardModelType& getUniqueRewardModel();
 
    virtual bool hasUniqueRewardModel() const override;
 
    bool hasRewardModel() const;
 
    std::unordered_map<std::string, RewardModelType>& getRewardModels();
    std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
 
    uint_fast64_t getNumberOfRewardModels() const;
 
    virtual void printModelInformationToStream(std::ostream& out) const override;
 
    virtual bool isSymbolicModel() const override;
 
    virtual bool supportsParameters() const override;
 
    virtual bool hasParameters() const override;
 
    std::vector<std::string> getLabels() const;
 
    void addParameters(std::set<storm::RationalFunctionVariable> const& parameters);
 
    std::set<storm::RationalFunctionVariable> const& getParameters() const;
 
    template<typename NewValueType>
    typename std::enable_if<!std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type toValueType() const;
 
    template<typename NewValueType>
    typename std::enable_if<std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type toValueType() const;
 
    void writeDotToFile(std::string const& filename) const;
 
   protected:
    void setTransitionMatrix(storm::dd::Add<Type, ValueType> const& transitionMatrix);
 
    std::map<std::string, storm::expressions::Expression> const& getLabelToExpressionMap() const;
 
    std::map<std::string, storm::dd::Bdd<Type>> const& getLabelToBddMap() const;
 
    void printModelInformationHeaderToStream(std::ostream& out) const;
 
    void printModelInformationFooterToStream(std::ostream& out) const;
 
    void printRewardModelsInformationToStream(std::ostream& out) const;
 
    virtual void printDdVariableInformationToStream(std::ostream& out) const;
 
   protected:
    std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> const& getRowExpressionAdapter() const;
 
   private:
    // The manager responsible for the decision diagrams.
    std::shared_ptr<storm::dd::DdManager<Type>> manager;
 
    // A vector representing the reachable states of the model.
    storm::dd::Bdd<Type> reachableStates;
 
   protected:
    // A matrix representing transition relation.
    storm::dd::Add<Type, ValueType> transitionMatrix;
 
   private:
    // The meta variables used to encode the rows of the transition matrix.
    std::set<storm::expressions::Variable> rowVariables;
 
    // An adapter that can translate expressions to DDs over the row meta variables.
    std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter;
 
    // The meta variables used to encode the columns of the transition matrix.
    std::set<storm::expressions::Variable> columnVariables;
 
    // A vector holding all pairs of row and column meta variable pairs. This is used to swap the variables
    // in the DDs from row to column variables and vice versa.
    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
 
    // A mapping from labels to expressions defining them.
    std::map<std::string, storm::expressions::Expression> labelToExpressionMap;
 
    // A mapping from labels to BDDs characterizing the labeled states.
    std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap;
 
    // The reward models associated with the model.
    std::unordered_map<std::string, RewardModelType> rewardModels;
 
    // The parameters. Only meaningful for models over rational functions.
    std::set<storm::RationalFunctionVariable> parameters;
 
    // An empty variable set that can be used when references to non-existing sets need to be returned.
    std::set<storm::expressions::Variable> emptyVariableSet;
};
 
}  // namespace symbolic
}  // namespace models
}  // namespace storm
 
#endif /* STORM_MODELS_SYMBOLIC_MODEL_H_ */