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

Classes
class	SymbolicMdpPrctlModelChecker
class	QuantitativeCheckResult
class	SymbolicQuantitativeCheckResult
class	SparseCtmcInstantiationModelChecker
	Class to efficiently check a formula on a parametric model with different parameter instantiations. More...
class	SparseDtmcInstantiationModelChecker
	Class to efficiently check a formula on a parametric model with different parameter instantiations. More...
class	SparseInstantiationModelChecker
	Class to efficiently check a formula on a parametric model with different parameter instantiations. More...
class	SparseMdpInstantiationModelChecker
	Class to efficiently check a formula on a parametric model with different parameter instantiations. More...
struct	AnnotatedRegion
struct	MonotonicityAnnotation
class	MonotonicityBackend
class	SparseDtmcParameterLiftingModelChecker
class	OrderBasedMonotonicityBackend
class	RegionModelChecker
class	PartitioningProgress
class	RegionRefinementChecker
struct	RegionSplittingStrategy
class	SparseMdpParameterLiftingModelChecker
class	SparseParameterLiftingModelChecker
	Class to approximately 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	ValidatingSparseParameterLiftingModelChecker
class	RegionCheckResult
class	RegionRefinementCheckResult
class	CheckTask
class	AbstractModelChecker
class	HybridCtmcCslModelChecker
class	HybridMarkovAutomatonCslModelChecker
class	SparseCtmcCslModelChecker
class	SparseMarkovAutomatonCslModelChecker
class	SparseExplorationModelChecker
class	ExplicitModelCheckerHint
	This class contains information that might accelerate the model checking process. More...
class	ModelCheckerHint
	This class contains information that might accelerate the model checking process. More...
class	HybridDtmcPrctlModelChecker
class	HybridMdpPrctlModelChecker
class	SparseDtmcPrctlModelChecker
class	SparseMdpPrctlModelChecker
class	SymbolicDtmcPrctlModelChecker
class	SparsePropositionalModelChecker
class	SymbolicPropositionalModelChecker
class	SparseDtmcEliminationModelChecker
class	ExplicitQualitativeCheckResult
class	ExplicitQuantitativeCheckResult
class	ExplicitParetoCurveCheckResult
class	LexicographicCheckResult
class	SymbolicQualitativeCheckResult
class	HybridQuantitativeCheckResult
class	SymbolicParetoCurveCheckResult
class	CheckResult
class	ParetoCurveCheckResult
class	QualitativeCheckResult
class	SparseSmgRpatlModelChecker

Typedefs
template<typename ConstantType, bool Robust>
using	SolverFactoryType
template<typename ConstantType, bool Robust>
using	GeneralSolverFactoryType
template<typename ParametricType, typename ConstantType, bool Robust>
using	ParameterLifterType

Enumerations
enum class	RegionCheckEngine { ParameterLifting , ExactParameterLifting , ValidatingParameterLifting , RobustParameterLifting }
	The considered engine for region checking. More...
enum class	RegionResult { Unknown , ExistsSat , ExistsViolated , ExistsIllDefined , CenterSat , CenterViolated , CenterIllDefined , ExistsBoth , AllSat , AllViolated , AllIllDefined }
	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	RegionSplitEstimateKind { Distance , StateValueDelta , StateValueDeltaWeighted , Derivative }
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)
std::ostream &	operator<< (std::ostream &os, RegionSplittingStrategy::Heuristic const &e)
template<typename ConstantType>
std::optional< storm::storage::Scheduler< ConstantType > >	getSchedulerHelper (std::optional< std::vector< uint64_t > > const &choices)
bool	supportsStateValueDeltaEstimates (storm::logic::Formula const &f)
bool	supportsOrderBasedMonotonicity (storm::logic::Formula const &f)
template<typename RegionType>
auto	getOptimalValuationForMonotonicity (RegionType const &region, std::map< typename RegionType::VariableType, storm::analysis::MonotonicityKind > const &monotonicityResult, storm::OptimizationDirection dir)
template<typename ValueType, typename SolutionType>
std::unique_ptr< CheckResult >	computeConditionalProbabilities (Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, bool produceSchedulers, 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, bool produceSchedulers, 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, bool produceSchedulers, 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<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)

Typedef Documentation

◆ GeneralSolverFactoryType

template<typename ConstantType, bool Robust>

using storm::modelchecker::GeneralSolverFactoryType

Initial value:

std::conditional_t<Robust, storm::solver::GeneralMinMaxLinearEquationSolverFactory<storm::Interval, ConstantType>,

storm::solver::GeneralMinMaxLinearEquationSolverFactory<ConstantType>>

storm::solver::GeneralMinMaxLinearEquationSolverFactory

Definition MinMaxLinearEquationSolver.h:269

Definition at line 28 of file SparseDtmcParameterLiftingModelChecker.h.

◆ ParameterLifterType

template<typename ParametricType, typename ConstantType, bool Robust>

using storm::modelchecker::ParameterLifterType

Initial value:

std::conditional_t<Robust, storm::transformer::RobustParameterLifter<ParametricType, ConstantType>,

