storm::gbar::api Namespace Reference

Typedefs
using	AbstractionRefinementOptions = storm::gbar::abstraction::AbstractionOptions

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 &, 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, 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 &, std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > 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 (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, AbstractionRefinementOptions const &options=AbstractionRefinementOptions())

Typedef Documentation

AbstractionRefinementOptions

using storm::gbar::api::AbstractionRefinementOptions = storm::gbar::abstraction::AbstractionOptions

Definition at line 16 of file verification.h.

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,
		AbstractionRefinementOptions const &	options = AbstractionRefinementOptions() )

Definition at line 92 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 &	,
		AbstractionRefinementOptions const &	= AbstractionRefinementOptions() )

Definition at line 85 of file verification.h.

verifyWithAbstractionRefinementEngine() [3/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 &	,
		storm::storage::SymbolicModelDescription const &	,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	,
		AbstractionRefinementOptions const &	= AbstractionRefinementOptions() )

Definition at line 43 of file verification.h.

verifyWithAbstractionRefinementEngine() [4/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,
		AbstractionRefinementOptions const &	options = AbstractionRefinementOptions() )

Definition at line 58 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 20 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 50 of file verification.h.