Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | Friends | List of all members
storm::jani::OrderedAssignments Class Reference

#include <OrderedAssignments.h>

Public Member Functions

 OrderedAssignments (std::vector< Assignment > const &assignments=std::vector< Assignment >())
 Creates an ordered set of assignments.
 
 OrderedAssignments (Assignment const &assignment)
 
bool add (Assignment const &assignment, bool addToExisting=false)
 Adds the given assignment to the set of assignments.
 
bool remove (Assignment const &assignment)
 Removes the given assignment from this set of assignments.
 
bool hasMultipleLevels (bool onlyTransient=false) const
 Checks whether the assignments have several levels.
 
OrderedAssignments simplifyLevels (bool synchronous, VariableSet const &localVars, bool first=true) const
 Produces a new OrderedAssignments object with simplified leveling.
 
bool empty (bool onlyTransient=false) const
 Retrieves whether this set of assignments is empty.
 
void clear ()
 Removes all assignments from this set.
 
std::size_t getNumberOfAssignments () const
 Retrieves the total number of assignments.
 
int64_t getLowestLevel (bool onlyTransient=false) const
 Retrieves the lowest level among all assignments.
 
int64_t getHighestLevel (bool onlyTransient=false) const
 Retrieves the highest level among all assignments.
 
bool contains (Assignment const &assignment) const
 Retrieves whether the given assignment is contained in this set of assignments.
 
detail::ConstAssignments getAllAssignments () const
 Returns all assignments in this set of assignments.
 
detail::ConstAssignments getTransientAssignments () const
 Returns all transient assignments in this set of assignments.
 
detail::ConstAssignments getTransientAssignments (int64_t assignmentLevel) const
 Returns all transient assignments in this set of assignments.
 
detail::ConstAssignments getNonTransientAssignments () const
 Returns all non-transient assignments in this set of assignments.
 
detail::ConstAssignments getNonTransientAssignments (int64_t assignmentLevel) const
 Returns all non-transient assignments in this set of assignments.
 
bool hasTransientAssignment () const
 Retrieves whether the set of assignments has at least one transient assignment.
 
detail::Assignments::iterator begin ()
 Returns an iterator to the assignments.
 
detail::ConstAssignments::iterator begin () const
 Returns an iterator to the assignments.
 
detail::Assignments::iterator end ()
 Returns an iterator past the end of the assignments.
 
detail::ConstAssignments::iterator end () const
 Returns an iterator past the end of the 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.
 
void changeAssignmentVariables (std::map< Variable const *, std::reference_wrapper< Variable const > > const &remapping)
 Changes all variables in assignments based on the given mapping.
 
bool areLinear () const
 Checks the assignments for linearity.
 
OrderedAssignments clone () const
 
bool checkOrder () const
 Checks whether this ordered assignment is in the correct order.
 

Friends

std::ostream & operator<< (std::ostream &stream, OrderedAssignments const &assignments)
 

Detailed Description

Definition at line 17 of file OrderedAssignments.h.

Constructor & Destructor Documentation

◆ OrderedAssignments() [1/2]

storm::jani::OrderedAssignments::OrderedAssignments ( std::vector< Assignment > const &  assignments = std::vector<Assignment>())

Creates an ordered set of assignments.

Definition at line 10 of file OrderedAssignments.cpp.

◆ OrderedAssignments() [2/2]

storm::jani::OrderedAssignments::OrderedAssignments ( Assignment const &  assignment)
explicit

Definition at line 16 of file OrderedAssignments.cpp.

Member Function Documentation

◆ add()

bool storm::jani::OrderedAssignments::add ( Assignment const &  assignment,
bool  addToExisting = false 
)

Adds the given assignment to the set of assignments.

@addToExisting If true the value of the assigned expression is added to a (potentially) previous assignment to the variable. If false and there is already an assignment, an exception is thrown.

Returns
True iff the assignment was added.

Definition at line 28 of file OrderedAssignments.cpp.

◆ areLinear()

bool storm::jani::OrderedAssignments::areLinear ( ) const

Checks the assignments for linearity.

Definition at line 293 of file OrderedAssignments.cpp.

◆ begin() [1/2]

detail::Assignments::iterator storm::jani::OrderedAssignments::begin ( )

Returns an iterator to the assignments.

Definition at line 225 of file OrderedAssignments.cpp.

◆ begin() [2/2]

detail::ConstAssignments::iterator storm::jani::OrderedAssignments::begin ( ) const

Returns an iterator to the assignments.

Definition at line 229 of file OrderedAssignments.cpp.

◆ changeAssignmentVariables()

void storm::jani::OrderedAssignments::changeAssignmentVariables ( std::map< Variable const *, std::reference_wrapper< Variable const > > const &  remapping)

Changes all variables in assignments based on the given mapping.

Definition at line 248 of file OrderedAssignments.cpp.

◆ checkOrder()

