storm::modelchecker Namespace Reference

Namespaces
namespace	exploration_detail
namespace	helper
namespace	internal
namespace	lexicographic
namespace	multiobjective
namespace	region
namespace	utility

Classes
class	AbstractModelChecker
class	CheckResult
class	CheckTask
class	ExplicitModelCheckerHint
	This class contains information that might accelerate the model checking process. More...
class	ExplicitParetoCurveCheckResult
class	ExplicitQualitativeCheckResult
class	ExplicitQuantitativeCheckResult
class	HybridCtmcCslModelChecker
class	HybridDtmcPrctlModelChecker
class	HybridMarkovAutomatonCslModelChecker
class	HybridMdpPrctlModelChecker
class	HybridQuantitativeCheckResult
class	LexicographicCheckResult
class	ModelCheckerHint
	This class contains information that might accelerate the model checking process. More...
class	ParetoCurveCheckResult
class	QualitativeCheckResult
class	QuantitativeCheckResult
struct	RegionBound
class	RegionCheckResult
class	RegionModelChecker
class	RegionRefinementCheckResult
class	SparseCtmcCslModelChecker
class	SparseCtmcInstantiationModelChecker
	Class to efficiently check a formula on a parametric model with different parameter instantiations. More...
class	SparseDtmcEliminationModelChecker
class	SparseDtmcInstantiationModelChecker
	Class to efficiently check a formula on a parametric model with different parameter instantiations. More...
class	SparseDtmcParameterLiftingModelChecker
class	SparseDtmcPrctlModelChecker
class	SparseExplorationModelChecker
class	SparseInstantiationModelChecker
	Class to efficiently check a formula on a parametric model with different parameter instantiations. More...
class	SparseMarkovAutomatonCslModelChecker
class	SparseMdpInstantiationModelChecker
	Class to efficiently check a formula on a parametric model with different parameter instantiations. More...
class	SparseMdpParameterLiftingModelChecker
class	SparseMdpPrctlModelChecker
class	SparseParameterLiftingModelChecker
	Class to approximatively check a formula on a parametric model for all parameter valuations within a region It is assumed that all considered valuations are graph-preserving and well defined, i.e.,. More...
class	SparsePropositionalModelChecker
class	SparseSmgRpatlModelChecker
class	SymbolicDtmcPrctlModelChecker
class	SymbolicMdpPrctlModelChecker
class	SymbolicParetoCurveCheckResult
class	SymbolicPropositionalModelChecker
class	SymbolicQualitativeCheckResult
class	SymbolicQuantitativeCheckResult
class	ValidatingSparseDtmcParameterLiftingModelChecker
class	ValidatingSparseMdpParameterLiftingModelChecker
class	ValidatingSparseParameterLiftingModelChecker

Enumerations
enum class	RegionCheckEngine { ParameterLifting , ExactParameterLifting , ValidatingParameterLifting }
	The considered engine for region checking. More...
enum class	RegionResult {   Unknown , ExistsSat , ExistsViolated , CenterSat ,   CenterViolated , ExistsBoth , AllSat , AllViolated }
	The results for a single Parameter Region. More...
enum class	RegionResultHypothesis { Unknown , AllSat , AllViolated }
	hypothesis for the result for a single Parameter Region More...
enum class	CheckType { Probabilities , Rewards }
enum class	StateFilter { ARGMIN , ARGMAX }
enum class	FilterType {   MIN , MAX , SUM , AVG ,   COUNT , FORALL , EXISTS , ARGMIN ,   ARGMAX , VALUES }

