1#ifndef STORM_STORAGE_PRISM_UPDATE_H_
2#define STORM_STORAGE_PRISM_UPDATE_H_
13 using ExpressionPair = std::pair<storm::expressions::Expression, storm::expressions::Expression>;
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);
76 std::vector<storm::prism::Assignment>
const&
getAssignments()
const;
112 Update substitute(std::map<storm::expressions::Variable, storm::expressions::Expression>
const& substitution)
const;
128 friend std::ostream&
operator<<(std::ostream& stream,
Update const& assignment);
134 void createAssignmentMapping();
142 std::vector<storm::prism::Assignment> assignments;
145 std::map<std::string, uint_fast64_t> variableToAssignmentIndexMap;
148 uint_fast64_t globalIndex;
Update substituteNonStandardPredicates() const
std::size_t getNumberOfAssignments() const
Retrieves the number of assignments associated with this update.
bool isLikelihoodInterval() const
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.
Update simplify() const
Simplifies the update in various ways (also removes identity assignments)
std::pair< storm::expressions::Expression, storm::expressions::Expression > ExpressionPair
std::map< storm::expressions::Variable, storm::expressions::Expression > getAsVariableToExpressionMap() const
Creates a mapping representation of this update.
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.
uint_fast64_t getGlobalIndex() const
Retrieves the global index of the update, that is, a unique index over all modules.
Update & operator=(Update &&other)=default
Update removeIdentityAssignments() const
Removes all assignments which do not change the variable.
friend std::ostream & operator<<(std::ostream &stream, Update const &assignment)
ExpressionPair const & getLikelihoodExpressionInterval() const
Retrieves the two expression for the interval likelihood of this update.
std::vector< storm::prism::Assignment > const & getAssignments() const
Retrieves a reference to the map of variable names to their respective assignments.
storm::expressions::Expression const & getLikelihoodExpression() const
Retrieves the expression for the likelihood of this update.