Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
TemplateEdgeDestination.cpp
Go to the documentation of this file.
2
3namespace storm {
4namespace jani {
5
6TemplateEdgeDestination::TemplateEdgeDestination(OrderedAssignments const& assignments) : assignments(assignments) {
7 // Intentionally left empty.
8}
9
10TemplateEdgeDestination::TemplateEdgeDestination(Assignment const& assignment) : assignments(assignment) {
11 // Intentionally left empty.
12}
13
14TemplateEdgeDestination::TemplateEdgeDestination(std::vector<Assignment> const& assignments) : assignments(assignments) {
15 // Intentionally left empty.
16}
17
18void TemplateEdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution,
19 bool const substituteTranscendentalNumbers) {
20 assignments.substitute(substitution, substituteTranscendentalNumbers);
21}
22
23void TemplateEdgeDestination::changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) {
24 assignments.changeAssignmentVariables(remapping);
25}
26
28 return assignments;
29}
30
34
36 return assignments.remove(assignment);
37}
38
39void TemplateEdgeDestination::addAssignment(Assignment const& assignment, bool addToExisting) {
40 assignments.add(assignment, addToExisting);
41}
42
44 return assignments.contains(assignment);
45}
46
50
51bool TemplateEdgeDestination::usesAssignmentLevels(bool onlyTransient) const {
52 return assignments.hasMultipleLevels(onlyTransient);
53}
54
56 return assignments.areLinear();
57}
58
60 return !(assignments.empty());
61}
62
64 return TemplateEdgeDestination(assignments.simplifyLevels(syncronized, localVars));
65}
66} // namespace jani
67} // namespace storm
bool hasMultipleLevels(bool onlyTransient=false) const
Checks whether the assignments have several levels.
void substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution, bool const substituteTranscendentalNumbers)
Substitutes all variables in all expressions according to the given substitution.
void changeAssignmentVariables(std::map< Variable const *, std::reference_wrapper< Variable const > > const &remapping)
Changes all variables in assignments based on the given mapping.
bool empty(bool onlyTransient=false) const
Retrieves whether this set of assignments is empty.
OrderedAssignments simplifyLevels(bool synchronous, VariableSet const &localVars, bool first=true) const
Produces a new OrderedAssignments object with simplified leveling.
bool areLinear() const
Checks the assignments for linearity.
bool hasTransientAssignment() const
Retrieves whether the set of assignments has at least one transient assignment.
bool remove(Assignment const &assignment)
Removes the given assignment from this set of assignments.
bool add(Assignment const &assignment, bool addToExisting=false)
Adds the given assignment to the set of assignments.
bool contains(Assignment const &assignment) const
Retrieves whether the given assignment is contained in this set of assignments.
void substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution, bool const substituteTranscendentalNumbers)
Substitutes all variables in all expressions according to the given substitution.
bool hasAssignment(Assignment const &assignment) const
TemplateEdgeDestination simplifyIndexedAssignments(bool syncronized, VariableSet const &localVars) const
Simplify Indexed Assignments.
void changeAssignmentVariables(std::map< Variable const *, std::reference_wrapper< Variable const > > const &remapping)
Changes all variables in assignments based on the given mapping.
OrderedAssignments const & getOrderedAssignments() const
bool hasTransientAssignment() const
Retrieves whether this destination has transient assignments.
bool removeAssignment(Assignment const &assignment)
bool usesAssignmentLevels(bool onlyTransient=false) const
Retrieves whether the edge uses an assignment level other than zero.
bool isLinear() const
Checks the template edge destination for linearity.
void addAssignment(Assignment const &assignment, bool addToExisting=false)
bool hasAssignments() const
Checks whether the templ.
LabParser.cpp.
Definition cli.cpp:18