Automaton.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <string>
#include <unordered_map>
#include <vector>
 
#include "storm/storage/BoostTypes.h"
#include "storm/storage/jani/EdgeContainer.h"
#include "storm/storage/jani/FunctionDefinition.h"
#include "storm/storage/jani/TemplateEdgeContainer.h"
#include "storm/storage/jani/VariableSet.h"
 
namespace storm {
namespace jani {
 
class Automaton;
class Edge;
class TemplateEdge;
class Location;
 
class Model;
 
class Automaton {
   public:
    friend class detail::Edges;
    friend class detail::ConstEdges;
 
    typedef detail::Edges Edges;
    typedef detail::ConstEdges ConstEdges;
 
    Automaton(std::string const& name, storm::expressions::Variable const& locationExpressionVariable);
 
    Automaton(Automaton const& other) = default;
    Automaton& operator=(Automaton const& other) = default;
    Automaton(Automaton&& other) = default;
    Automaton& operator=(Automaton&& other) = default;
 
    Automaton clone(storm::expressions::ExpressionManager& manager, std::string const& nameOfClone, std::string const& variablePrefix) const;
 
    std::string const& getName() const;
 
    Variable const& addVariable(Variable const& variable);
 
    VariableSet& getVariables();
 
    VariableSet const& getVariables() const;
 
    bool hasVariable(std::string const& name) const;
 
    std::set<storm::expressions::Variable> getAllExpressionVariables() const;
 
    bool hasTransientVariable() const;
 
    FunctionDefinition const& addFunctionDefinition(FunctionDefinition const& functionDefinition);
 
    std::unordered_map<std::string, FunctionDefinition> const& getFunctionDefinitions() const;
 
    std::unordered_map<std::string, FunctionDefinition>& getFunctionDefinitions();
 
    bool hasLocation(std::string const& name) const;
 
    uint64_t getLocationIndex(std::string const& name) const;
 
    std::vector<Location> const& getLocations() const;
 
    std::vector<Location>& getLocations();
 
    Location const& getLocation(uint64_t index) const;
 
    Location& getLocation(uint64_t index);
 
    uint64_t addLocation(Location const& location);
 
    void addInitialLocation(std::string const& name);
 
    void addInitialLocation(uint64_t index);
 
    std::set<uint64_t> const& getInitialLocationIndices() const;
 
    std::map<uint64_t, std::string> buildIdToLocationNameMap() const;
 
    storm::expressions::Variable const& getLocationExpressionVariable() const;
 
    Edge const& getEdge(uint64_t index) const;
 
    Edges getEdgesFromLocation(std::string const& name);
 
    Edges getEdgesFromLocation(uint64_t index);
 
    ConstEdges getEdgesFromLocation(std::string const& name) const;
 
    ConstEdges getEdgesFromLocation(uint64_t index) const;
 
    Edges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex);
 
    ConstEdges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const;
 
    EdgeContainer const& getEdgeContainer() const;
 
    EdgeContainer& getEdgeContainer();
 
    void registerTemplateEdge(std::shared_ptr<TemplateEdge> const&);
 
    void addEdge(Edge const& edge);
 
    bool validate() const;
 
    std::vector<Edge>& getEdges();
 
    std::vector<Edge> const& getEdges() const;
 
    std::set<uint64_t> getActionIndices() const;
 
    uint64_t getNumberOfLocations() const;
 
    uint64_t getNumberOfEdges() const;
 
    bool hasRestrictedInitialStates() const;
 
    bool hasInitialStatesRestriction() const;
 
    bool hasNonTrivialInitialStates() const;
 
    storm::expressions::Expression const& getInitialStatesRestriction() const;
 
    void setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction);
 
    storm::expressions::Expression getInitialStatesExpression() const;
 
    bool hasTrivialInitialStatesExpression() const;
 
    bool hasEdgeLabeledWithActionIndex(uint64_t actionIndex) const;
 
    std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
 
    void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution, bool const substituteTranscendentalNumbers);
 
    void changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping);
 
    void finalize(Model const& containingModel);
 
    std::set<uint64_t> getUsedActionIndices() const;
 
    bool containsVariablesOnlyInProbabilitiesOrTransientAssignments(std::set<storm::expressions::Variable> const& variables) const;
 
    void pushEdgeAssignmentsToDestinations();
 
    void pushTransientRealLocationAssignmentsToEdges();
 
    bool hasTransientEdgeDestinationAssignments() const;
 
    void liftTransientEdgeDestinationAssignments(int64_t maxLevel = 0);
 
    bool usesAssignmentLevels(bool onlyTransient = false) const;
 
    void simplifyIndexedAssignments();
 
    bool isLinear() const;
 
    void writeDotToStream(std::ostream& outStream, std::vector<std::string> const& actionNames) const;
 
    void restrictToEdges(storm::storage::FlatSet<uint_fast64_t> const& edgeIndices);
 
   private:
    std::string name;
 
    storm::expressions::Variable locationExpressionVariable;
 
    VariableSet variables;
 
    std::unordered_map<std::string, FunctionDefinition> functionDefinitions;
 
    std::vector<Location> locations;
 
    std::unordered_map<std::string, uint64_t> locationToIndex;
 
    EdgeContainer edges;
 
    std::vector<uint64_t> locationToStartingIndex;
 
    std::set<uint64_t> initialLocationIndices;
 
    storm::expressions::Expression initialStatesRestriction;
 
    std::set<uint64_t> actionIndices;
};
 
}  // namespace jani
}  // namespace storm