Functions
std::ostream &	operator<< (std::ostream &os, RegionCheckEngine const &e)
std::ostream &	operator<< (std::ostream &os, RegionResult const &regionResult)
std::ostream &	operator<< (std::ostream &os, RegionResultHypothesis const &regionResultHypothesis)
template<typename ValueType , typename SolutionType >
std::unique_ptr< CheckResult >	computeConditionalProbabilities (Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
template std::unique_ptr< CheckResult >	computeConditionalProbabilities (Environment const &env, storm::solver::SolveGoal< double > &&goal, storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
template std::unique_ptr< CheckResult >	computeConditionalProbabilities (Environment const &env, storm::solver::SolveGoal< storm::RationalNumber > &&goal, storm::storage::SparseMatrix< storm::RationalNumber > const &transitionMatrix, storm::storage::SparseMatrix< storm::RationalNumber > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
std::ostream &	operator<< (std::ostream &out, CheckResult const &checkResult)
template<typename JsonRationalType >
void	insertJsonEntry (storm::json< JsonRationalType > &json, uint64_t const &id, bool value, std::optional< storm::storage::sparse::StateValuations > const &stateValuations=std::nullopt, std::optional< storm::models::sparse::StateLabeling > const &stateLabels=std::nullopt)
template storm::json< storm::RationalNumber >	ExplicitQualitativeCheckResult::toJson< storm::RationalNumber > (std::optional< storm::storage::sparse::StateValuations > const &, std::optional< storm::models::sparse::StateLabeling > const &) const
template<typename ValueType >
void	print (std::ostream &out, ValueType const &value)
template<typename ValueType >
void	printRange (std::ostream &out, ValueType const &min, ValueType const &max)
template<typename ValueType >
void	insertJsonEntry (storm::json< ValueType > &json, uint64_t const &id, ValueType const &value, std::optional< storm::storage::sparse::StateValuations > const &stateValuations=std::nullopt, std::optional< storm::models::sparse::StateLabeling > const &stateLabels=std::nullopt)
std::string	toString (FilterType ft)
std::string	toPrismSyntax (FilterType ft)
bool	isStateFilter (FilterType)

Enumeration Type Documentation

CheckType

enum class storm::modelchecker::CheckType

strong

Enumerator
Probabilities
Rewards

Definition at line 24 of file CheckTask.h.

FilterType

enum class storm::modelchecker::FilterType

strong

Enumerator
MIN
MAX
SUM
AVG
COUNT
FORALL
EXISTS
ARGMIN
ARGMAX
VALUES

Definition at line 9 of file FilterType.h.

RegionCheckEngine

enum class storm::modelchecker::RegionCheckEngine

strong

The considered engine for region checking.

Enumerator
ParameterLifting	Parameter lifting approach.
ExactParameterLifting	Parameter lifting approach with exact arithmethics.
ValidatingParameterLifting	Parameter lifting approach with a) inexact (and fast) computation first and b) exact validation of obtained results second.

Definition at line 10 of file RegionCheckEngine.h.

RegionResult

enum class storm::modelchecker::RegionResult

strong

The results for a single Parameter Region.

Enumerator
Unknown	the result is unknown
ExistsSat	the formula is satisfied for at least one parameter evaluation that lies in the given region
ExistsViolated	the formula is violated for at least one parameter evaluation that lies in the given region
CenterSat	the formula is satisfied for the parameter Valuation that corresponds to the center point of the region
CenterViolated	the formula is violated for the parameter Valuation that corresponds to the center point of the region
ExistsBoth	the formula is satisfied for some parameters but also violated for others
AllSat	the formula is satisfied for all parameters in the given region
AllViolated	the formula is violated for all parameters in the given region

Definition at line 10 of file RegionResult.h.

RegionResultHypothesis

enum class storm::modelchecker::RegionResultHypothesis

strong

hypothesis for the result for a single Parameter Region

Enumerator
Unknown
AllSat
AllViolated

Definition at line 10 of file RegionResultHypothesis.h.

StateFilter

enum class storm::modelchecker::StateFilter

strong

Enumerator
ARGMIN
ARGMAX

Definition at line 7 of file FilterType.h.

Function Documentation

computeConditionalProbabilities() [1/3]

template std::unique_ptr< CheckResult > storm::modelchecker::computeConditionalProbabilities	(	Environment const &	env,
		storm::solver::SolveGoal< double > &&	goal,
		storm::storage::SparseMatrix< double > const &	transitionMatrix,
		storm::storage::SparseMatrix< double > const &	backwardTransitions,
		storm::storage::BitVector const &	targetStates,
		storm::storage::BitVector const &	conditionStates
	)

computeConditionalProbabilities() [2/3]

template std::unique_ptr< CheckResult > storm::modelchecker::computeConditionalProbabilities	(	Environment const &	env,
		storm::solver::SolveGoal< storm::RationalNumber > &&	goal,
		storm::storage::SparseMatrix< storm::RationalNumber > const &	transitionMatrix,
		storm::storage::SparseMatrix< storm::RationalNumber > const &	backwardTransitions,
		storm::storage::BitVector const &	targetStates,
		storm::storage::BitVector const &	conditionStates
	)

computeConditionalProbabilities() [3/3]

template<typename ValueType , typename SolutionType >

std::unique_ptr< CheckResult > storm::modelchecker::computeConditionalProbabilities	(	Environment const &	env,
		storm::solver::SolveGoal< ValueType, SolutionType > &&	goal,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	targetStates,
		storm::storage::BitVector const &	conditionStates
	)

Definition at line 705 of file ConditionalHelper.cpp.

ExplicitQualitativeCheckResult::toJson< storm::RationalNumber >()

template storm::json< storm::RationalNumber > storm::modelchecker::ExplicitQualitativeCheckResult::toJson< storm::RationalNumber >	(	std::optional< storm::storage::sparse::StateValuations > const &	,
		std::optional< storm::models::sparse::StateLabeling > const &
	)		const

insertJsonEntry() [1/2]

template<typename JsonRationalType >

void storm::modelchecker::insertJsonEntry	(	storm::json< JsonRationalType > &	json,
		uint64_t const &	id,
		bool	value,
		std::optional< storm::storage::sparse::StateValuations > const &	stateValuations = std::nullopt,
		std::optional< storm::models::sparse::StateLabeling > const &	stateLabels = std::nullopt
	)

Definition at line 245 of file ExplicitQualitativeCheckResult.cpp.

insertJsonEntry() [2/2]

template<typename ValueType >

void storm::modelchecker::insertJsonEntry	(	storm::json< ValueType > &	json,
		uint64_t const &	id,
		ValueType const &	value,
		std::optional< storm::storage::sparse::StateValuations > const &	stateValuations = std::nullopt,
		std::optional< storm::models::sparse::StateLabeling > const &	stateLabels = std::nullopt
	)

Definition at line 461 of file ExplicitQuantitativeCheckResult.cpp.

isStateFilter()

bool storm::modelchecker::isStateFilter

(

FilterType

)

operator<<() [1/4]

std::ostream & storm::modelchecker::operator<<	(	std::ostream &	os,
		RegionCheckEngine const &	e
	)

Definition at line 8 of file RegionCheckEngine.cpp.

operator<<() [2/4]

std::ostream & storm::modelchecker::operator<<	(	std::ostream &	os,
		RegionResult const &	regionResult
	)

Definition at line 8 of file RegionResult.cpp.

operator<<() [3/4]

std::ostream & storm::modelchecker::operator<<	(	std::ostream &	os,
		RegionResultHypothesis const &	regionResultHypothesis
	)

Definition at line 8 of file RegionResultHypothesis.cpp.

operator<<() [4/4]

std::ostream & storm::modelchecker::operator<<	(	std::ostream &	out,
		CheckResult const &	checkResult
	)

Definition at line 52 of file CheckResult.cpp.

print()

template<typename ValueType >

void storm::modelchecker::print	(	std::ostream &	out,
		ValueType const &	value
	)

Definition at line 239 of file ExplicitQuantitativeCheckResult.cpp.

printRange()

template<typename ValueType >

void storm::modelchecker::printRange	(	std::ostream &	out,
		ValueType const &	min,
		ValueType const &	max
	)

Definition at line 251 of file ExplicitQuantitativeCheckResult.cpp.

toPrismSyntax()

std::string storm::modelchecker::toPrismSyntax

(

FilterType

ft

)

Definition at line 35 of file FilterType.cpp.

toString()

std::string storm::modelchecker::toString

(

FilterType

ft

)

Definition at line 9 of file FilterType.cpp.