storm::gbar::api Namespace Reference

Classes
struct	AbstractionRefinementOptions

Functions
template<storm::dd::DdType DdType, typename ValueType>
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithAbstractionRefinementEngine (storm::Environment const &env, storm::storage::SymbolicModelDescription const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, AbstractionRefinementOptions const &options=AbstractionRefinementOptions())
template<storm::dd::DdType DdType, typename ValueType>
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithAbstractionRefinementEngine (storm::Environment const &env, storm::storage::SymbolicModelDescription const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &, AbstractionRefinementOptions const &=AbstractionRefinementOptions())
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithAbstractionRefinementEngine (storm::storage::SymbolicModelDescription const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, AbstractionRefinementOptions const &options=AbstractionRefinementOptions())
template<storm::dd::DdType DdType, typename ValueType>
std::enable_if< std::is_same< ValueType, double >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithAbstractionRefinementEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<storm::dd::DdType DdType, typename ValueType>
std::enable_if<!std::is_same< ValueType, double >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithAbstractionRefinementEngine (storm::Environment const &, std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &)
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithAbstractionRefinementEngine (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

Function Documentation

verifyWithAbstractionRefinementEngine() [1/6]

template<storm::dd::DdType DdType, typename ValueType>

std::unique_ptr< storm::modelchecker::CheckResult > storm::gbar::api::verifyWithAbstractionRefinementEngine	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task )

Definition at line 101 of file verification.h.

verifyWithAbstractionRefinementEngine() [2/6]

template<storm::dd::DdType DdType, typename ValueType>

std::enable_if<!std::is_same< ValueType, double >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::gbar::api::verifyWithAbstractionRefinementEngine	(	storm::Environment const &	,
		std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	)

Definition at line 94 of file verification.h.

verifyWithAbstractionRefinementEngine() [3/6]

template<storm::dd::DdType DdType, typename ValueType>

std::enable_if< std::is_same< ValueType, double >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::gbar::api::verifyWithAbstractionRefinementEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task )

Definition at line 68 of file verification.h.

verifyWithAbstractionRefinementEngine() [4/6]

template<storm::dd::DdType DdType, typename ValueType>

std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::gbar::api::verifyWithAbstractionRefinementEngine	(	storm::Environment const &	env,
		storm::storage::SymbolicModelDescription const &	,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	,
		AbstractionRefinementOptions const &	= AbstractionRefinementOptions() )

Definition at line 53 of file verification.h.

verifyWithAbstractionRefinementEngine() [5/6]

template<storm::dd::DdType DdType, typename ValueType>

std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::gbar::api::verifyWithAbstractionRefinementEngine	(	storm::Environment const &	env,
		storm::storage::SymbolicModelDescription const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task,
		AbstractionRefinementOptions const &	options = AbstractionRefinementOptions() )

Definition at line 28 of file verification.h.

verifyWithAbstractionRefinementEngine() [6/6]

template<storm::dd::DdType DdType, typename ValueType>

std::unique_ptr< storm::modelchecker::CheckResult > storm::gbar::api::verifyWithAbstractionRefinementEngine	(	storm::storage::SymbolicModelDescription const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task,
		AbstractionRefinementOptions const &	options = AbstractionRefinementOptions() )

Definition at line 60 of file verification.h.