verification.h File Reference

#include <type_traits>
#include "storm/environment/Environment.h"
#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h"
#include "storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h"
#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
#include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
#include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h"
#include "storm/models/symbolic/Dtmc.h"
#include "storm/models/symbolic/MarkovAutomaton.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/Smg.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/AbstractionSettings.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/EliminationSettings.h"
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/utility/macros.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.

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

Functions
template<typename ValueType >
storm::modelchecker::CheckTask< storm::logic::Formula, ValueType >	storm::api::createTask (std::shared_ptr< const storm::logic::Formula > const &formula, bool onlyInitialStatesRelevant=false)
template<typename ValueType >
std::enable_if< std::is_same< ValueType, double >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	storm::api::verifyWithExplorationEngine (storm::Environment const &env, storm::storage::SymbolicModelDescription const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::enable_if<!std::is_same< ValueType, double >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	storm::api::verifyWithExplorationEngine (storm::Environment const &, storm::storage::SymbolicModelDescription const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithExplorationEngine (storm::storage::SymbolicModelDescription const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &ctmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &ctmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	storm::api::verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Mdp< ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	storm::api::verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Mdp< ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::Mdp< ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	storm::api::verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &ma, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	storm::api::verifyWithSparseEngine (storm::Environment const &, std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &ma, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	storm::api::verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Smg< ValueType > > const &smg, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	storm::api::verifyWithSparseEngine (storm::Environment const &, std::shared_ptr< storm::models::sparse::Smg< ValueType > > const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::Smg< ValueType > > const &smg, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::computeSteadyStateDistributionWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::computeSteadyStateDistributionWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &ctmc)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::computeSteadyStateDistributionWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::computeExpectedVisitingTimesWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::computeExpectedVisitingTimesWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &ctmc)
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::computeExpectedVisitingTimesWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model)
template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithHybridEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithHybridEngine (std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithHybridEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Ctmc< DdType, ValueType > > const &ctmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithHybridEngine (std::shared_ptr< storm::models::symbolic::Ctmc< DdType, ValueType > > const &ctmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
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::api::verifyWithHybridEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
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::api::verifyWithHybridEngine (storm::Environment const &, std::shared_ptr< storm::models::symbolic::Mdp< 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::api::verifyWithHybridEngine (std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
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::api::verifyWithHybridEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::MarkovAutomaton< DdType, ValueType > > const &ma, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
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::api::verifyWithHybridEngine (storm::Environment const &, std::shared_ptr< storm::models::symbolic::MarkovAutomaton< 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::api::verifyWithHybridEngine (std::shared_ptr< storm::models::symbolic::MarkovAutomaton< DdType, ValueType > > const &ma, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithHybridEngine (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::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithHybridEngine (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::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithDdEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithDdEngine (std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
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::api::verifyWithDdEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
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::api::verifyWithDdEngine (storm::Environment const &, std::shared_ptr< storm::models::symbolic::Mdp< 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::api::verifyWithDdEngine (std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithDdEngine (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::unique_ptr< storm::modelchecker::CheckResult >	storm::api::verifyWithDdEngine (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)