storm::pars::analysis Namespace Reference

Classes
struct	RegionWitness
	A point of a parameter region, mapping the variables to exact values. More...
struct	RegionCheckResult
class	RegionConstraintChecker
	Checks whether the constraints collected for a parametric model hold over an entire rectangular region. More...

Typedefs
using	RationalFunctionRegion = storm::storage::ParameterRegion<storm::RationalFunction>
using	CoefficientType = RationalFunctionRegion::CoefficientType
using	ConstraintVerdict = storm::solver::SmtSolver::CheckResult
	Tri-state outcome of a check: Sat means the constraint holds on the whole region, Unsat means it is violated somewhere (a witness is available), and Unknown means neither could be established.

Enumerations
enum class	GraphPreservationStatus { None , WellDefined , GraphPreserving , Unknown }
	Describes to what extent a set of regions is known to be well-defined and to preserve the graph structure of the parametric model. More...

Functions
bool	isGraphPreserving (GraphPreservationStatus status)
	Returns whether the given status guarantees that the graph structure of the model is preserved.
std::ostream &	operator<< (std::ostream &stream, GraphPreservationStatus status)
std::ostream &	operator<< (std::ostream &out, RegionWitness const &witness)
	Prints the witness as a comma-separated list of assignments, e.g.

Typedef Documentation

CoefficientType

using storm::pars::analysis::CoefficientType = RationalFunctionRegion::CoefficientType

Definition at line 17 of file RegionConstraintChecker.h.

ConstraintVerdict

using storm::pars::analysis::ConstraintVerdict = storm::solver::SmtSolver::CheckResult

Tri-state outcome of a check: Sat means the constraint holds on the whole region, Unsat means it is violated somewhere (a witness is available), and Unknown means neither could be established.

Definition at line 23 of file RegionConstraintChecker.h.

RationalFunctionRegion

using storm::pars::analysis::RationalFunctionRegion = storm::storage::ParameterRegion<storm::RationalFunction>

Definition at line 16 of file RegionConstraintChecker.h.

Enumeration Type Documentation

GraphPreservationStatus

enum class storm::pars::analysis::GraphPreservationStatus

strong

Describes to what extent a set of regions is known to be well-defined and to preserve the graph structure of the parametric model.

Enumerator
None	No guarantee. The graph structure of the model may change within a region. Only engines that can handle non-graph-preserving regions (currently robust parameter lifting) may be used in this case.
WellDefined	The regions are known to be well-defined, i.e. all probabilities lie in [0, 1] and all denominators are non-zero, but it is not known whether they preserve the graph structure of the model.
GraphPreserving	The regions are known (or assumed) to preserve the graph structure of the model. This implies that they are well-defined, as a model that is not well-formed cannot be graph-preserving.
Unknown	It could not be established whether the regions are well-defined or preserve the graph structure of the model.

Definition at line 11 of file GraphPreservationStatus.h.

Function Documentation

isGraphPreserving()

bool storm::pars::analysis::isGraphPreserving ( GraphPreservationStatus status )

inline

Returns whether the given status guarantees that the graph structure of the model is preserved.

Definition at line 37 of file GraphPreservationStatus.h.

operator<<() [1/2]

std::ostream & storm::pars::analysis::operator<<	(	std::ostream &	out,
		RegionWitness const &	witness )

Prints the witness as a comma-separated list of assignments, e.g.

x = 1/2, y = 1.

Definition at line 126 of file RegionConstraintChecker.cpp.

operator<<() [2/2]

std::ostream & storm::pars::analysis::operator<< ( std::ostream & stream, GraphPreservationStatus status )

inline

Definition at line 41 of file GraphPreservationStatus.h.