#include <Order.h>

Classes
struct	Node
	Nodes of the Reachability Order. More...

Public Types
enum	NodeComparison { UNKNOWN , BELOW , ABOVE , SAME }
	Constants for comparison of nodes/states. More...

Public Member Functions
	Order (storm::storage::BitVector topStates, storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates, storage::Decomposition< storage::StronglyConnectedComponent > sccsSorted, std::vector< uint_fast64_t > statesSorted)
	Constructs an order with the given top and bottom states.

	Order (uint_fast64_t top, uint_fast64_t bottom, uint_fast64_t numberOfStates, storage::Decomposition< storage::StronglyConnectedComponent > sccsSorted, std::vector< uint_fast64_t > statesSorted)
	Constructs an order with the given top state and bottom state.

	Order ()
	Constructs a new Order.

void	add (uint_fast64_t state)
	Adds state between the top and bottom node of the order.

void	addAbove (uint_fast64_t state, Node *node)
	Adds a node with the given state above the given node.

void	addBelow (uint_fast64_t state, Node *node)
	Adds a node with the given state below the given node.

void	addBetween (uint_fast64_t state, Node node1, Node node2)
	Adds a node with the given state below node1 and above node2.

void	addBetween (uint_fast64_t state, uint_fast64_t above, uint_fast64_t below)
	Adds a node with the given state between the nodes of below and above.

void	addRelationNodes (storm::analysis::Order::Node above, storm::analysis::Order::Node below, bool allowMerge=false)
	Adds a new relation between two nodes to the order.

void	addRelation (uint_fast64_t above, uint_fast64_t below, bool allowMerge=false)
	Adds a new relation between two states to the order.

void	addToNode (uint_fast64_t state, Node *node)
	Adds state to the states of the given node.

bool	mergeNodes (Node node1, Node node2)
	Merges node2 into node1.

bool	merge (uint_fast64_t var1, uint_fast64_t var2)
	Merges node of var2 into node of var1.

Order::NodeComparison	compare (uint_fast64_t state1, uint_fast64_t state2, NodeComparison hypothesis=UNKNOWN)
	Compares the level of the nodes of the states.

Order::NodeComparison	compareFast (uint_fast64_t state1, uint_fast64_t state2, NodeComparison hypothesis=UNKNOWN) const

NodeComparison	compare (Node node1, Node node2, NodeComparison hypothesis=UNKNOWN)
	Compares the level of the two nodes.

NodeComparison	compareFast (Node node1, Node node2, NodeComparison hypothesis=UNKNOWN) const

bool	contains (uint_fast64_t state) const
	Check if state is already contained in order.

Node *	getBottom () const
	Retrieves the bottom node of the order.

bool	getDoneBuilding () const
	Returns true if done building the order.

uint_fast64_t	getNextDoneState (uint_fast64_t state) const
	Returns the next done state of the order, returns the number of state if end of done states is reached.

uint_fast64_t	getNumberOfDoneStates () const

Node *	getNode (uint_fast64_t state) const
	Retrieves the pointer to a Node at which the state occurs.

std::vector< Node * >	getNodes () const
	Returns the vector with the nodes of the order.

std::vector< uint_fast64_t > &	getStatesSorted ()

Node *	getTop () const
	Retrieves the top node of the order.

uint_fast64_t	getNumberOfAddedStates () const
	Returns the number of added states.

uint_fast64_t	getNumberOfStates () const
	Returns the number of possible states in the order.

bool	isBottomState (uint_fast64_t) const
	Checks if the given state is a bottom state.

bool	isTopState (uint_fast64_t) const
	Checks if the given state is a top state.

bool	isOnlyBottomTopOrder () const
	Returns if the order only consists of bottom and top states (so no in-between nodes).

std::vector< uint_fast64_t >	sortStates (std::vector< uint_fast64_t > *states)
	Sorts the given states if possible.

std::pair< bool, bool >	allAboveBelow (std::vector< uint_fast64_t > const states, uint_fast64_t state)

std::pair< std::pair< uint_fast64_t, uint_fast64_t >, std::vector< uint_fast64_t > >	sortStatesForForward (uint_fast64_t currentState, std::vector< uint_fast64_t > const &successors)
	Sorts the given states if possible.

