Model.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
 
#include "Composition.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/storage/BoostTypes.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;
 
    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