Class to collect constraints on parametric Markov chains. More...

#include <GraphConditions.h>

Public Types
using	ConstraintSet = std::vector<storm::expressions::Expression>
	The type of the collected constraints.

Public Member Functions
	ConstraintCollector (storm::models::sparse::Model< storm::RationalFunction > const &model)
	Constructs a constraint collector for the given model.
ConstraintSet const &	getWellformedConstraints () const
	Returns the set of wellformed-ness constraints.
ConstraintSet const &	getGraphPreservingConstraints () const
	Returns the set of graph-preserving constraints.
std::set< storm::RationalFunctionVariable > const &	getVariables () const
	Returns the set of variables in the model.
void	operator() (storm::models::sparse::Model< storm::RationalFunction > const &model)
	Constructs the constraints for the given model by calling the process method.

Detailed Description

Class to collect constraints on parametric Markov chains.

The collected constraints are stored as expressions in a Storm expression manager. In particular, this avoids a dependency on a dedicated logical formula representation.

Structurally equal constraints are deduplicated. Note that Storm's expressions hash and compare by identity of their underlying node, so a container keyed by expressions themselves would not deduplicate them. We therefore bucket the collected constraints by their structural hash (storm::expressions::HashVisitor) and compare the candidates in a bucket with Expression::isSyntacticallyEqual, which allows looking up an existing constraint without scanning all of the collected ones. The constraints themselves are kept in the order in which they are discovered, which is determined by the traversal of the model.

Definition at line 34 of file GraphConditions.h.

Member Typedef Documentation

◆ ConstraintSet

using storm::analysis::ConstraintCollector::ConstraintSet = std::vector<storm::expressions::Expression>

The type of the collected constraints.

Definition at line 39 of file GraphConditions.h.

Constructor & Destructor Documentation

◆ ConstraintCollector()

storm::analysis::ConstraintCollector::ConstraintCollector ( storm::models::sparse::Model< storm::RationalFunction > const & model )

explicit

Constructs a constraint collector for the given model.

The constraints are built and ready for retrieval after the construction.

Parameters

model The model for which to create the constraints.

Definition at line 27 of file GraphConditions.cpp.

Member Function Documentation

◆ getGraphPreservingConstraints()

ConstraintCollector::ConstraintSet const & storm::analysis::ConstraintCollector::getGraphPreservingConstraints ( ) const

Returns the set of graph-preserving constraints.

Returns: The set of graph-preserving constraints, keyed by their string representation.

Definition at line 36 of file GraphConditions.cpp.

◆ getVariables()

std::set< storm::RationalFunctionVariable > const & storm::analysis::ConstraintCollector::getVariables ( ) const

Returns the set of variables in the model.

Returns

Definition at line 40 of file GraphConditions.cpp.

◆ getWellformedConstraints()

ConstraintCollector::ConstraintSet const & storm::analysis::ConstraintCollector::getWellformedConstraints ( ) const

Returns the set of wellformed-ness constraints.

Returns: The set of wellformed-ness constraints, keyed by their string representation.

Definition at line 32 of file GraphConditions.cpp.

◆ operator()()

void storm::analysis::ConstraintCollector::operator() ( storm::models::sparse::Model< storm::RationalFunction > const & model )

Constructs the constraints for the given model by calling the process method.