Location.h

Go to the documentation of this file.

#pragma once
 
#include <string>
 
#include "storm/storage/jani/OrderedAssignments.h"
 
namespace storm {
namespace jani {
 
class Location {
   public:
    Location(std::string const& name, std::vector<Assignment> const& transientAssignments = {});
 
    Location(std::string const& name, OrderedAssignments const& assignments);
    std::string const& getName() const;
 
    OrderedAssignments const& getAssignments() const;
 
    OrderedAssignments& getAssignments();
 
    void addTransientAssignment(storm::jani::Assignment const& assignment);
 
    bool hasTimeProgressInvariant() const;
 
    storm::expressions::Expression const& getTimeProgressInvariant() const;
 
    void setTimeProgressInvariant(storm::expressions::Expression const& expression);
 
    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 checkValid() const;
 
    bool isLinear() const;
 
   private:
    std::string name;
 
    OrderedAssignments assignments;
 
    // The location's time progress condition
    storm::expressions::Expression timeProgressInvariant;
};
 
}  // namespace jani
}  // namespace storm