bool storm::jani::OrderedAssignments::checkOrder ( ) const

Checks whether this ordered assignment is in the correct order.

Definition at line 301 of file OrderedAssignments.cpp.

◆ clear()

void storm::jani::OrderedAssignments::clear ( )

Removes all assignments from this set.

Definition at line 100 of file OrderedAssignments.cpp.

◆ clone()

OrderedAssignments storm::jani::OrderedAssignments::clone ( ) const

Definition at line 20 of file OrderedAssignments.cpp.

◆ contains()

bool storm::jani::OrderedAssignments::contains ( Assignment const &  assignment) const

Retrieves whether the given assignment is contained in this set of assignments.

Definition at line 122 of file OrderedAssignments.cpp.

◆ empty()

bool storm::jani::OrderedAssignments::empty ( bool  onlyTransient = false) const

Retrieves whether this set of assignments is empty.

Definition at line 93 of file OrderedAssignments.cpp.

◆ end() [1/2]

detail::Assignments::iterator storm::jani::OrderedAssignments::end ( )

Returns an iterator past the end of the assignments.

Definition at line 233 of file OrderedAssignments.cpp.

◆ end() [2/2]

detail::ConstAssignments::iterator storm::jani::OrderedAssignments::end ( ) const

Returns an iterator past the end of the assignments.

Definition at line 237 of file OrderedAssignments.cpp.

◆ getAllAssignments()

detail::ConstAssignments storm::jani::OrderedAssignments::getAllAssignments ( ) const

Returns all assignments in this set of assignments.

Definition at line 188 of file OrderedAssignments.cpp.

◆ getHighestLevel()

int64_t storm::jani::OrderedAssignments::getHighestLevel ( bool  onlyTransient = false) const

Retrieves the highest level among all assignments.

Note that this may only be called if there is at least one assignment.

Definition at line 116 of file OrderedAssignments.cpp.

◆ getLowestLevel()

int64_t storm::jani::OrderedAssignments::getLowestLevel ( bool  onlyTransient = false) const

Retrieves the lowest level among all assignments.

Note that this may only be called if there is at least one assignment.

Definition at line 110 of file OrderedAssignments.cpp.

◆ getNonTransientAssignments() [1/2]

detail::ConstAssignments storm::jani::OrderedAssignments::getNonTransientAssignments ( ) const

Returns all non-transient assignments in this set of assignments.

Definition at line 196 of file OrderedAssignments.cpp.

◆ getNonTransientAssignments() [2/2]

detail::ConstAssignments storm::jani::OrderedAssignments::getNonTransientAssignments ( int64_t  assignmentLevel) const

Returns all non-transient assignments in this set of assignments.

Definition at line 215 of file OrderedAssignments.cpp.

◆ getNumberOfAssignments()

std::size_t storm::jani::OrderedAssignments::getNumberOfAssignments ( ) const

Retrieves the total number of assignments.

Definition at line 106 of file OrderedAssignments.cpp.

◆ getTransientAssignments() [1/2]

detail::ConstAssignments storm::jani::OrderedAssignments::getTransientAssignments ( ) const

Returns all transient assignments in this set of assignments.

Definition at line 192 of file OrderedAssignments.cpp.

◆ getTransientAssignments() [2/2]

detail::ConstAssignments storm::jani::OrderedAssignments::getTransientAssignments ( int64_t  assignmentLevel) const

Returns all transient assignments in this set of assignments.

Definition at line 209 of file OrderedAssignments.cpp.

◆ hasMultipleLevels()

bool storm::jani::OrderedAssignments::hasMultipleLevels ( bool  onlyTransient = false) const

Checks whether the assignments have several levels.

Returns
True if more than one level occurs in the assignment set.

Definition at line 86 of file OrderedAssignments.cpp.

◆ hasTransientAssignment()

bool storm::jani::OrderedAssignments::hasTransientAssignment ( ) const

Retrieves whether the set of assignments has at least one transient assignment.

Definition at line 221 of file OrderedAssignments.cpp.

◆ remove()

bool storm::jani::OrderedAssignments::remove ( Assignment const &  assignment)

Removes the given assignment from this set of assignments.

Returns
True if the assignment was found and removed.

Definition at line 60 of file OrderedAssignments.cpp.

◆ simplifyLevels()

OrderedAssignments storm::jani::OrderedAssignments::simplifyLevels ( bool  synchronous,
VariableSet const &  localVars,
bool  first = true 
) const

Produces a new OrderedAssignments object with simplified leveling.

Parameters
synchronous
localVars
Returns

Definition at line 131 of file OrderedAssignments.cpp.

◆ substitute()

void storm::jani::OrderedAssignments::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.

Definition at line 241 of file OrderedAssignments.cpp.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<< ( std::ostream &  stream,
OrderedAssignments const &  assignments 
)
friend

Definition at line 310 of file OrderedAssignments.cpp.

The documentation for this class was generated from the following files: