Model.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
 
#include "Composition.h"
#include "storm/storage/BoostTypes.h"
#include "storm/storage/jani/Action.h"
#include "storm/storage/jani/Automaton.h"
#include "storm/storage/jani/Constant.h"
#include "storm/storage/jani/Edge.h"
#include "storm/storage/jani/FunctionDefinition.h"
#include "storm/storage/jani/Location.h"
#include "storm/storage/jani/ModelFeatures.h"
#include "storm/storage/jani/ModelType.h"
#include "storm/storage/jani/TemplateEdge.h"
#include "storm/storage/jani/VariableSet.h"
#include "storm/utility/solver.h"
 
namespace storm {
namespace expressions {
class ExpressionManager;
}
 
namespace jani {
 
class Variable;
class Automaton;
class Exporter;
class SynchronizationVector;
struct ArrayEliminatorData;
class Property;
struct InformationObject;
 
class Model {
   public:
    friend class Exporter;

    Model();

    Model(std::string const& name, ModelType const& modelType, uint64_t version = 1,
          boost::optional<std::shared_ptr<storm::expressions::ExpressionManager>> const& expressionManager = boost::none);

    Model(Model const& other);

    Model& operator=(Model const& other);
 
    Model(Model&& other);
    Model& operator=(Model&& other);

    storm::expressions::ExpressionManager& getManager() const;

    uint64_t getJaniVersion() const;

    ModelType const& getModelType() const;

    void setModelType(ModelType const&);

    ModelFeatures const& getModelFeatures() const;

    ModelFeatures& getModelFeatures();

    std::string const& getName() const;

    void setName(std::string const& newName);

    Model flattenComposition(
        std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::SmtSolverFactory>()) const;

    bool hasAction(std::string const& name) const;

    uint64_t getActionIndex(std::string const& name) const;

    std::unordered_map<std::string, uint64_t> const& getActionToIndexMap() const;

    uint64_t addAction(Action const& action);

    Action const& getAction(uint64_t index) const;

    std::vector<Action> const& getActions() const;

    std::map<uint64_t, std::string> getActionIndexToNameMap() const;

    storm::storage::FlatSet<uint64_t> const& getNonsilentActionIndices() const;

    void addConstant(Constant const& constant);

    bool hasConstant(std::string const& name) const;

    void removeConstant(std::string const& name);

    std::vector<Constant> const& getConstants() const;

    std::vector<Constant>& getConstants();

    Constant const& getConstant(std::string const& name) const;

    Variable const& addVariable(Variable const& variable);

    VariableSet& getGlobalVariables();

    VariableSet const& getGlobalVariables() const;

    std::set<storm::expressions::Variable> getAllExpressionVariables(bool includeLocationExpressionVariables = false) const;

    std::set<storm::expressions::Variable> getAllLocationExpressionVariables() const;

    bool hasGlobalVariable(std::string const& name) const;

    Variable const& getGlobalVariable(std::string const& name) const;

    bool hasNonGlobalTransientVariable() const;

    FunctionDefinition const& addFunctionDefinition(FunctionDefinition const& functionDefinition);

    std::unordered_map<std::string, FunctionDefinition> const& getGlobalFunctionDefinitions() const;

    std::unordered_map<std::string, FunctionDefinition>& getGlobalFunctionDefinitions();

    storm::expressions::ExpressionManager& getExpressionManager() const;

    bool hasNonTrivialRewardExpression() const;

    bool isNonTrivialRewardModelExpression(std::string const& identifier) const;

    bool addNonTrivialRewardExpression(std::string const& identifier, storm::expressions::Expression const& rewardExpression);

    storm::expressions::Expression getRewardModelExpression(std::string const& identifier) const;

    std::vector<std::pair<std::string, storm::expressions::Expression>> getAllRewardModelExpressions() const;

    std::unordered_map<std::string, storm::expressions::Expression> const& getNonTrivialRewardExpressions() const;

    std::unordered_map<std::string, storm::expressions::Expression>& getNonTrivialRewardExpressions();

    uint64_t addAutomaton(Automaton const& automaton);

    std::vector<Automaton>& getAutomata();

    std::vector<Automaton> const& getAutomata() const;

    void replaceAutomaton(uint64_t index, Automaton const& newAutomaton);

    bool hasAutomaton(std::string const& name) const;
    Automaton& getAutomaton(std::string const& name);

    Automaton& getAutomaton(uint64_t index);

    Automaton const& getAutomaton(uint64_t index) const;

    Automaton const& getAutomaton(std::string const& name) const;

    uint64_t getAutomatonIndex(std::string const& name) const;

