verification.h File Reference

#include "storm/environment/Environment.h"
#include "storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h"
#include "storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h"

Include dependency graph for verification.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	storm::gbar::api::AbstractionRefinementOptions

Namespaces
namespace	storm
	LabParser.cpp.
namespace	storm::gbar
namespace	storm::gbar::api

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	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())
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())
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())
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)
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 &)
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)