Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Update.h
Go to the documentation of this file.
1#ifndef STORM_STORAGE_PRISM_UPDATE_H_
2#define STORM_STORAGE_PRISM_UPDATE_H_
3
4#include <vector>
5
8
9namespace storm {
10namespace prism {
11class Update : public LocatedInformation {
12 public:
13 using ExpressionPair = std::pair<storm::expressions::Expression, storm::expressions::Expression>;
14
24 Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments,
25 std::string const& filename = "", uint_fast64_t lineNumber = 0);
36 Update(uint_fast64_t globalIndex, ExpressionPair const& likelihoodExpressionInterval, std::vector<storm::prism::Assignment> const& assignments,
37 std::string const& filename = "", uint_fast64_t lineNumber = 0);
38
39 // Create default implementations of constructors/assignment.
40 Update() = default;
41 Update(Update const& other) = default;
42 Update& operator=(Update const& other) = default;
43 Update(Update&& other) = default;
44 Update& operator=(Update&& other) = default;
45
46 bool isLikelihoodInterval() const;
47
55
63
69 std::size_t getNumberOfAssignments() const;
70
76 std::vector<storm::prism::Assignment> const& getAssignments() const;
77
83 std::vector<storm::prism::Assignment>& getAssignments();
84
90 storm::prism::Assignment const& getAssignment(std::string const& variableName) const;
91
97 std::map<storm::expressions::Variable, storm::expressions::Expression> getAsVariableToExpressionMap() const;
98
104 uint_fast64_t getGlobalIndex() const;
105
112 Update substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
113
120
122
126 Update simplify() const;
127
128 friend std::ostream& operator<<(std::ostream& stream, Update const& assignment);
129
130 private:
134 void createAssignmentMapping();
135
136 // Expressions specifying the likelihood of taking this update.
137 // Either both expressions are initialized (representing an interval likelihood [first, second] for interval models)
138 // or only the first one is initialized (standard, non-interval interpretation)
139 ExpressionPair likelihoodExpressions;
140
141 // The assignments of this update.
142 std::vector<storm::prism::Assignment> assignments;
143
144 // A mapping from variable names to their assignments.
145 std::map<std::string, uint_fast64_t> variableToAssignmentIndexMap;
146
147 // The global index of the update.
148 uint_fast64_t globalIndex;
149};
150} // namespace prism
151} // namespace storm
152
153#endif /* STORM_STORAGE_PRISM_UPDATE_H_ */
Update substituteNonStandardPredicates() const
Definition Update.cpp:133
std::size_t getNumberOfAssignments() const
Retrieves the number of assignments associated with this update.
Definition Update.cpp:71
bool isLikelihoodInterval() const
Definition Update.cpp:57
Update & operator=(Update const &other)=default
Update substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all identifiers in the update according to the given map.
Definition Update.cpp:111
Update simplify() const
Simplifies the update in various ways (also removes identity assignments)
Definition Update.cpp:166
std::pair< storm::expressions::Expression, storm::expressions::Expression > ExpressionPair
Definition Update.h:13
std::map< storm::expressions::Variable, storm::expressions::Expression > getAsVariableToExpressionMap() const
Creates a mapping representation of this update.
Definition Update.cpp:90
Update(Update &&other)=default
Update(Update const &other)=default
storm::prism::Assignment const & getAssignment(std::string const &variableName) const
Retrieves a reference to the assignment for the variable with the given name.
Definition Update.cpp:83
uint_fast64_t getGlobalIndex() const
Retrieves the global index of the update, that is, a unique index over all modules.
Definition Update.cpp:100
Update & operator=(Update &&other)=default
Update removeIdentityAssignments() const
Removes all assignments which do not change the variable.
Definition Update.cpp:155
friend std::ostream & operator<<(std::ostream &stream, Update const &assignment)
Definition Update.cpp:184
ExpressionPair const & getLikelihoodExpressionInterval() const
Retrieves the two expression for the interval likelihood of this update.
Definition Update.cpp:66
std::vector< storm::prism::Assignment > const & getAssignments() const
Retrieves a reference to the map of variable names to their respective assignments.
Definition Update.cpp:75
storm::expressions::Expression const & getLikelihoodExpression() const
Retrieves the expression for the likelihood of this update.
Definition Update.cpp:61
LabParser.cpp.