    std::size_t getNumberOfAutomata() const;

    std::size_t getNumberOfEdges() const;

    std::size_t getTotalNumberOfNonTransientVariables() const;

    InformationObject getModelInformation() const;

    void setSystemComposition(std::shared_ptr<Composition> const& composition);

    void setStandardSystemComposition();

    std::shared_ptr<Composition> getStandardSystemComposition() const;

    Composition const& getSystemComposition() const;

    void simplifyComposition();

    std::set<std::string> getActionNames(bool includeSilent = true) const;

    Model defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;

    bool hasUndefinedConstants() const;

    std::vector<std::reference_wrapper<Constant const>> getUndefinedConstants() const;

    Model& replaceUnassignedVariablesWithConstants();

    Model& substituteConstantsInPlace(bool const substituteTranscendentalNumbers);

    Model substituteConstants() const;

    Model preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;

    Model preprocess(std::string const& constantDefinitionString = "") const;

    std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;

    void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution, bool const substituteTranscendentalNumbers);

    void substituteFunctions();
    void substituteFunctions(std::vector<Property>& properties);

    Model substituteConstantsFunctionsTranscendentals() const;

    bool containsArrayVariables() const;

    ArrayEliminatorData eliminateArrays(bool keepNonTrivialArrayAccess = false);

    void eliminateArrays(std::vector<Property>& properties);

    ModelFeatures restrictToFeatures(ModelFeatures const& modelFeatures);

    ModelFeatures restrictToFeatures(ModelFeatures const& modelFeatures, std::vector<Property>& properties);

    bool hasInitialStatesRestriction() const;

    bool hasNonTrivialInitialStates() const;

    void setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction);

    storm::expressions::Expression const& getInitialStatesRestriction() const;

    storm::expressions::Expression getInitialStatesExpression() const;

    bool hasTrivialInitialStatesExpression() const;

    storm::expressions::Expression getInitialStatesExpression(std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& automata) const;

    bool isDeterministicModel() const;

    bool isDiscreteTimeModel() const;

    std::vector<storm::expressions::Expression> getAllRangeExpressions(
        std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& automata = {}) const;

    bool hasStandardComposition() const;

    bool hasStandardCompliantComposition() const;

    void finalize();

    void checkValid() const;

    storm::expressions::Expression getLabelExpression(Variable const& transientVariable,
                                                      std::vector<std::reference_wrapper<Automaton const>> const& automata) const;

    storm::expressions::Expression getLabelExpression(Variable const& transientVariable) const;

    bool undefinedConstantsAreGraphPreserving() const;

    void liftTransientEdgeDestinationAssignments(int64_t maxLevel = 0);

    bool hasTransientEdgeDestinationAssignments() const;

    bool usesAssignmentLevels(bool onlyTransient = false) const;

    bool isLinear() const;
 
    void makeStandardJaniCompliant();
 
    // Pushes all edge assignments to their destination
    void pushEdgeAssignmentsToDestinations();

    bool reusesActionsInComposition() const;

    static uint64_t encodeAutomatonAndEdgeIndices(uint64_t automatonIndex, uint64_t edgeIndex);
    static std::pair<uint64_t, uint64_t> decodeAutomatonAndEdgeIndices(uint64_t index);

    Model restrictEdges(storm::storage::FlatSet<uint_fast64_t> const& automataAndEdgeIndices) const;
 
    void writeDotToStream(std::ostream& outStream = std::cout) const;

    static const std::string SILENT_ACTION_NAME;

    static const uint64_t SILENT_ACTION_INDEX;
 
   private:
    Model createModelFromAutomaton(Automaton const& automaton) const;

    std::string name;

    ModelType modelType;

    uint64_t version;

    ModelFeatures modelFeatures;

    std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;

    std::vector<Action> actions;

    std::unordered_map<std::string, uint64_t> actionToIndex;

    std::unordered_map<std::string, storm::expressions::Expression> nonTrivialRewardModels;

    storm::storage::FlatSet<uint64_t> nonsilentActionIndices;

    std::vector<Constant> constants;

    std::unordered_map<std::string, uint64_t> constantToIndex;

    VariableSet globalVariables;

    std::unordered_map<std::string, FunctionDefinition> globalFunctions;

    std::vector<Automaton> automata;

    std::unordered_map<std::string, size_t> automatonToIndex;

    std::shared_ptr<Composition> composition;
 
    // The expression restricting the legal initial values of the global variables.
    storm::expressions::Expression initialStatesRestriction;
};
 
std::ostream& operator<<(std::ostream& out, Model const& model);
}  // namespace jani
}  // namespace storm