storm::transformer::ParameterLifter<ParametricType, ConstantType>>

storm::transformer::ParameterLifter

This class lifts parameter choices to nondeterminism: For each row in the given matrix that considerd...

Definition ParameterLifter.h:40

Definition at line 32 of file SparseDtmcParameterLiftingModelChecker.h.

◆ SolverFactoryType

template<typename ConstantType, bool Robust>

using storm::modelchecker::SolverFactoryType

Initial value:

std::conditional_t<Robust, storm::solver::MinMaxLinearEquationSolverFactory<storm::Interval, ConstantType>,

storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>

storm::solver::MinMaxLinearEquationSolverFactory

Definition MinMaxLinearEquationSolver.h:244

Definition at line 24 of file SparseDtmcParameterLiftingModelChecker.h.

Enumeration Type Documentation

◆ CheckType

enum class storm::modelchecker::CheckType

strong

Enumerator
Probabilities
Rewards

Definition at line 25 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.
RobustParameterLifting	Parameter lifting approach based on robust markov models instead of generating nondeterminism.

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
ExistsIllDefined	the formula is ill-defined 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
CenterIllDefined	the formula is ill-defined 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 well-defined parameters in the given region
AllViolated	the formula is violated for all well-defined parameters in the given region
AllIllDefined	the formula is ill-defined 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.

◆ RegionSplitEstimateKind

enum class storm::modelchecker::RegionSplitEstimateKind

strong

Enumerator
Distance
StateValueDelta
StateValueDeltaWeighted
Derivative

Definition at line 4 of file RegionSplitEstimateKind.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,
		bool	produceSchedulers,
		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,
		bool	produceSchedulers,
		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,
		bool	produceSchedulers,
		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 1273 of file ConditionalHelper.cpp.

◆ getOptimalValuationForMonotonicity()

template<typename RegionType>

auto storm::modelchecker::getOptimalValuationForMonotonicity	(	RegionType const &	region,
		std::map< typename RegionType::VariableType, storm::analysis::MonotonicityKind > const &	monotonicityResult,
		storm::OptimizationDirection	dir )

Definition at line 67 of file SparseParameterLiftingModelChecker.cpp.

◆ getSchedulerHelper()

template<typename ConstantType>

std::optional< storm::storage::Scheduler< ConstantType > > storm::modelchecker::getSchedulerHelper ( std::optional< std::vector< uint64_t > > const & choices )

Definition at line 812 of file SparseDtmcParameterLiftingModelChecker.cpp.

◆ 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 300 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 460 of file ExplicitQuantitativeCheckResult.cpp.

◆ isStateFilter()

bool storm::modelchecker::isStateFilter ( FilterType )

◆ operator<<() [1/5]

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

Definition at line 8 of file RegionCheckEngine.cpp.

◆ operator<<() [2/5]

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

Definition at line 8 of file RegionResult.cpp.

◆ operator<<() [3/5]

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

Definition at line 8 of file RegionResultHypothesis.cpp.

◆ operator<<() [4/5]

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

Definition at line 8 of file RegionSplittingStrategy.cpp.

◆ operator<<() [5/5]

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

Definition at line 48 of file CheckResult.cpp.

◆ print()

template<typename ValueType>

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

Definition at line 240 of file ExplicitQuantitativeCheckResult.cpp.

◆ printRange()

template<typename ValueType>

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

Definition at line 252 of file ExplicitQuantitativeCheckResult.cpp.

◆ supportsOrderBasedMonotonicity()

bool storm::modelchecker::supportsOrderBasedMonotonicity ( storm::logic::Formula const & f )

Definition at line 843 of file SparseDtmcParameterLiftingModelChecker.cpp.

◆ supportsStateValueDeltaEstimates()

bool storm::modelchecker::supportsStateValueDeltaEstimates ( storm::logic::Formula const & f )

Definition at line 835 of file SparseDtmcParameterLiftingModelChecker.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.

Namespaces

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ GeneralSolverFactoryType

◆ ParameterLifterType

◆ SolverFactoryType

Enumeration Type Documentation

◆ CheckType

◆ FilterType

◆ RegionCheckEngine

◆ RegionResult

◆ RegionResultHypothesis

◆ RegionSplitEstimateKind

◆ StateFilter

Function Documentation

◆ computeConditionalProbabilities() [1/3]

◆ computeConditionalProbabilities() [2/3]

◆ computeConditionalProbabilities() [3/3]

◆ getOptimalValuationForMonotonicity()

◆ getSchedulerHelper()

◆ insertJsonEntry() [1/2]

◆ insertJsonEntry() [2/2]

◆ isStateFilter()

◆ operator<<() [1/5]

◆ operator<<() [2/5]

◆ operator<<() [3/5]

◆ operator<<() [4/5]

◆ operator<<() [5/5]

◆ print()

◆ printRange()

◆ supportsOrderBasedMonotonicity()

◆ supportsStateValueDeltaEstimates()

◆ toPrismSyntax()

◆ toString()