TemplateEdge.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <vector>
 
#include "storm/storage/BoostTypes.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/jani/TemplateEdgeDestination.h"
 
namespace storm {
namespace jani {
class Model;
 
class TemplateEdge {
   public:
    TemplateEdge() = default;
    TemplateEdge(TemplateEdge const&) = default;
    TemplateEdge(storm::expressions::Expression const& guard);
    TemplateEdge(storm::expressions::Expression const& guard, OrderedAssignments const& assignments, std::vector<TemplateEdgeDestination> const& destinations);
 
    storm::expressions::Expression const& getGuard() const;
    void setGuard(storm::expressions::Expression const& newGuard);
 
    void addDestination(TemplateEdgeDestination const& destination);
 
    void finalize(Model const& containingModel);
 
    std::size_t getNumberOfDestinations() const;
    std::vector<TemplateEdgeDestination> const& getDestinations() const;
    std::vector<TemplateEdgeDestination>& getDestinations();
    TemplateEdgeDestination const& getDestination(uint64_t index) const;
 
    OrderedAssignments const& getAssignments() const;
    OrderedAssignments& getAssignments();
 
    bool addTransientAssignment(Assignment const& assignment, bool addToExisting = false);
 
    storm::storage::FlatSet<storm::expressions::Variable> const& getWrittenGlobalVariables() 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 liftTransientDestinationAssignments(int64_t maxLevel = 0);
 
    void pushAssignmentsToDestinations();
 
    bool usesVariablesInNonTransientAssignments(std::set<storm::expressions::Variable> const& variables) const;
 
    bool hasTransientEdgeDestinationAssignments() const;
 
    bool usesAssignmentLevels(bool onlyTransient = false) const;
 
    int64_t const& getLowestAssignmentLevel() const;
 
    int64_t const& getHighestAssignmentLevel() const;
 
    bool isLinear() const;
 
    bool hasEdgeDestinationAssignments() const;
 
    TemplateEdge simplifyIndexedAssignments(bool syncronized, VariableSet const& localVars) const;
 
   private:
    // The guard of the template edge.
    storm::expressions::Expression guard;
 
    // The destinations of the template edge.
    std::vector<TemplateEdgeDestination> destinations;
 
    OrderedAssignments assignments;
 
    int64_t lowestAssignmentLevel, highestAssignmentLevel;
 
    storm::storage::FlatSet<storm::expressions::Variable> writtenGlobalVariables;
};
 
}  // namespace jani
}  // namespace storm