std::pair< std::pair< uint_fast64_t, uint_fast64_t >, std::vector< uint_fast64_t > >	sortStatesUnorderedPair (const std::vector< uint_fast64_t > *states)
	Sorts the given states if possible.

std::vector< uint_fast64_t >	sortStates (storm::storage::BitVector *states)
	Sorts the given states if possible.

bool	isTrivial (uint_fast64_t state)

std::pair< uint_fast64_t, bool >	getNextStateNumber ()

bool	existsNextState ()

bool	existsStateToHandle ()

std::pair< uint_fast64_t, bool >	getStateToHandle ()

void	addStateToHandle (uint_fast64_t state)

void	addStateSorted (uint_fast64_t state)

void	setDoneBuilding (bool done=true)
	If the order is fully built, this can be set to true.

void	toDotOutput () const
	Prints the dot output to normal STORM_PRINT.

void	dotOutputToFile (std::ofstream &dotOutfile) const
	Writes dotoutput to the given file.

std::shared_ptr< Order >	copy () const
	Creates a copy of the calling Order.

void	setDoneState (uint_fast64_t sccNumber)

bool	isInvalid () const

Protected Member Functions
storage::Decomposition< storage::StronglyConnectedComponent >	getDecomposition () const

Detailed Description

Definition at line 13 of file Order.h.

Member Enumeration Documentation

◆ NodeComparison

enum storm::analysis::Order::NodeComparison

Constants for comparison of nodes/states.

Enumerator
UNKNOWN
BELOW
ABOVE
SAME

Definition at line 18 of file Order.h.

Constructor & Destructor Documentation

◆ Order() [1/3]

storm::analysis::Order::Order	(	storm::storage::BitVector *	topStates,
		storm::storage::BitVector *	bottomStates,
		uint_fast64_t	numberOfStates,
		storage::Decomposition< storage::StronglyConnectedComponent >	sccsSorted,
		std::vector< uint_fast64_t >	statesSorted
	)

Constructs an order with the given top and bottom states.

Parameters

topStates	A Bitvector with the top states of the resulting order.
bottomStates	A Bitvector with the bottom states of the resulting order.
numberOfStates	Maximum number of states in order.
statesSorted	Pointer to a vector which contains the states which still need to added to the order.

Definition at line 9 of file Order.cpp.

◆ Order() [2/3]

storm::analysis::Order::Order	(	uint_fast64_t	top,
		uint_fast64_t	bottom,
		uint_fast64_t	numberOfStates,
		storage::Decomposition< storage::StronglyConnectedComponent >	sccsSorted,
		std::vector< uint_fast64_t >	statesSorted
	)

Constructs an order with the given top state and bottom state.

Parameters

top	The top state of the resulting order.
bottom	The bottom state of the resulting order.
numberOfStates	Maximum number of states in order.
statesSorted	Pointer to a vector which contains the states which still need to added to the order.

Definition at line 36 of file Order.cpp.

◆ Order() [3/3]

storm::analysis::Order::Order ( )

Constructs a new Order.

Definition at line 61 of file Order.cpp.

Member Function Documentation

◆ add()

void storm::analysis::Order::add ( uint_fast64_t state )

Adds state between the top and bottom node of the order.

Parameters

state The given state.

Definition at line 67 of file Order.cpp.

◆ addAbove()

void storm::analysis::Order::addAbove	(	uint_fast64_t	state,
		Node *	node
	)

Adds a node with the given state above the given node.

Parameters

state	The state which is added.
node	The pointer to the node above which the state is added, should not be nullptr.

Definition at line 73 of file Order.cpp.

◆ addBelow()

void storm::analysis::Order::addBelow	(	uint_fast64_t	state,
		Node *	node
	)

Adds a node with the given state below the given node.

Parameters

state	The state which is added.
node	The pointer to the node below which the state is added, should not be nullptr.

Definition at line 93 of file Order.cpp.

◆ addBetween() [1/2]

void storm::analysis::Order::addBetween	(	uint_fast64_t	state,
		Node *	node1,
		Node *	node2
	)

Adds a node with the given state below node1 and above node2.

Parameters

state	The given state.
node1	The pointer to the node below which a new node (with state) is added.
node2	The pointer to the node above which a new node (with state) is added.

Definition at line 113 of file Order.cpp.

◆ addBetween() [2/2]

