storm::modelchecker::lexicographic Namespace Reference

Typedefs
typedef std::function< storm::storage::BitVector(storm::logic::Formula const &)>	CheckFormulaCallback

Functions
template<typename SparseModelType , typename ValueType >
helper::MDPSparseModelCheckingHelperReturnType< ValueType >	check (Environment const &env, SparseModelType const &model, CheckTask< storm::logic::MultiObjectiveFormula, ValueType > const &checkTask, CheckFormulaCallback const &formulaChecker)
	check a lexicographic LTL-formula
template helper::MDPSparseModelCheckingHelperReturnType< double >	check< storm::models::sparse::Mdp< double >, double > (Environment const &env, storm::models::sparse::Mdp< double > const &model, CheckTask< storm::logic::MultiObjectiveFormula, double > const &checkTask, CheckFormulaCallback const &formulaChecker)

Typedef Documentation

CheckFormulaCallback

typedef std::function<storm::storage::BitVector(storm::logic::Formula const&)> storm::modelchecker::lexicographic::CheckFormulaCallback

Definition at line 16 of file lexicographicModelChecking.h.

Function Documentation

check()

template<typename SparseModelType , typename ValueType >

helper::MDPSparseModelCheckingHelperReturnType< ValueType > storm::modelchecker::lexicographic::check	(	Environment const &	,
		SparseModelType const &	model,
		CheckTask< storm::logic::MultiObjectiveFormula, ValueType > const &	checkTask,
		CheckFormulaCallback const &	formulaChecker
	)

check a lexicographic LTL-formula

Definition at line 17 of file lexicographicModelChecking.cpp.

check< storm::models::sparse::Mdp< double >, double >()

template helper::MDPSparseModelCheckingHelperReturnType< double > storm::modelchecker::lexicographic::check< storm::models::sparse::Mdp< double >, double >	(	Environment const &	env,
		storm::models::sparse::Mdp< double > const &	model,
		CheckTask< storm::logic::MultiObjectiveFormula, double > const &	checkTask,
		CheckFormulaCallback const &	formulaChecker
	)