void storm::analysis::Order::addBetween	(	uint_fast64_t	state,
		uint_fast64_t	above,
		uint_fast64_t	below
	)

Adds a node with the given state between the nodes of below and above.

Result: below -> state -> above

Parameters

state	The given state.
above	The state number of the state below which a new node (with state) is added.
below	The state number of the state above which a new node (with state) is added.

Definition at line 142 of file Order.cpp.

◆ addRelation()

void storm::analysis::Order::addRelation	(	uint_fast64_t	above,
		uint_fast64_t	below,
		bool	allowMerge = `false`
	)

Adds a new relation between two states to the order.

Parameters

above	The state closest to the top Node of the Order.
below	The state closest to the bottom Node of the Order.

Definition at line 150 of file Order.cpp.

◆ addRelationNodes()

void storm::analysis::Order::addRelationNodes	(	storm::analysis::Order::Node *	above,
		storm::analysis::Order::Node *	below,
		bool	allowMerge = `false`
	)

Adds a new relation between two nodes to the order.

Parameters

above	The node closest to the top Node of the Order.
below	The node closest to the bottom Node of the Order.

Definition at line 155 of file Order.cpp.

◆ addStateSorted()

void storm::analysis::Order::addStateSorted ( uint_fast64_t state )

Definition at line 782 of file Order.cpp.

◆ addStateToHandle()

void storm::analysis::Order::addStateToHandle ( uint_fast64_t state )

Definition at line 776 of file Order.cpp.

◆ addToNode()

void storm::analysis::Order::addToNode	(	uint_fast64_t	state,
		Node *	node
	)

Adds state to the states of the given node.

Parameters

state	The state which is added.
node	The pointer to the node to which state is added, should not be nullptr.

Definition at line 173 of file Order.cpp.

◆ allAboveBelow()

std::pair< bool, bool > storm::analysis::Order::allAboveBelow	(	std::vector< uint_fast64_t > const	states,
		uint_fast64_t	state
	)

Definition at line 786 of file Order.cpp.

◆ compare() [1/2]

Order::NodeComparison storm::analysis::Order::compare	(	Node *	node1,
		Node *	node2,
		NodeComparison	hypothesis = `UNKNOWN`
	)

Compares the level of the two nodes.

Parameters

node1	The first node.
node2	The second node.

Returns: SAME if the nodes are on the same level; ABOVE if node1 is closer to top than node2; BELOW if node2 is closer to top than node1; UNKNOWN if it is unclear from the structure of the order how the nodes relate.

Definition at line 267 of file Order.cpp.

◆ compare() [2/2]

Order::NodeComparison storm::analysis::Order::compare	(	uint_fast64_t	state1,
		uint_fast64_t	state2,
		NodeComparison	hypothesis = `UNKNOWN`
	)

Compares the level of the nodes of the states.

Behaviour unknown when one or more of the states does not occur at any Node in the Order.

Parameters

State1	the first state.
State2	the second state.

Returns: SAME if the nodes are on the same level; ABOVE if the node of the first state is closer to top than the node of the second state; BELOW if the node of the second state is closer to top than the node of the first state; UNKNOWN if it is unclear from the structure of the order how the nodes relate.

Definition at line 237 of file Order.cpp.

◆ compareFast() [1/2]

Order::NodeComparison storm::analysis::Order::compareFast	(	Node *	node1,
		Node *	node2,
		NodeComparison	hypothesis = `UNKNOWN`
	)		const

Definition at line 246 of file Order.cpp.

◆ compareFast() [2/2]

Order::NodeComparison storm::analysis::Order::compareFast	(	uint_fast64_t	state1,
		uint_fast64_t	state2,
		NodeComparison	hypothesis = `UNKNOWN`
	)		const

Definition at line 241 of file Order.cpp.

◆ contains()

bool storm::analysis::Order::contains ( uint_fast64_t state ) const

Check if state is already contained in order.

Definition at line 289 of file Order.cpp.

◆ copy()

std::shared_ptr< Order > storm::analysis::Order::copy ( ) const

Creates a copy of the calling Order.

Returns: Pointer to the copy.

Definition at line 510 of file Order.cpp.

◆ dotOutputToFile()

void storm::analysis::Order::dotOutputToFile ( std::ofstream & dotOutfile ) const

Writes dotoutput to the given file.

Parameters

dotOutfile

Definition at line 603 of file Order.cpp.

◆ existsNextState()

bool storm::analysis::Order::existsNextState ( )

Definition at line 743 of file Order.cpp.

◆ existsStateToHandle()

bool storm::analysis::Order::existsStateToHandle ( )

Definition at line 769 of file Order.cpp.

◆ getBottom()

Order::Node * storm::analysis::Order::getBottom ( ) const

Retrieves the bottom node of the order.

Returns: The bottom node.

Definition at line 293 of file Order.cpp.

◆ getDecomposition()

storage::Decomposition< storage::StronglyConnectedComponent > storm::analysis::Order::getDecomposition ( ) const

protected

◆ getDoneBuilding()

bool storm::analysis::Order::getDoneBuilding ( ) const

Returns true if done building the order.

Definition at line 297 of file Order.cpp.

◆ getNextDoneState()

uint_fast64_t storm::analysis::Order::getNextDoneState ( uint_fast64_t state ) const

Returns the next done state of the order, returns the number of state if end of done states is reached.

Definition at line 302 of file Order.cpp.

◆ getNextStateNumber()

std::pair< uint_fast64_t, bool > storm::analysis::Order::getNextStateNumber ( )

Definition at line 751 of file Order.cpp.

◆ getNode()

Order::Node * storm::analysis::Order::getNode ( uint_fast64_t state ) const

Retrieves the pointer to a Node at which the state occurs.

Parameters

state The number of the state.

Returns: The pointer to the node of the state, nullptr if the node does not exist.

Definition at line 306 of file Order.cpp.

◆ getNodes()

std::vector< Order::Node * > storm::analysis::Order::getNodes ( ) const

Returns the vector with the nodes of the order.

Each index in the vector refers to a state. When the state is not yet added at a node, it will contain the nullptr.

Returns: The vector with nodes of the order.

Definition at line 311 of file Order.cpp.

◆ getNumberOfAddedStates()

uint_fast64_t storm::analysis::Order::getNumberOfAddedStates ( ) const

Returns the number of added states.

Definition at line 323 of file Order.cpp.

◆ getNumberOfDoneStates()

uint_fast64_t storm::analysis::Order::getNumberOfDoneStates ( ) const

Definition at line 797 of file Order.cpp.

◆ getNumberOfStates()

uint_fast64_t storm::analysis::Order::getNumberOfStates ( ) const

Returns the number of possible states in the order.

Definition at line 327 of file Order.cpp.

◆ getStatesSorted()

std::vector< uint_fast64_t > & storm::analysis::Order::getStatesSorted ( )

Definition at line 315 of file Order.cpp.

◆ getStateToHandle()

std::pair< uint_fast64_t, bool > storm::analysis::Order::getStateToHandle ( )

Definition at line 762 of file Order.cpp.

◆ getTop()

Order::Node * storm::analysis::Order::getTop ( ) const

Retrieves the top node of the order.

Returns: The top node.

Definition at line 319 of file Order.cpp.

◆ isBottomState()

bool storm::analysis::Order::isBottomState ( uint_fast64_t state ) const

Checks if the given state is a bottom state.

Definition at line 331 of file Order.cpp.

◆ isInvalid()

bool storm::analysis::Order::isInvalid ( ) const

Definition at line 801 of file Order.cpp.

◆ isOnlyBottomTopOrder()

bool storm::analysis::Order::isOnlyBottomTopOrder ( ) const

Returns if the order only consists of bottom and top states (so no in-between nodes).

Definition at line 341 of file Order.cpp.

◆ isTopState()

bool storm::analysis::Order::isTopState ( uint_fast64_t state ) const

Checks if the given state is a top state.

Definition at line 336 of file Order.cpp.

◆ isTrivial()

bool storm::analysis::Order::isTrivial ( uint_fast64_t state )

Definition at line 747 of file Order.cpp.

◆ merge()

bool storm::analysis::Order::merge	(	uint_fast64_t	var1,
		uint_fast64_t	var2
	)

Merges node of var2 into node of var1.

Returns: false when merging leads to invalid order

Definition at line 231 of file Order.cpp.

◆ mergeNodes()

bool storm::analysis::Order::mergeNodes	(	Node *	node1,
		Node *	node2
	)

Merges node2 into node1.

Returns: false when merging leads to invalid order

Definition at line 192 of file Order.cpp.

◆ setDoneBuilding()

void storm::analysis::Order::setDoneBuilding ( bool done = true )

If the order is fully built, this can be set to true.

◆ setDoneState()

void storm::analysis::Order::setDoneState ( uint_fast64_t sccNumber )

Definition at line 555 of file Order.cpp.

◆ sortStates() [1/2]

std::vector< uint_fast64_t > storm::analysis::Order::sortStates ( std::vector< uint_fast64_t > * states )

Sorts the given states if possible.

Parameters

states Vector of the states to be sorted.

Returns: Vector with states sorted, length equals number of states to sort. If states cannot be sorted, last state of the vector will always equal the length of the BitVector.

Definition at line 345 of file Order.cpp.

◆ sortStates() [2/2]

std::vector< uint_fast64_t > storm::analysis::Order::sortStates ( storm::storage::BitVector * states )

Sorts the given states if possible.

Parameters

states Bitvector of the states to be sorted.

Returns: vector with states sorted, length equals number of states to sort. If states cannot be sorted, last state of the vector will always equal the length of the BitVector.

Definition at line 471 of file Order.cpp.

◆ sortStatesForForward()

std::pair< std::pair< uint_fast64_t, uint_fast64_t >, std::vector< uint_fast64_t > > storm::analysis::Order::sortStatesForForward	(	uint_fast64_t	currentState,
		std::vector< uint_fast64_t > const &	successors
	)

Sorts the given states if possible.

Parameters

states Vector of the states to be sorted.

Returns: s1, s2, vector if s1 == numberOfSTates, all states could be sorted including current if s1 < numberOfStates && s2 == numberOfStates, all states excluding s1 could be sorted, forward reasonging can be continued else assumption is needed

Definition at line 383 of file Order.cpp.

◆ sortStatesUnorderedPair()

std::pair< std::pair< uint_fast64_t, uint_fast64_t >, std::vector< uint_fast64_t > > storm::analysis::Order::sortStatesUnorderedPair ( const std::vector< uint_fast64_t > * states )

Sorts the given states if possible.

Parameters

states Vector of the states to be sorted.

Returns: pair of unsortabe states, vector with states sorted (so far). If all states could be sorted, both values of the pair are numberOfStates and the vectors length will equal the number of states to sort.

Definition at line 436 of file Order.cpp.

◆ toDotOutput()

void storm::analysis::Order::toDotOutput ( ) const

Prints the dot output to normal STORM_PRINT.

Definition at line 561 of file Order.cpp.

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

src/storm-pars/analysis/Order.h
src/storm-pars/analysis/Order.cpp

Classes

Public Types

Public Member Functions

Protected Member Functions

Detailed Description

Member Enumeration Documentation

◆ NodeComparison

Constructor & Destructor Documentation

◆ Order() [1/3]

◆ Order() [2/3]

◆ Order() [3/3]

Member Function Documentation

◆ add()

◆ addAbove()

◆ addBelow()

◆ addBetween() [1/2]

◆ addBetween() [2/2]

◆ addRelation()

◆ addRelationNodes()

◆ addStateSorted()

◆ addStateToHandle()

◆ addToNode()

◆ allAboveBelow()

◆ compare() [1/2]

◆ compare() [2/2]

◆ compareFast() [1/2]

◆ compareFast() [2/2]

◆ contains()

◆ copy()

◆ dotOutputToFile()

◆ existsNextState()

◆ existsStateToHandle()

◆ getBottom()

◆ getDecomposition()

◆ getDoneBuilding()

◆ getNextDoneState()

◆ getNextStateNumber()

◆ getNode()

◆ getNodes()

◆ getNumberOfAddedStates()

◆ getNumberOfDoneStates()

◆ getNumberOfStates()

◆ getStatesSorted()

◆ getStateToHandle()

◆ getTop()

◆ isBottomState()

◆ isInvalid()

◆ isOnlyBottomTopOrder()

◆ isTopState()

◆ isTrivial()

◆ merge()

◆ mergeNodes()

◆ setDoneBuilding()

◆ setDoneState()

◆ sortStates() [1/2]

◆ sortStates() [2/2]

◆ sortStatesForForward()

◆ sortStatesUnorderedPair()

◆ toDotOutput()